SAT.MiniSat

This module provides high-level Haskell bindings for the well-known 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, well-optimized general-purpose 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 low-level C functions, to give the user fine-grained interactive control over the SAT solver, or to provide building blocks for developing new SAT solvers. Rather, we package the SAT solver as a general-purpose tool that can easily be integrated into other programs as a turn-key solution to many search problems.

It is well-known that the boolean satisfiability problem is NP-complete, 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 general-purpose SAT solver can often be a time saver.

We provide a convenient high-level 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 low-level 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.

Boolean formulas

data Formula v

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.

Constructors

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)

Let a f is the formula "let x=a in fx", which permits the subexpression a to be re-used. It is logically equivalent to fa, but typically smaller.

Bound Integer

For internal use only.

Instances

Eq v => Eq (Formula v)

Ord v => Ord (Formula v)

Show v => Show (Formula v)

SAT solver interface

satisfiable :: Ord v => Formula v -> Bool

Check whether a boolean formula is satisfiable.

solve :: Ord v => Formula v -> Maybe (Map v Bool)

Return a satisfying assignment for the boolean formula, if any.

solve_all :: Ord v => Formula v -> [Map v Bool]

Lazily enumerate all satisfying assignments for the boolean formula.