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
|The depth-first method.
|traceFinalClauseId :: ClauseId||The id of the last, conflicting clause in the solving process.
|traceFinalAssignment :: IAssignment|
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|
|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
|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
|AntecedentNotUnit Clause||Indicates that the constructed antecedent clause not unit under
|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
|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
|Unsatisfiable cores are not unique.
|Produced by Haddock version 2.3.0|