logic-classes-1.4.8: Framework for propositional and first order logic, theorem proving

MaintainerSebastian Fischer (sebf@informatik.uni-kiel.de)
Safe HaskellSafe-Inferred



This Haskell library provides an implementation of the Davis-Putnam-Logemann-Loveland algorithm (cf. http://en.wikipedia.org/wiki/DPLL_algorithm) for the boolean satisfiability problem. It not only allows to solve boolean formulas in one go but also to add constraints and query bindings of variables incrementally.

The implementation is not sophisticated at all but uses the basic DPLL algorithm with unit propagation.



data Boolean Source

Boolean formulas are represented as values of type Boolean.


Var Int

Variables are labeled with an Int,


Yes represents true,


No represents false,

Not Boolean

Not constructs negated formulas,

Boolean :&&: Boolean

and finally we provide conjunction

Boolean :||: Boolean

and disjunction of boolean formulas.


data SatSolver Source

A SatSolver can be used to solve boolean formulas.


data Literal Source

Literals are variables that occur either positively or negatively.


Pos Int 
Neg Int 

literalVar :: Literal -> IntSource

This function returns the name of the variable in a literal.

invLiteral :: Literal -> LiteralSource

This function negates a literal.

isPositiveLiteral :: Literal -> BoolSource

This predicate checks whether the given literal is positive.

type CNF = [Clause]Source

Conjunctive normalforms are lists of lists of literals.

booleanToCNF :: Boolean -> CNFSource

We convert boolean formulas to conjunctive normal form by pushing negations down to variables and repeatedly applying the distributive laws.

newSatSolver :: SatSolverSource

A new SAT solver without stored constraints.

isSolved :: SatSolver -> BoolSource

This predicate tells whether all constraints are solved.

lookupVar :: Int -> SatSolver -> Maybe BoolSource

We can lookup the binding of a variable according to the currently stored constraints. If the variable is unbound, the result is Nothing.

assertTrue :: MonadPlus m => Boolean -> SatSolver -> m SatSolverSource

We can assert boolean formulas to update a SatSolver. The assertion may fail if the resulting constraints are unsatisfiable.

branchOnVar :: MonadPlus m => Int -> SatSolver -> m SatSolverSource

This function guesses a value for the given variable, if it is currently unbound. As this is a non-deterministic operation, the resulting solvers are returned in an instance of MonadPlus.

selectBranchVar :: SatSolver -> IntSource

We select a variable from the shortest clause hoping to produce a unit clause.

solve :: MonadPlus m => SatSolver -> m SatSolverSource

This function guesses values for variables such that the stored constraints are satisfied. The result may be non-deterministic and is, hence, returned in an instance of MonadPlus.

isSolvable :: SatSolver -> BoolSource

This predicate tells whether the stored constraints are solvable. Use with care! This might be an inefficient operation. It tries to find a solution using backtracking and returns True if and only if that fails.