Hackage :: [Package]

funsat: A modern DPLL-style SAT solver

[ algorithms, bsd3, library, program ] [ Propose Tags ]

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 (see Funsat.Resolution) and a logical circuit interface (see Funsat.Circuit). New in 0.6: circuits and BSD3 license.

[Skip to Readme]

Modules

[Last Documentation]

  • Control
    • Monad
      • Control.Monad.MonadST
  • Funsat
    • Funsat.Circuit
    • Funsat.Monad
    • Funsat.Resolution
    • Funsat.Solver
    • Funsat.Types
      • Funsat.Types.Internal
    • Funsat.Utils
      • Funsat.Utils.Internal
  • Text
    • Text.Tabular

Downloads

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 (>=0.2 && <0.3), base (>=3 && <5), bimap (>=0.2 && <0.3), bitset (<1), containers (>=0.2 && <0.3), fgl (>=5 && <=5.4.2.2), mtl (>=1 && <2), parse-dimacs (>=1.2 && <2), pretty (<2), QuickCheck (<2), random (<2), time (<1.2) [details]
License BSD-3-Clause
Author Denis Bueno
Maintainer Denis Bueno <dbueno@gmail.com>
Category Algorithms
Home page http://github.com/dbueno/funsat
Uploaded by DenisBueno at 2010-06-26T20:43:58Z
Distributions
Reverse Dependencies 2 direct, 0 indirect [details]
Executables funsat
Downloads 5686 total (18 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-29 [all 6 reports]

Readme for funsat-0.6.1

[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