Funsat.Resolution

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.

Interface

genUnsatCore :: ResolutionTrace -> Either ResolutionError UnsatisfiableCore

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 UnsatisfiableCore

The depth-first method.

Data Types

data ResolutionTrace

A resolution trace records how the SAT solver proved the original CNF formula unsatisfiable.

Constructors

ResolutionTrace

Fields

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

Show ResolutionTrace

initResolutionTrace :: ClauseId -> IAssignment -> ResolutionTrace

data ResolutionError

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

Show ResolutionError

Error ResolutionError

type UnsatisfiableCore = [Clause]

Unsatisfiable cores are not unique.