funsat: A modern DPLL-style SAT solver

[ algorithms, bsd3, library, program ] [ Propose Tags ] [ Report a vulnerability ]

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, giving (hopefully) small unsatisfiable sub-problems of unsatisfiable input problems (see Funsat.Resolution).

[Skip to Readme]

Modules

[Index]

Control
- Monad
  - Control.Monad.MonadST
Funsat
Text
- Text.Tabular

Downloads

funsat-0.5.tar.gz [browse] (Cabal source package)
Package description (revised from the package)

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

Package maintainers

DenisBueno

For package maintainers and hackage trustees

edit package information

Candidates

No Candidates

Versions [RSS]	0.4, 0.5, 0.5.1, 0.5.2, 0.6.0, 0.6.1, 0.6.2
Dependencies	array, base (<4.8), bitset, containers, fgl, mtl, parse-dimacs, parsec, pretty, QuickCheck, random, time [details]
License	LicenseRef-LGPL
Author	Denis Bueno
Maintainer	Denis Bueno <dbueno@gmail.com>
Revised	Revision 1 made by sjakobi at 2022-01-28T22:50:13Z
Category	Algorithms
Uploaded	by DenisBueno at 2008-06-10T02:32:30Z
Distributions
Reverse Dependencies	2 direct, 0 indirect [details]
Executables	funsat
Downloads	5788 total (23 in the last 30 days)
Rating	(no votes yet) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs uploaded by user Build status unknown [no reports yet]

Readme for funsat-0.5

[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.

http://hackage.haskell.org/cgi-bin/hackage-scripts/package/parse-dimacs

*** bitset [bitset]
http://hackage.haskell.org/cgi-bin/hackage-scripts/package/bitset