Generates and checks a resolution proof of Unsat
from a
resolution trace of a SAT solver (Funsat.Solver.solve
will generate this
trace). As a side effect of this process an unsatisfiable core is
generated from the resolution trace. This core is a (hopefully small) subset
of the input clauses which is still unsatisfiable. Intuitively, it a concise
reason why the problem is unsatisfiable.
The resolution trace checker is based on the implementation from the paper ''Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications'' by Lintao Zhang and Sharad Malik. Unsatisfiable cores are discussed in the paper ''Extracting Small Unsatisfiable Cores from Unsatisfiable Boolean Formula'' by Zhang and Malik.
- genUnsatCore :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore
- checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore
- data ResolutionTrace = ResolutionTrace {}
- initResolutionTrace :: ClauseId -> IAssignment -> ResolutionTrace
- data ResolutionError
- type UnsatisfiableCore = [Clause]
Interface
genUnsatCore :: ResolutionTrace -> Either ResolutionError UnsatisfiableCoreSource
Check the given resolution trace of a (putatively) unsatisfiable formula.
If the result is ResolutionError
, the proof trace has failed to establish
the unsatisfiability of the formula. Otherwise, an unsatisfiable core of
clauses is returned.
This function simply calls checkDepthFirst
.
checkDepthFirst :: ResolutionTrace -> Either ResolutionError UnsatisfiableCoreSource
The depth-first method.
Data Types
data ResolutionTrace Source
A resolution trace records how the SAT solver proved the original CNF formula unsatisfiable.
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.