Funsat.Solver

Contents

Description

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.

Bibliography

''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

Synopsis

Interface

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 when the result is Unsat.

solve1 :: CNF -> (Solution, Stats, Maybe ResolutionTrace)Source

Solve with the default configuration defaultConfig.

data Solution Source

The solution to a SAT problem. In each case we return an assignment, which is obviously right in the Sat case; in the Unsat case, the reason is to assist in the generation of an unsatisfiable core.

Constructors

Sat IAssignment
Unsat IAssignment

Instances

Eq Solution
Show Solution

Verification

verify :: Solution -> Maybe ResolutionTrace -> CNF -> Maybe VerifyError Source

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

Constructors

SatError [(Clause, Either () Bool)]	Indicates a unsatisfactory assignment that was claimed satisfactory. Each clause is tagged with its status using `Model.statusUnder`.
UnsatError ResolutionError	Indicates an error in the resultion checking process.

Instances

Show VerifyError

Configuration

data DPLLConfig Source

Configuration parameters for the solver.

Constructors

Cfg
Fields configRestart :: !Int64 Number of conflicts before a restart. configRestartBump :: !Double `configRestart` is altered after each restart by multiplying it by this value. configUseVSIDS :: !Bool If true, use dynamic variable ordering. configUseRestarts :: !Bool

Instances

Show DPLLConfig

defaultConfig :: CNF -> DPLLConfig Source

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

Constructors

Stats

Fields

statsNumConfl :: Int64: Number of conflicts since last restart.
statsNumConflTotal :: Int64: Number of conflicts since beginning of solving.
statsNumLearnt :: Int64: Number of learned clauses currently in DB (fluctuates because DB is compacted every restart).
statsAvgLearntLen :: Double: Avg. number of literals per learnt clause.
statsNumDecisions :: Int64: Total number of decisions since beginning of solving.
statsNumImpl :: Int64: Total number of unit implications since beginning of solving.

Instances

Show Stats

newtype ShowWrapped Source

The show instance uses the wrapped string.

Constructors

WrapString
Fields unwrapString :: String

Instances

Show ShowWrapped

statTable :: Stats -> Table ShowWrapped Source

Convert statistics to a nice-to-display tabular form.

statSummary :: Stats -> String Source

Converts statistics into a tabular, human-readable summary.