[Haskell-cafe] ANN: funsat 0.5, a SAT solver written in Haskell

Denis Bueno dbueno at gmail.com
Mon Jun 9 23:00:10 EDT 2008

Hi all,

It is my pleasure to announce the first reasonable release of funsat,
a modern, DPLL-style SAT solver written in Haskell.  Funsat solves
formulas in conjunctive normal form and produces a total variable
assignment for satisfiable problems.  It is available from Hackage:


As well as in a Git repo, which contains many benchmark files funsat can solve.

    git clone http://churn.ath.cx/funsat

Funsat is intended to be reasonably efficient for practical problems
and convenient to use as a constraint-solving backend in other

The former is achieved by using several well-known techniques from the
literature including two-watched literals, conflict-directed learning,
non-chronological backtracking, a VSIDS-like dynamic variable
ordering, and restarts.  The latter is supported currently by
efficient unsatisfiable core generation, which generates a minimal
unsatisfiable problem for a given unsatisfiable problem.  In the
future, I plan to add support for converting boolean circuits into
CNF, as well as support for other types of constraints.

Please try it out and report bugs!  (This email is the one listed on
the website.)


More information about the Haskell-Cafe mailing list