Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav08:dpll_algorithm_for_sat [2008/03/12 17:34] vkuncak |
sav08:dpll_algorithm_for_sat [2008/03/12 18:34] vkuncak |
||
---|---|---|---|
Line 72: | Line 72: | ||
===== Emiting a Satisfying Assignments or a Proof ===== | ===== Emiting a Satisfying Assignments or a Proof ===== | ||
- | Satisfying assignment: propagate or branch until map is complete. | + | 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 | ||
- | Proof 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 ===== | ===== DPLL Imperatively ===== | ||
Line 82: | Line 130: | ||
Lemma learning. | Lemma learning. | ||
- |