Package org.tweetyproject.sat.minisat

Class MinisatSatSolver

java.lang.Object

org.tweetyproject.sat.minisat.MinisatSatSolver

All Implemented Interfaces:

AutoCloseable, SatSolver

public final class MinisatSatSolver
extends Object
implements SatSolver

This class provides an implementation of the `SatSolver` interface using the MiniSat SAT solver. MiniSat is a widely used, efficient solver for boolean satisfiability problems.

The class handles interactions with the native MiniSat solver through bindings, allowing for operations such as variable creation, clause addition, and satisfiability checking.

Constructor Summary

Constructors

Constructor	Description
MinisatSatSolver()	Initializes a new instance of the MiniSat SAT solver.

Method Summary

Modifier and Type	Method	Description
void	add(int[] clause)	Adds the given clause to the SAT solver state.
void	close()
int	newVar()	Creates and returns the integer representation of a fresh propositional variable.
boolean	satisfiable()	Checks if the formula is satisfiable without any assumptions.
boolean	satisfiable(int[] assumptions)	Checks if the formula is satisfiable under the given assumptions.
boolean[]	witness(int[] atoms)	Returns the truth assignment of the given variables assuming no assumptions.
boolean[]	witness(int[] atoms, int[] assumptions)	Returns the truth assignment of the given variables under the specified assumptions.

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Details

MinisatSatSolver

public MinisatSatSolver()

Initializes a new instance of the MiniSat SAT solver.

This constructor initializes the MiniSat solver instance by calling the native `init` method through the `Binding` class. The handle to the MiniSat instance is stored in the `handle` field.

Method Details

satisfiable

public boolean satisfiable()

Description copied from interface: SatSolver

Checks if the formula is satisfiable without any assumptions.

This is a default method that delegates to SatSolver.satisfiable(int[]) with an empty array of assumptions.

Specified by:

satisfiable in interface SatSolver

Returns:

true if the formula is satisfiable, false otherwise.

satisfiable

public boolean satisfiable(int[] assumptions)

Description copied from interface: SatSolver

Checks if the formula is satisfiable under the given assumptions.

Specified by:

satisfiable in interface SatSolver

Parameters:

assumptions - an array of literals that are assumed to be true. If the array is empty, no assumptions are made.

Returns:

true if the formula is satisfiable under the assumptions, false otherwise.

witness

public boolean[] witness(int[] atoms)

Description copied from interface: SatSolver

Returns the truth assignment of the given variables assuming no assumptions.

This is a default method that delegates to SatSolver.witness(int[], int[]) with an empty array of assumptions.

Specified by:

witness in interface SatSolver

Parameters:

atoms - an array of variable indices for which the truth assignment is requested.

Returns:

an array of booleans representing the truth assignment of the given variables.

witness

public boolean[] witness(int[] atoms,
 int[] assumptions)

Description copied from interface: SatSolver

Returns the truth assignment of the given variables under the specified assumptions.

Specified by:

witness in interface SatSolver

Parameters:

atoms - an array of variable indices for which the truth assignment is requested.

assumptions - an array of literals that are assumed to be true. If the array is empty, no assumptions are made.

Returns:

an array of booleans representing the truth assignment of the given variables under the assumptions.

add

public void add(int[] clause)

Description copied from interface: SatSolver

Adds the given clause to the SAT solver state.

Note that contrary to DIMACS format, a trailing '0' is not required!

Specified by:

add in interface SatSolver

Parameters:

clause - the clause to add

newVar

public int newVar()

Description copied from interface: SatSolver

Creates and returns the integer representation of a fresh propositional variable.

It is necessary to only use variables returned by this method, since some solvers require to first allocate and maintain a data structure of the variables before they can be used in clauses. Hence, using integers not returned by this method may work for some solvers, but not for others.

Specified by:

newVar in interface SatSolver

Returns:

the integer representation

close

public void close()

Specified by:

close in interface AutoCloseable

Specified by:

close in interface SatSolver