public class Sat4jSolver extends SatSolver
Modifier and Type | Field and Description |
---|---|
private int |
maxvar
Max number of variables for this solver.
|
private static int |
MAXVAR
Default value for max number of variables for asolver.
|
private int |
nbclauses
Max number of expected clauses for this solver.
|
private static int |
NBCLAUSES
Default value for max number of expected clauses for a solver.
|
Constructor and Description |
---|
Sat4jSolver()
Creates a new solver with default parameters (maxvar=1000000, nbclauses=500000).
|
Sat4jSolver(int maxvar,
int nbclauses)
Creates a new solver with the given parameters.
|
Modifier and Type | Method and Description |
---|---|
Interpretation |
getWitness(java.util.Collection<PropositionalFormula> formulas)
If the collection of formulas is consistent this method
returns some model of it or, if it is inconsistent, null.
|
boolean |
isSatisfiable(java.util.Collection<PropositionalFormula> formulas)
Checks whether the given set of formulas is satisfiable.
|
convertToDimacs, convertToDimacs, createTmpDimacsFile, createTmpDimacsFile, getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver, setTempFolder
private static final int MAXVAR
private static final int NBCLAUSES
private int maxvar
private int nbclauses
public Sat4jSolver(int maxvar, int nbclauses)
maxvar
- Max number of variables for this solver.nbclauses
- Max number of expected clauses for this solver.public Sat4jSolver()
public boolean isSatisfiable(java.util.Collection<PropositionalFormula> formulas)
SatSolver
isSatisfiable
in class SatSolver
formulas
- a set of formulas.public Interpretation getWitness(java.util.Collection<PropositionalFormula> formulas)
SatSolver
getWitness
in interface ConsistencyWitnessProvider<PropositionalFormula>
getWitness
in class SatSolver