Class MinisatSatSolver
- All Implemented Interfaces:
AutoCloseable
,SatSolver
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
-
Method Summary
Modifier and TypeMethodDescriptionvoid
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
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.
-
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 interfaceSatSolver
- 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 interfaceSatSolver
- 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. -
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 interfaceSatSolver
- 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
-
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.
-
close
public void close()- Specified by:
close
in interfaceAutoCloseable
- Specified by:
close
in interfaceSatSolver
-