The funsat package

[Tags: bsd3, library, program]

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).

[Skip to ReadMe]


Versions0.4, 0.5, 0.5.1, 0.5.2, 0.6.0, 0.6.1, 0.6.2
Change logNone available
Dependenciesarray, base, bitset, containers, fgl, mtl, parse-dimacs, parsec, pretty, QuickCheck, random, time [details]
AuthorDenis Bueno
MaintainerDenis Bueno <>
UploadedTue Jun 10 02:32:30 UTC 2008 by DenisBueno
Downloads1204 total (52 in last 30 days)
0 []
StatusDocs uploaded by user
Build status unknown [no reports yet]




Maintainers' corner

For package maintainers and hackage trustees

Readme for funsat-0.5

-*- mode: outline -*-

* A DPLL-style SAT solver in pure Haskell
Install using the typical Cabal procedure:

$ ./Setup.lhs configure
$ ./Setup.lhs 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, uncomment the profiling executable in funsat.cabal, and a profiling
binary will automatically be built in ./dist/build/funsat-prof/funsat-prof.

** Dependencies
All the dependences are cabal-ised and available from hackage.  URLs below.

They're also available in subdirectories.

*** parse-dimacs [cnf]
A haskell CNF file parser.

*** bitset [bitset]