0380502 - MÚ 2013 RIV NL eng J - Článek v odborném periodiku
Krajíček, Jan
A note on SAT algorithms and proof complexity.
Information Processing Letters. Roč. 112, č. 12 (2012), s. 490-493. ISSN 0020-0190. E-ISSN 1872-6119
Grant CEP: GA AV ČR IAA100190902
Výzkumný záměr: CEZ:AV0Z10190503
Klíčová slova: computational complexity
Kód oboru RIV: BA - Obecná matematika
Impakt faktor: 0.488, rok: 2012
http://www.sciencedirect.com/science/article/pii/S0020019012000774

We apply classical proof complexity ideas to transfer lengths-of-proofs lower bounds for a propositional proof system P into examples of hard unsatisfiable formulas for a class Alg(P) of SAT algorithms determined by P. The class Alg(P) contains those algorithms M for which P proves in polynomial size tautologies expressing the soundness of M. For example, the class Alg(F-d) determined by a depth d Frege system contains the commonly considered enhancements of DPLL (even for small d). Exponential lower bounds are known for all F-d. Such results can be interpreted as a form of consistency of P not equal NP. Further we show how the soundness statements can be used to find hard satisfiable instances, if they exist.
Trvalý link: http://hdl.handle.net/11104/0211194