Funsat aims to be a reasonably efficient modern SAT solver that is easy to integrate as a backend to other projects. SAT is NPcomplete, and thus has reductions from many other interesting problems. We hope this implementation is efficient enough to make it useful to solve mediumsize, realworld problem mapped from another space. We also aim to test the solver rigorously to encourage confidence in its output.
One particular nicetie facilitating integration of Funsat into other projects is the efficient calculation of an unsatisfiable core for unsatisfiable problems (see the Funsat.Resolution module). In the case a problem is unsatisfiable, as a byproduct of checking the proof of unsatisfiability, Funsat will generate a minimal set of input clauses that are also unsatisfiable.
 07 Jun 2008 21:43:42: N.B. because of the use of mutable arrays in the ST monad, the solver will actually give _wrong_ answers if you compile without optimisation. Which is okay, 'cause that's really slow anyway.
Bibliography
 ''Abstract DPLL and DPLL Modulo Theories''
 ''Chaff: Engineering an Efficient SAT solver''
 ''An Extensible SATsolver'' by Niklas Een, Niklas Sorensson
 ''Efficient Conflict Driven Learning in a Boolean Satisfiability Solver'' by Zhang, Madigan, Moskewicz, Malik
 ''SATMICRO: petit mais costaud!'' by Conchon, Kanig, and Lescuyer
 solve :: DPLLConfig > CNF > (Solution, Stats, Maybe ResolutionTrace)
 solve1 :: CNF > (Solution, Stats, Maybe ResolutionTrace)
 data Solution
 verify :: Solution > Maybe ResolutionTrace > CNF > Maybe VerifyError
 data VerifyError
 = SatError [(Clause, Either () Bool)]
  UnsatError ResolutionError
 data DPLLConfig = Cfg {
 configRestart :: !Int64
 configRestartBump :: !Double
 configUseVSIDS :: !Bool
 configUseRestarts :: !Bool
 defaultConfig :: CNF > DPLLConfig
 data Stats = Stats {}
 newtype ShowWrapped = WrapString {}
 statTable :: Stats > Table ShowWrapped
 statSummary :: Stats > String
Interface
solve :: DPLLConfig > CNF > (Solution, Stats, Maybe ResolutionTrace)Source
solve1 :: CNF > (Solution, Stats, Maybe ResolutionTrace)Source
Solve with the default configuration defaultConfig
.
Verification
verify :: Solution > Maybe ResolutionTrace > CNF > Maybe VerifyErrorSource
data VerifyError Source
SatError [(Clause, Either () Bool)]  Indicates a unsatisfactory assignment that was claimed
satisfactory. Each clause is tagged with its status using

UnsatError ResolutionError  Indicates an error in the resultion checking process. 
Configuration
data DPLLConfig Source
Configuration parameters for the solver.
Cfg  

defaultConfig :: CNF > DPLLConfigSource
A default configuration based on the formula to solve.
 restarts every 100 conflicts
 requires 1.5 as many restarts after restarting as before, each time
 VSIDS to be enabled
 restarts to be enabled
Solver statistics
Stats  

newtype ShowWrapped Source
The show instance uses the wrapped string.
statTable :: Stats > Table ShowWrappedSource
Convert statistics to a nicetodisplay tabular form.
statSummary :: Stats > StringSource
Converts statistics into a tabular, humanreadable summary.