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 19:31] 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 |
- | ===== DPLL Imperatively ===== | + | **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}$. | ||
- | Selecting order of variables. | + | Why can we modify resolution proof to move $p$ from assumption and put its negation to conclusion? |
+ | ++++ | ||
- | Lemma learning. | + | === 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]] | ||