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 (see Funsat.Resolution) and a logical circuit interface (see Funsat.Circuit). New in 0.6: circuits and BSD3 license.
[Skip to Readme]
Versions | 0.4, 0.5, 0.5.1, 0.5.2, 0.6.0, 0.6.1, 0.6.2 |
---|---|
Change log | CHANGES |
Dependencies | array, base, bimap (==0.2.*), bitset (==0.*), containers, fgl, mtl, parse-dimacs (>=1.2 && <2), pretty, QuickCheck (<2), random, time [details] |
License | BSD-3-Clause |
Author | Denis Bueno |
Maintainer | Denis Bueno <dbueno@gmail.com> |
Category | Algorithms |
Home page | http://github.com/dbueno/funsat |
Uploaded | by DenisBueno at Fri Apr 17 22:51:25 UTC 2009 |
Distributions | NixOS:0.6.2 |
Executables | funsat |
Downloads | 2730 total (15 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 |
Modules
[Index]
Downloads
- funsat-0.6.0.tar.gz [browse] (Cabal source package)
- Package description (as included in the package)