Proofs, circuits, and total search problems
Many recent results in both propositional proof complexity and boolean circuit complexity have been enabled, either directly or indirectly, by a deeper understanding of proofs and circuits as a consequence of viewing them through the lens of total search problems, and by the development of query-to-communication lifting theorems, which show that in certain scenarios query complexity lower bounds can be “lifted” to communication lower bounds. Such results include explicit strongly exponential lower bounds on monotone formula complexity, separations between the mon−ACi and the mon−NCi hierarchies, new techniques for proving lower bounds on the size of monotone circuits and of cutting planes proofs, exponential lower bounds on the size of cutting planes proofs for random CNF formulas, the resolution of the Alon-Saks-Seymour problem, and many others.
This talk will focus on characterizations of proofs and circuits using the theory of total search problems (TFNP), expanding on classical results in complexity theory such as the characterization of circuit depth by Karchmer-Wigderson games, and the equivalence between tree-like Resolution and decision trees. We will also discuss how lifting theorems and feasible interpolation provide a connection between the query and communication complexity of certain search problems, and how this perspective suggests a whole program for further research.
This document was translated from LATEX by HEVEA.