funsat-0.5: A modern DPLL-style SAT solverSource codeContentsIndex
Solver statistics

Funsat aims to be a reasonably efficient modern SAT solver that is easy to integrate as a backend to other projects. SAT is NP-complete, and thus has reductions from many other interesting problems. We hope this implementation is efficient enough to make it useful to solve medium-size, real-world 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 by-product 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.
  • ''Abstract DPLL and DPLL Modulo Theories''
  • ''Chaff: Engineering an Efficient SAT solver''
  • ''An Extensible SAT-solver'' by Niklas Een, Niklas Sorensson
  • ''Efficient Conflict Driven Learning in a Boolean Satisfiability Solver'' by Zhang, Madigan, Moskewicz, Malik
  • ''SAT-MICRO: petit mais costaud!'' by Conchon, Kanig, and Lescuyer
solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace)
solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace)
data Solution
= Sat IAssignment
| Unsat IAssignment
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 {
statsNumConfl :: Int64
statsNumConflTotal :: Int64
statsNumLearnt :: Int64
statsAvgLearntLen :: Double
statsNumDecisions :: Int64
statsNumImpl :: Int64
newtype ShowWrapped = WrapString {
unwrapString :: String
statTable :: Stats -> Table ShowWrapped
statSummary :: Stats -> String
solve :: DPLLConfig -> CNF -> (Solution, Stats, Maybe ResolutionTrace)Source
Run the DPLL-based SAT solver on the given CNF instance. Returns a solution, along with internal solver statistics and possibly a resolution trace. The trace is for checking a proof of Unsat, and thus is only present then.
solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace)Source
Solve with the default configuration defaultConfig.
data Solution Source
The solution to a SAT problem is either an assignment or unsatisfiable.
Sat IAssignment
Unsat IAssignment
show/hide Instances
verify :: Solution -> Maybe ResolutionTrace -> CNF -> Maybe VerifyErrorSource
Verify the solution. In case of Sat, checks that the assignment is well-formed and satisfies the CNF problem. In case of Unsat, runs a resolution-based checker on a trace of the SAT solver.
data VerifyError Source
SatError [(Clause, Either () Bool)]Indicates a unsatisfactory assignment that was claimed satisfactory. Each clause is tagged with its status using Model.statusUnder.
UnsatError ResolutionErrorIndicates an error in the resultion checking process.
show/hide Instances
data DPLLConfig Source
Configuration parameters for the solver.
configRestart :: !Int64Number of conflicts before a restart.
configRestartBump :: !DoubleconfigRestart is altered after each restart by multiplying it by this value.
configUseVSIDS :: !BoolIf true, use dynamic variable ordering.
configUseRestarts :: !Bool
show/hide Instances
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
data Stats Source
statsNumConfl :: Int64Number of conflicts since last restart.
statsNumConflTotal :: Int64Number of conflicts since beginning of solving.
statsNumLearnt :: Int64Number of learned clauses currently in DB (fluctuates because DB is compacted every restart).
statsAvgLearntLen :: DoubleAvg. number of literals per learnt clause.
statsNumDecisions :: Int64Total number of decisions since beginning of solving.
statsNumImpl :: Int64Total number of unit implications since beginning of solving.
show/hide Instances
newtype ShowWrapped Source
The show instance uses the wrapped string.
unwrapString :: String
show/hide Instances
statTable :: Stats -> Table ShowWrappedSource
Convert statistics to a nice-to-display tabular form.
statSummary :: Stats -> StringSource
Converts statistics into a tabular, human-readable summary.
Produced by Haddock version 2.1.0