Abstract

For every binary predicate $R$, there is a \emph{search problem} $Q_R$ for finding, given $x$, any $y$ such that $R(x,y)$ holds. $Q_R$ is said to be \emph{total} if every instance $x$ has a solution $y$, that is, $(\forall x)(\exists 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 $Q_R$ and the difficulty of proving the totality of $Q_R$ 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 proble m $Q_R$, 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 pro ve the first direct links between reducibilities among type-2 search problems an d lengths of propositional proofs. Based on this and the results on proposition al proof complexity, we obtain a number of relative separations among the so-cal led NP-search classes such as Polynomial Local Search ($\PLS$). Some of the rel ative separations we obtain are new.

Let $H$ be a QPC proof system and $j\geq 1$. We define the $\Sigma^q_j$-witnessing problem for $H$ to be: given an $H$-proof of a prenex $\Sigma^q_j$-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 $G_0$, and prove that the $\Sigma^q_1$-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 $VNC^1$ of bounded arithmetic, and show that the $\Sigma^B_1$-definable functions of $VNC^1$ are precisely the $NC^1$-functions. We describe simple translations of every $VNC^1$-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 $\Sigma^q_j$-witnessing problem for $H$ for various $H$ and $j\geq 1$.

Table of Contents

1. Introduction

2. Preliminaries

I Type-2 Search Problems

3. Type-2 Search Problems and Proof Complexity

4. The Limitations of Local Search Heuristics

II Quantified Propositional Calculus and Bounded Arithmetic

5. Quantified Propositional Calculus
 
6. The Witnessing Procedure for QPC

7. Second Order Theories of Bounded Arithmetic

8. Bounded Arithmetic and the Witnessing Problems for QPC

9. Concluding Remarks for Part II