Package org.tweetyproject.logics.pl.sat
Class SimpleDpllSolver
java.lang.Object
org.tweetyproject.logics.pl.sat.SatSolver
org.tweetyproject.logics.pl.sat.SimpleDpllSolver
- All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>
,ConsistencyTester<BeliefSet<PlFormula,
,?>> ConsistencyWitnessProvider<PlBeliefSet,
PlFormula>
This class provides a simple reference implementation of the DPLL (Davis–Putnam–Logemann–Loveland)
algorithm for satisfiability testing, see e.g https://en.wikipedia.org/wiki/DPLL_algorithm.
The order of the variables is simply taken by the standard iterator of the induced signature. Only
unit propagation is used for satisfiability testing.
- Author:
- Matthias Thimm
-
Constructor Summary
-
Method Summary
Modifier and TypeMethodDescriptiongetWitness
(Collection<PlFormula> formulas) If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.boolean
Return whether the solve ris installedboolean
isSatisfiable
(Collection<PlFormula> formulas) Checks whether the given set of formulas is satisfiable.Methods inherited from class org.tweetyproject.logics.pl.sat.SatSolver
getDefaultSolver, getWitness, getWitness, hasDefaultSolver, isConsistent, isConsistent, isConsistent, setDefaultSolver
-
Constructor Details
-
SimpleDpllSolver
public SimpleDpllSolver()Default Constructor
-
-
Method Details
-
getWitness
Description copied from class:SatSolver
If the collection of formulas is consistent this method returns some model of it or, if it is inconsistent, null.- Specified by:
getWitness
in interfaceConsistencyWitnessProvider<PlBeliefSet,
PlFormula> - Specified by:
getWitness
in classSatSolver
- Parameters:
formulas
- a set of formulas- Returns:
- some model of the formulas or null.
-
isSatisfiable
Description copied from class:SatSolver
Checks whether the given set of formulas is satisfiable.- Specified by:
isSatisfiable
in classSatSolver
- Parameters:
formulas
- a set of formulas.- Returns:
- "true" if the set is consistent.
-
isInstalled
public boolean isInstalled()Description copied from class:SatSolver
Return whether the solve ris installed- Specified by:
isInstalled
in classSatSolver
- Returns:
- whether the solve ris installed
-