Title:
On the relationship between the complexity of total search problems and the hardness of proving their totality

Abstract:
A search problem Q is defined by a binary relation R in the following way: given x, find y such that R(x,y) holds. Q is said to be total if for every x there is y with R(x,y). Total search problems are commonplace in computer science and mathematics: examples include optimization problems such as the problem of finding a Traveling Salesman tour that is locally optimal with respect to the 2-OPT heuristic, and the problems in game theory such as the problem of finding a Nash equilibrium given payoff matrices for two players.

For a total search problem Q, we associate a combinatorial principle F that asserts the totality of Q. In this talk, we show several new connections between the complexity of Q and the hardness of proving F in the following three logical formalisms: propositional logic, quantified propositional logic, and theories of bounded arithmetic. Thus, studying the logical properties of F sheds light on the complexity of Q, and vice versa.

The main result of this talk is the first explicit connection between the complexity of Q and the length of proofs of propositional translations of F. By utilizing a number of lower bounds obtained in proof complexity research, we are able to obtain relative separations among classes of search problems, some of which have been previously unknown. We also show a simple condition C such that, if Q satisfies C, then Q cannot be solved using local search heuristics in a relativized world.

We also define a class of new search problems: the witnessing problems for quantified propositional logic (QPC). QPC is known to be closely connected to bounded arithmetic and the polynomial-time hierarchy. We briefly describe the relationship among search problems, QPC, and bounded arithmetic, and state our contributions in making further connections.

This talk is based on two joint works: one with Joshua Buresh-Oppenheim and another with Stephen Cook.