|
|
|
|
|
| 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
|
|
|
| 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.
|
|
|
| Solve with the default configuration defaultConfig.
|
|
|
| The solution to a SAT problem is either an assignment or unsatisfiable.
| | Constructors | |  Instances | |
|
|
| Verification
|
|
|
| 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.
|
|
|
| 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 | |
|
|
| Configuration
|
|
|
| Configuration parameters for the solver.
| | Constructors | | Cfg | | | 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 | |
|
|
|
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
|
|
|
| Constructors | | Stats | | | 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 | |
|
|
|
| The show instance uses the wrapped string.
| | Constructors | | | Instances | |
|
|
|
| Convert statistics to a nice-to-display tabular form.
|
|
|
| Converts statistics into a tabular, human-readable summary.
|
|
| Produced by Haddock version 2.1.0 |
