For every binary predicate R, there is a search problem QR for finding, given x, any y such that R(x, y) holds. QR is said to be total if every instance x has a solution y, that is, (∀x)(∃y)R( x, y) holds. Total search problems are commonplace in computer science, and studying their complexity is therefore an important endeavour. In this dissertation, we present links between the complexity of solving QR and the difficulty of proving the totality of QR in the three logical formalisms: propositional calculus, quantified propositional calculus (QPC), and theories of bounded arithmetic. These links allow logical approaches to the complexity of search problems.; We show several links between the complexity of a type-2 total search problem QR, where R is represented by a first-order existential sentence phi, and the lengths of proofs of the propositional translations of phi in bounded-depth Frege systems and the Nullstellensatz proof system. In particular, we prove the first direct links between reducibilities among type-2 search problems and lengths of propositional proofs. Based on this and the results on propositional proof complexity, we obtain a number of relative separations among the so-called NP-search classes such as Polynomial Local Search (PLS). Some of the relative separations we obtain are new.; Let H be a QPC proof system and j ≥ 1. We define the Sqj -witnessing problem for H to be: given an H-proof of a prenex Sqj -formula A, and a truth assignment to the free variables of A, find a witness for the outermost existential quantifiers of A. These witnessing problems provide a tangible link between the proof lengths in QPC and the complexity of search problems, and we consider them for various parameters. We also introduce and study the new QPC proof systems G*0 and G0, and prove that the Sq1 -witnessing problem for each is complete for NC 1-search problems. Our proof involves proving the TC 0-versions of Gentzen's midsequent theorem and Herbrand's theorem.; We introduce a second-order theory VNC1 of bounded arithmetic, and show that the SB1 -definable functions of VNC1 are precisely the NC1-functions. We describe simple translations of every VNC1-proof into a family of polynomial-size G*0 -proofs. From this and similar translation theorems for other bounded arithmetic theories, we obtain the hardness of the Sqj -witnessing problem for H for various H and j ≥ 1.
展开▼
