Towards NP-P via proof complexity and search (Q408544)

This article is a survey of proof complexity with particular emphasis on applications of proof complexity to proof search. The survey starts by providing background and some historical notes on proof systems and the P vs. NP question. It then discusses Cook's programme for separating NP and coNP and provides references to state-of-the-art lower bounds for the size of proofs. The next two sections are devoted to proof search and algorithmic consequences of proof complexity. The first item here is the efficient construction of proofs (automatizability) and current barriers towards that goal. Most proof systems are not automatizable (under suitable assumptions) and even to approximate the lengths of proofs is impossible (unless \(\mathrm{P}=\mathrm{NP}\)). The second item under the theme of proof search are relations to SAT solvers. In particular, modern algorithmic solving techniques (DPLL + clause learning) and their connections to subsystems of resolution are explained. The last two sections discuss general approaches for lower bounds (as proof complexity generators) and current barriers in this programme.