A note on SAT algorithms and proof complexity
| Autor: | Jan Krajíček |
|---|---|
| Rok vydání: | 2012 |
| Předmět: |
Discrete mathematics
Soundness Class (set theory) Polynomial Computational complexity theory Propositional proof system Proof complexity Frege system P versus NP problem Computer Science Applications Theoretical Computer Science Combinatorics Signal Processing Algorithm Information Systems Mathematics |
| Zdroj: | Information Processing Letters. 112:490-493 |
| ISSN: | 0020-0190 |
| DOI: | 10.1016/j.ipl.2012.03.009 |
| Popis: | 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 NP. Further we show how the soundness statements can be used to find hard satisfiable instances, if they exist. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|
Full Text from ScienceDirect