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. It is possible to use funsat both as a library and as a standalone executable.

[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 <>
UploadedFri Jun 6 14:45:44 UTC 2008 by DenisBueno
Downloads1272 total (35 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.4

-*- 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]