funsat: A modern DPLL-style SAT solver
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).
| Versions | 0.4, 0.5, 0.5.1, 0.5.2, 0.6.0 |
|---|---|
| Dependencies | array, base, bitset, containers, fgl, mtl, parse-dimacs (>=1.2), parsec, pretty, QuickCheck, random, time |
| License | LGPL |
| Author | Denis Bueno |
| Maintainer | Denis Bueno <dbueno@gmail.com> |
| Stability | alpha |
| Category | Algorithms |
| Home page | http://github.com/dbueno/funsat |
| Executables | funsat |
| Upload date | Sat Oct 18 20:38:25 UTC 2008 |
| Uploaded by | DenisBueno |
| Built on | ghc-6.10 |
| Build failure | ghc-6.12 (log), ghc-6.8 (log) |
| Distributions | Arch: 0.6.0 |
Modules
- Control
- Funsat
- Text
Downloads
- funsat-0.5.1.tar.gz (Cabal source package)
- package description (included in the package)