Safe Haskell  None 

Language  Haskell98 
This module provides highlevel Haskell bindings for the wellknown MiniSat satisfiability solver. It solves the boolean satisfiability problem, i.e., the input is a boolean formula, and the output is a list of all satisfying assignments. MiniSat is a fully automated, welloptimized generalpurpose SAT solver written by Niklas Een and Niklas Sorensson, and further modified by Takahisa Toda.
Unlike other similar Haskell packages, the purpose of this library is not to provide access to lowlevel C functions, to give the user finegrained interactive control over the SAT solver, or to provide building blocks for developing new SAT solvers. Rather, we package the SAT solver as a generalpurpose tool that can easily be integrated into other programs as a turnkey solution to many search problems.
It is wellknown that the boolean satisfiability problem is NPcomplete, and therefore, no SAT solver can be efficient for all inputs. However, there are many search problems that can be naturally expressed as satisfiability problems and are nevertheless tractable. Writing custom code to traverse the search space is tedious and rarely efficient, especially in cases where the size of the search space is sensitive to the order of traversal. This is where using a generalpurpose SAT solver can often be a time saver.
We provide a convenient highlevel interface to the SAT solver,
hiding the complexity of the underlying C implementation. The main
API function is solve_all
, which inputs a boolean formula, and
outputs a list of all satisfying assignments (which are modelled as
maps from variables to truth values). The list is generated lazily,
so that the underlying lowlevel C code only does as much work as
necessary.
Two example programs illustrating the use of this library can be found in the "examples" directory of the Cabal package.
 data Formula v
 = Var v
  Yes
  No
  Not (Formula v)
  (Formula v) :&&: (Formula v)
  (Formula v) :: (Formula v)
  (Formula v) :++: (Formula v)
  (Formula v) :>: (Formula v)
  (Formula v) :<>: (Formula v)
  All [Formula v]
  Some [Formula v]
  None [Formula v]
  ExactlyOne [Formula v]
  AtMostOne [Formula v]
  Let (Formula v) (Formula v > Formula v)
  Bound Integer
 satisfiable :: Ord v => Formula v > Bool
 solve :: Ord v => Formula v > Maybe (Map v Bool)
 solve_all :: Ord v => Formula v > [Map v Bool]
Boolean formulas
The type of boolean formulas. It is parametric over a set of
variables v. We provide the usual boolean operators, including
implications and exclusive or. For convenience, we also provide the
list quantifiers All
, Some
, None
, ExactlyOne
, and
AtMostOne
, as well as a general Let
operator that can be
used to reduce the size of repetitive formulas.
Var v  A variable. 
Yes  The formula true. 
No  The formula false. 
Not (Formula v)  Negation. 
(Formula v) :&&: (Formula v) infixr 6  Conjunction. 
(Formula v) :: (Formula v) infixr 5  Disjunction. 
(Formula v) :++: (Formula v) infixr 4  Exclusive or. 
(Formula v) :>: (Formula v) infixr 2  Implication. 
(Formula v) :<>: (Formula v) infix 1  If and only if. 
All [Formula v]  All are true. 
Some [Formula v]  At least one is true. 
None [Formula v]  None are true. 
ExactlyOne [Formula v]  Exactly one is true. 
AtMostOne [Formula v]  At most one is true. 
Let (Formula v) (Formula v > Formula v) 

Bound Integer  For internal use only. 