|
|
|
|
|
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 |
|
|
|
|
Interface
|
|
|
The depth-first method.
|
|
Data Types
|
|
|
Constructors | ResolutionTrace | | 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 | |
|
| Instances | |
|
|
|
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 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.
|
| Instances | |
|
|
|
Unsatisfiable cores are not unique.
|
|
Produced by Haddock version 2.3.0 |