public class SimpleDpllSolver extends SatSolver
Constructor and Description |
---|
SimpleDpllSolver() |
Modifier and Type | Method and Description |
---|---|
Interpretation<PlBeliefSet,PropositionalFormula> |
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
public Interpretation<PlBeliefSet,PropositionalFormula> getWitness(java.util.Collection<PropositionalFormula> formulas)
SatSolver
getWitness
in interface ConsistencyWitnessProvider<PlBeliefSet,PropositionalFormula>
getWitness
in class SatSolver
public boolean isSatisfiable(java.util.Collection<PropositionalFormula> formulas)
SatSolver
isSatisfiable
in class SatSolver
formulas
- a set of formulas.