A modern DPLL-style SAT solver http://github.com/dbueno/funsat
|Latest on Hackage:||0.6.2|
This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.
* 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
Currently along this theme we provide /unsatisfiable core/ generation, giving
(hopefully) small unsatisfiable sub-problems of unsatisfiable input problems
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
All the dependences are cabal-ised and available from hackage, or in etc/.
A haskell CNF file parser.
- Logical circuit representation added.
- License is now BSD3, which is apparently happier for some people.
Maintenance update because a new (incompatible) version of bitset, version 1.0,
was released. Funsat should again compile via cabal-install.
** Update for compatibility with parse-dimacs 1.2,
which should mean faster parsing.
** Code cleanup