| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 429014 | Information Processing Letters | 2012 | 4 Pages |
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)Alg(P) of SAT algorithms determined by P . The class Alg(P)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)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 FdFd. Such results can be interpreted as a form of consistency of P≠NPP≠NP.Further we show how the soundness statements can be used to find hard satisfiable instances, if they exist.
► Lengths-of-proofs lower bounds yield formulas hard for SAT algorithms. ► Lower bounds for a proof system are a form of consistency of “P differs from NP”. ► The soundness statements for a SAT algorithm yield hard satisfiable formulas.
