This is an old revision of the document!
DPLL Algorithm for SAT
Approach:
- boolean constraint propagation when possible
- case analysis on variables for completeness
INPUT: set of clauses (see Normal Forms for Propositional Logic, Definition of Propositional Resolution)
OUTPUT: true iff there exists an interpretation that makes true
Terminology
A unit clause is or where .
Unit resolution is application of resolution to two clauses where at least one clause is a unit clause.
- like substituting the value of variable forced by the unit clause
Boolean Constraint Propagation
Apply unit resolution as much as possible.
def BCP(S : Set[Clause]) : Set[Clause] = if for some unit clause U and clause C in S, resolve(U,C) is not in in S then BCP(S union resolve(U,C)) else S
Note: for each unit clause and other clause we can perform unit resolution at most once (variable disappears)
- BCP is polynomial procedure
We do not need to keep literals that are subset of existing ones:
def RemoveSubsumed(S : Set[Clause]) : Set[Clause] = if there are C1,C2 in S such that C1 subset C2 then RemoveSubsumes(S - {C2}) else S
In particular, when we apply unit resolution, the original clause can be deleted.
DPLL Recursively
def DPLL(S : Set[Clause]) : boolean = val S' = RemoveSubsumed(BCP(S)) if (emptyClause in S') then false else if (S' has only unit clauses) then true else val P = pick variable from FV(S') DPLL(F' union {p}) or DPLL(F' union {Not(p)})
State Representation
State representation - group clauses by number of elements:
- S.C (conflict, size zero): true if empty clause was derived
- S.A (assignment, size one): partial map from to
- for
- for
- S.B: the remaining clauses
To check satisfiability of set of clauses, invoke DPLL procedure with
- S.C=false
- S.A=EmptyMap
- S.B containing all desired clauses
Desired invariants:
- if S.A(p) defined, then p does not occur in S.B
- S.B has only clauses with at least two literals
Maintaining invariant - part of BCP
- if S.A(p)=1, delete from S.B clauses containing and remove literals from clauses in S.B
- if S.A(p)=0, delete from S.B clauses containing and remove literals from clauses in S.B
- if empty clause is in S.B, set S.C to true
- if is in S.B, then set
- if is in S.B, then set
Termination conditions (when invariants hold):
- if S.C, set is unsatisfiable
- if S.B is empty and not S.C, then S.A gives satisfying assignment
Emiting a Satisfying Assignments or a Proof
Instead of returning just true/false we want SAT solver to return
- one satisfying assignment, if is satisfiable (easy: print S.A)
- proof, if is unsatisfiable - in some format
Emiting resolution proofs - needs extra work
Unit resolution is resolution, so we can construct proofs directly.
Decision step (picking variable value): from proofs for \[
S' \cup \{p\} \vdash {\it false}
\] \[
S' \cup \{\lnot p\} \vdash {\it false}
\] we would like to construct the proof for \[
S' \vdash {\it false}
\] From \[
S' \cup \{p\} \vdash {\it false}
\] derive proof tree for \[
S' \vdash \lnot p
\] and from \[
S' \cup \{\lnot p\} \vdash {\it false}
\] derive proof tree for \[
S' \vdash p
\] Then combine these two trees with resolution on and to get .
Why can we modify resolution proof to move from assumption and put its negation to conclusion?
Lower Bounds on Running Time
Observation: constructed resolution proof is polynomial in the running time of the DPLL algorithm.
Theorem: for some formulas, shortest resolution proofs are exponential.
This does not contradict P vs NP question, because there may be “better” proof systems than resolution.
Lower bounds for both resolution and a stronger system are shown here by proving that interpolants can be exponential, and that interpolants are polynomial in proof size (see Interpolants from Resolution Proofs):