funsat-0.5.2: A modern DPLL-style SAT solver




Generates and checks a resolution proof of UNSAT from a resolution trace of a SAT solver (Funsat in particular will generate this trace). This is based on the implementation discussed in the paper ''Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications'' by Lintao Zhang and Sharad Malik.

As a side effect of this process an unsatisfiable core is generated from the resolution trace, as discussed in the paper ''Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula'' by Zhang and Malik.



Data Types

data ResolutionTrace Source




traceFinalClauseId :: ClauseId

The id of the last, conflicting clause in the solving process.

traceFinalAssignment :: IAssignment

Final assignment.

Precondition: All variables assigned at decision level zero.

traceSources :: Map ClauseId [ClauseId]

Invariant: Each id has at least one source (otherwise that id should not even have a mapping).

Invariant: Should be ordered topologically backward (?) from each conflict clause. (IOW, record each clause id as its encountered when generating the conflict clause.)

traceOriginalClauses :: Map ClauseId Clause

Original clauses of the CNF input formula.

traceAntecedents :: Map Var ClauseId

data ResolutionError Source

A type indicating an error in the checking process. Assuming this checker's code is correct, such an error indicates a bug in the SAT solver.


ResolveError Var Clause Clause

Indicates that the clauses do not properly resolve on the variable.

CannotResolve [Var] Clause Clause

Indicates that the clauses do not have complementary variables or have too many. The complementary variables (if any) are in the list.

AntecedentNotUnit Clause

Indicates that the constructed antecedent clause not unit under traceFinalAssignment.

AntecedentImplication (Clause, Lit) Var

Indicates that in the clause-lit pair, the unit literal of clause is the literal, but it ought to be the variable.

AntecedentMissing Var

Indicates that the variable has no antecedent mapping, in which case it should never have been assigned/encountered in the first place.

EmptySource ClauseId

Indicates that the clause id has an entry in traceSources but no resolution sources.

OrphanSource ClauseId

Indicates that the clause id is referenced but has no entry in traceSources.

type UnsatisfiableCore = [Clause]Source

Unsatisfiable cores are not unique.