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