Differences
This shows you the differences between two versions of the page.
|
sav08:dpll_algorithm_for_sat [2013/04/17 17: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 | ||
| - | |||
| - | We do not need to keep literals that are subset of existing ones: | ||
| - | <code> | ||
| - | 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 | ||
| - | </code> | ||
| - | In particular, when we apply unit resolution, the original clause can be deleted. | ||
| - | |||
| - | ===== DPLL Recursively ===== | ||
| - | |||
| - | <code> | ||
| - | 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)}) | ||
| - | </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} | ||
| - | \] | ||
| - | 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 (see [[Interpolants from Resolution Proofs]]): | ||
| - | * Pavel Pudlák: [[http://citeseer.ist.psu.edu/36219.html|Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations]] | ||