A modern DPLL-style SAT solver

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 to host generated Haddocks.

BSD3 licensed by Denis Bueno
Maintained by Denis Bueno
-*- 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

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

** Dependencies
All the dependences are cabal-ised and available from hackage, or in etc/.

*** parse-dimacs
A haskell CNF file parser.

*** bitset


-*- mode: outline -*-

* 0.6.0
- Logical circuit representation added.
- License is now BSD3, which is apparently happier for some people.

* 0.5.2
Maintenance update because a new (incompatible) version of bitset, version 1.0,
was released. Funsat should again compile via cabal-install.

* 0.5.1
** Update for compatibility with parse-dimacs 1.2,
which should mean faster parsing.
** Code cleanup

comments powered byDisqus