LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
sav08:dpll_algorithm_for_sat [2008/03/13 17:46]
vkuncak
sav08:dpll_algorithm_for_sat [2013/04/17 17:35]
vkuncak
Line 100: Line 100:
     S' \vdash {\it false}     S' \vdash {\it false}
 \] \]
-++++Idea:| 
 From From
 \[ \[
Line 120: Line 119:
  
 Why can we modify resolution proof to move $p$ from assumption and put its negation to conclusion? Why can we modify resolution proof to move $p$ from assumption and put its negation to conclusion?
-+++++
  
 === Lower Bounds on Running Time === === Lower Bounds on Running Time ===
Line 128: Line 127:
 Theorem: for some formulas, shortest resolution proofs are exponential. 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.+This does not contradict ​that P vs NP question ​is open, 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]]): 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]]   * Pavel Pudlák: [[http://​citeseer.ist.psu.edu/​36219.html|Lower Bounds for Resolution and Cutting Plane Proofs and Monotone Computations]]