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]


Versions 0.4, 0.5, 0.5.1, 0.5.2, 0.6.0, 0.6.1, 0.6.2
Dependencies array, base, bitset, containers, fgl, mtl, parse-dimacs, parsec, pretty, QuickCheck, random, time [details]
License LGPL
Author Denis Bueno
Maintainer Denis Bueno <>
Category Algorithms
Uploaded Fri Jun 6 14:45:44 UTC 2008 by DenisBueno
Distributions NixOS:0.6.2
Downloads 1656 total (5 in the last 30 days)
0 []
Status Docs uploaded by user
Build status unknown [no reports yet]




Maintainer's Corner

For package maintainers and hackage trustees

Readme for funsat

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]