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

[Denis Bueno]

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:

    http://hackage.haskell.org/cgi-bin/hackage-scripts/package/funsat
    http://churn.ath.cx/funsat.html

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
software.

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.)

-- 
 Denis