Hackage :: [Package]

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]

Downloads

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

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.4, 0.5, 0.5.1, 0.5.2, 0.6.0, 0.6.1, 0.6.2
Change log CHANGES
Dependencies array, base (<4.8), bitset (<1), containers, fgl, mtl, parse-dimacs (>=1.2 && <2), 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:12Z
Category Algorithms
Home page http://github.com/dbueno/funsat
Uploaded by DenisBueno at 2009-02-18T14:07:25Z
Distributions
Reverse Dependencies 2 direct, 0 indirect [details]
Executables funsat
Downloads 5848 total (7 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.2

[back to package description] 
-*- 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