Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Denis Bueno <dbueno <at> gmail.com>
Subject: ANN: funsat 0.5, a SAT solver written in Haskell
Newsgroups: gmane.comp.lang.haskell.cafe
Date: Tuesday 10th June 2008 03:00:10 UTC (over 9 years ago)
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
 
CD: 4ms