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.
- checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore
- data ResolutionTrace = ResolutionTrace {}
- initResolutionTrace :: ClauseId -> IAssignment -> ResolutionTrace
- data ResolutionError
- type UnsatisfiableCore = [Clause]
Interface
checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCoreSource
The depth-first method.
Data Types
data ResolutionTrace Source
ResolutionTrace | |
|
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
|
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 |
OrphanSource ClauseId | Indicates that the clause id is referenced but has no entry in
|
type UnsatisfiableCore = [Clause]Source
Unsatisfiable cores are not unique.