The funsat package
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.2: works with ghc-6.12 and fixed some space leaks. =/
Properties
| Versions | 0.4, 0.5, 0.5.1, 0.5.2, 0.6.0, 0.6.1, 0.6.2 |
|---|---|
| Dependencies | array, base (<4), bimap (0.2.*), bitset (1.*), containers, fgl, mtl, parse-dimacs (≥1.2 & <2), pretty, QuickCheck (2.*), random, time |
| License | BSD3 |
| Author | Denis Bueno |
| Maintainer | Denis Bueno <dbueno@gmail.com> |
| Stability | beta |
| Category | Algorithms |
| Home page | http://github.com/dbueno/funsat |
| Executables | funsat |
| Upload date | Sun Feb 27 01:35:19 UTC 2011 |
| Uploaded by | DenisBueno |
| Build failure | ghc-7.0 (log) |
Modules
- Control
- Monad
- Control.Monad.MonadST
- Monad
- Funsat
- Funsat.Circuit
- Funsat.Monad
- Funsat.Resolution
- Funsat.Solver
- Funsat.Types
- Funsat.Types.Internal
- Text
- Text.Tabular
Downloads
- funsat-0.6.2.tar.gz (Cabal source package)
- package description (included in the package)