Differences

This shows you the differences between two versions of the page.

--- 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 =====
-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]]