LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:dpll_algorithm_for_sat [2013/04/17 17:34]
vkuncak
sav08:dpll_algorithm_for_sat [2013/04/17 17:35]
vkuncak
Line 127: 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]]