dbueno / funsat

An efficient, embeddable DPLL SAT solver in Haskell

This URL has Read+Write access

funsat /
name age
history
message
file .gitignore Fri Jul 04 07:29:18 -0700 2008 Ignore compiled Setup.hs files. [dbueno]
file CHANGES Loading commit data...
file ClauseTrie.hs
file LICENSE
file Main.hs
file README Sat Oct 18 13:22:51 -0700 2008 indent [dbueno]
file README.benchmark Mon Jul 07 17:03:06 -0700 2008 Sanely name the test and benchmarking scripts. ... [dbueno]
file Setup.hs Fri Jun 06 07:32:36 -0700 2008 Refactor to prepare for release onto Hackage. [dbueno]
file ashish.org
directory bench-results/ Thu May 08 06:24:36 -0700 2008 used bm results [dbueno]
directory bench/ Sat Oct 18 13:03:56 -0700 2008 Describe how these two files work together. [dbueno]
file benchmark.sh Sat Oct 18 13:03:56 -0700 2008 Describe how these two files work together. [dbueno]
file bugs.org
directory doc/ Fri Jun 06 14:43:14 -0700 2008 pdfs [dbueno]
file dsat.prof.current
directory etc/
file funsat.cabal
directory src/
file test.sh
directory tests/
file todo.org
directory website/ Fri Jul 04 06:35:01 -0700 2008 License note. [dbueno]
README
-*- mode: outline -*-

* Funsat: A DPLL-style SAT solver in pure Haskell

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").


* Installation
Install using the typical Cabal procedure:

    $ ghc --make -o Setup Setup.hs
    $ ./Setup configure
    $ ./Setup 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, a profiling binary is automatically built in
./dist/build/funsat-prof/funsat-prof.

** Dependencies
All the dependences are cabal-ised and available from hackage, or in etc/.

*** parse-dimacs
A haskell CNF file parser.

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

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