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
DPLL Recursively
def DPLL(S : Set[Clause]) : boolean = val S' = 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
Satisfying assignment: propagate or branch until map is complete.
Proof format.
DPLL Imperatively
Selecting order of variables.
Lemma learning.