Differences
This shows you the differences between two versions of the page.
sav08:dpll_algorithm_for_sat [2008/03/12 18:34] vkuncak |
sav08:dpll_algorithm_for_sat [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== DPLL Algorithm for SAT ====== | ||
- | Approach: | ||
- | * boolean constraint propagation when possible | ||
- | * case analysis on variables for completeness | ||
- | |||
- | INPUT: set of clauses $S$ (see [[Normal Forms for Propositional Logic]], [[Definition of Propositional Resolution]]) | ||
- | |||
- | OUTPUT: //true// iff there exists an interpretation that makes $S$ //true// | ||
- | |||
- | ===== Terminology ===== | ||
- | |||
- | A **unit clause** is $\{p\}$ or $\{\lnot p\}$ where $p \in V$. | ||
- | |||
- | **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. | ||
- | <code> | ||
- | 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 | ||
- | </code> | ||
- | |||
- | Note: for each unit clause and other clause we can perform unit resolution at most once (variable disappears) | ||
- | * BCP is polynomial procedure | ||
- | |||
- | ===== DPLL Recursively ===== | ||
- | |||
- | <code> | ||
- | 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)}) | ||
- | </code> | ||
- | |||
- | ===== 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 $V$ to $\{0,1\}$ | ||
- | * $p \mapsto 1$ for $\{p\}$ | ||
- | * $p \mapsto 0$ for $\{\lnot p\}$ | ||
- | * 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 $p$ and remove literals $\lnot p$ from clauses in S.B | ||
- | * if S.A(p)=0, delete from S.B clauses containing $\lnot p$ and remove literals $p$ from clauses in S.B | ||
- | * if empty clause is in S.B, set S.C to true | ||
- | * if $\{p\}$ is in S.B, then set $S.A(p)=1$ | ||
- | * if $\{\lnot p\}$ is in S.B, then set $S.A(p)=0$ | ||
- | |||
- | 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 $S$ is satisfiable (easy: print S.A) | ||
- | * proof, if $S$ 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} | ||
- | \] | ||
- | ++++Idea:| | ||
- | 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 $\{p\}$ and $\{\lnot p\}$ to get ${\it false}$. | ||
- | |||
- | Why can we modify resolution proof to move $p$ 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: | ||
- | * Pavel Pudlák: [[http://citeseer.ist.psu.edu/36219.html|Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations]] | ||
- | |||
- | ===== DPLL Imperatively ===== | ||
- | |||
- | |||
- | Selecting order of variables. | ||
- | |||
- | Lemma learning. |