funsat-0.5.1: A modern DPLL-style SAT solverSource codeContentsIndex
Funsat.Resolution
Contents
Interface
Data Types
Description

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.

Synopsis
checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore
data ResolutionTrace = ResolutionTrace {
traceFinalClauseId :: ClauseId
traceFinalAssignment :: IAssignment
traceSources :: Map ClauseId [ClauseId]
traceOriginalClauses :: Map ClauseId Clause
traceAntecedents :: Map Var ClauseId
}
data ResolutionError
= ResolveError Var Clause Clause
| CannotResolve [Var] Clause Clause
| AntecedentNotUnit Clause
| AntecedentImplication (Clause, Lit) Var
| AntecedentMissing Var
| EmptySource ClauseId
| OrphanSource ClauseId
type UnsatisfiableCore = [Clause]
Interface
checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCoreSource
The depth-first method.
Data Types
data ResolutionTrace Source
Constructors
ResolutionTrace
traceFinalClauseId :: ClauseIdThe 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 ClauseOriginal clauses of the CNF input formula.
traceAntecedents :: Map Var ClauseId
show/hide Instances
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.
Constructors
ResolveError Var Clause ClauseIndicates that the clauses do not properly resolve on the variable.
CannotResolve [Var] Clause ClauseIndicates that the clauses do not have complementary variables or have too many. The complementary variables (if any) are in the list.
AntecedentNotUnit ClauseIndicates that the constructed antecedent clause not unit under traceFinalAssignment.
AntecedentImplication (Clause, Lit) VarIndicates that in the clause-lit pair, the unit literal of clause is the literal, but it ought to be the variable.
AntecedentMissing VarIndicates that the variable has no antecedent mapping, in which case it should never have been assigned/encountered in the first place.
EmptySource ClauseIdIndicates that the clause id has an entry in traceSources but no resolution sources.
OrphanSource ClauseIdIndicates that the clause id is referenced but has no entry in traceSources.
show/hide Instances
type UnsatisfiableCore = [Clause]Source
Unsatisfiable cores are not unique.
Produced by Haddock version 2.3.0