Title: A note on SAT algorithms and proof complexity
Abstract: 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(Fd) 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 Fd. Such results can be interpreted as a form of consistency of P≠NP. Further we show how the soundness statements can be used to find hard satisfiable instances, if they exist.
Publication Year: 2012
Publication Date: 2012-03-17
Language: en
Type: article
Indexed In: ['crossref']
Access and Citation
Cited By Count: 33
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot