-*- mode: outline -*-
* Funsat: A DPLL-style SAT solver in pure Haskell
Funsat is a native Haskell SAT solver that uses modern techniques for solving
SAT instances. Current features include two-watched literals, conflict-directed
learning, non-chronological backtracking, a VSIDS-like dynamic variable
ordering, and restarts. Our goal is to facilitate convenient embedding of a
reasonably fast SAT solver as a constraint solving backend in other
applications.
Currently along this theme we provide /unsatisfiable core/ generation, giving
(hopefully) small unsatisfiable sub-problems of unsatisfiable input problems
(see "Funsat.Resolution").
* Installation
Install using the typical Cabal procedure:
$ ghc --make -o Setup Setup.hs
$ ./Setup configure
$ ./Setup build
This will produce a binary called funsat at ./dist/build/funsat/funsat and a
standalone library interface for the solver. If you feel like profiling the
code, a profiling binary is automatically built in
./dist/build/funsat-prof/funsat-prof.
** Dependencies
All the dependences are cabal-ised and available from hackage, or in etc/.
*** parse-dimacs
A haskell CNF file parser.
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/parse-dimacs
*** bitset
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/bitset