funsat: A modern DPLL-style SAT solver

[ algorithms, bsd3, library, program ] [ Propose Tags ]

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 LicenseRef-LGPL
Author Denis Bueno
Maintainer Denis Bueno <>
Category Algorithms
Uploaded by DenisBueno at Fri Jun 6 14:45:44 UTC 2008
Distributions NixOS:0.6.2
Executables funsat
Downloads 2765 total (21 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user
Build status unknown [no reports yet]
Hackage Matrix CI




Maintainer's Corner

For package maintainers and hackage trustees

Readme for funsat-0.4

[back to package description]
-*- 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]