Class SimpleDpllSolver

All Implemented Interfaces:
BeliefSetConsistencyTester<PlFormula>, ConsistencyTester<BeliefSet<PlFormula,?>>, ConsistencyWitnessProvider<PlBeliefSet,PlFormula>

public class SimpleDpllSolver extends SatSolver
This class provides a simple reference implementation of the DPLL (Davis–Putnam–Logemann–Loveland) algorithm for satisfiability testing, see e.g The order of the variables is simply taken by the standard iterator of the induced signature. Only unit propagation is used for satisfiability testing.
Matthias Thimm