Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
An efficient, embeddable DPLL SAT solver in Haskell
Groff Haskell Other
Failed to load latest commit information.
bench-results/2008-05-07.1732
bench
doc
etc
src
tests
website
.gitignore
CHANGES
LICENSE Change licenses to BSD3
Main.hs
README
README.benchmark
Setup.hs
benchmark.sh cleanup
funsat.cabal
test.sh

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:

    $ cabal configure
    $ cabal 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.

** Testing

All the problems in tests/problems should run through.

  uf20 and uf50 - satisfiable
  uuf50 - unsatisfiable

** 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


Something went wrong with that request. Please try again.