-*- 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
Build the project with the `cabal.project` in this repository:

    $ cabal build
    $ cabal run funsat -- --version

This builds the `funsat` executable, the library, and the local package
dependencies listed in `cabal.project`.

To run the solver on a DIMACS CNF instance:

    $ cabal run funsat -- tests/problems/uf20/uf20-010.cnf

To run the test suite:

    $ cabal test funsat-tests

If you want to use the compiled executable directly, find the path with:

    $ cabal list-bin funsat

** Testing

The `funsat-tests` suite runs the regression corpus in `tests/problems`.
Expected results by corpus:

  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