Do optimal proof systems exist? (guest post by Olaf Beyersdorff)

This post is a survey on optimal proof systems. I will not cover any results in detail, but try to present the general picture of what is known and what to expect.

A general proof system in the sense of Cook and Reckhow (1979) can be understood as a nondeterministic guess-and-verify algorithm. The question whether there exist optimal proof systems essentially asks whether there exists a best such verification procedure. For practical purposes, such an optimal proof system would be extremely useful, as both the search for good verification algorithms as well as the quest for lower bounds to the proof size could concentrate on the optimal system. Thus the following question is of great significance: Do there exist optimal proof systems for a given language $L$ ?

Formally, a proof system $P$ for $L$ is optimal, if for any proof $\pi$ of $x$ in any proof system for $L$ there exists a proof $\pi'$ of $x$ in the system $P$ that is at most polynomially longer than $\pi$ . If this transformation of $\pi$ into $\pi'$ can even be computed efficiently, then $P$ is called p-optimal. Currently, it is only known that all languages in NP have optimal proof systems and all languages in P even admit p-optimal proof systems. However, it is open whether there exist languages outside NP with optimal proof systems or outside P with p-optimal proof systems.

1. Characterizations

Of central interest is the question whether there exists an optimal proof system for the coNP complete set of classical propositional tautologies. This question was posed by Krajíček and Pudlák (1989). Understanding the question better through characterizations is an important line of research with connections to a number of different topics. The first result in this area is due to Krajíček and Pudlák (1989) who showed the equivalence between the existence of p-optimal proof systems for propositional tautologies and the existence of optimal acceptors (algorithms that are optimal on the positive instances) for this problem. This equivalence was generalized to other problems by Sadowski (1999) and Messner (1999). Beyersdorff, Köbler, and Messner (2009) showed that optimality implies p-optimality for any system and any language if and only if the natural proof system for SAT (where proofs are just satisfying assignments) is p-optimal; the existence of an optimal system would imply the existence of a p-optimal system if there is some p-optimal system for SAT.

Recently, Chen and Flum (2012) uncovered further surprising relations of optimal proof systems to descriptive complexity and parameterized complexity. The link between these fields is provided by studying listings, i.e., enumerations of machines that compute all easy subsets of intractable problems like TAUT. Through this link Chen and Flum relate optimal proof systems to the existence of bounded logics for complexity classes such as polynomial time as well as deterministic and nondeterministic logarithmic space.

2. Necessary and sufficient conditions

There are also interesting connections to core questions of complexity theory. As already mentioned, an optimal system for propositional tautologies would allow to reduce the NP vs coNP question to proving proof size bounds for just this optimal proof system. Optimal proof systems also imply the existence of complete problems for various promise complexity classes as disjoint NP pairs (Razborov 1994, Pudlák 2003, Glaßer et al. 2005, Beyersdorff 2007), NP $\cap$ coNP (Sadowski 1997) and probabilistic classes such as BPP (Köbler et al. 2003). Further to these implications, Itsykson (2010) has shown the surprising result that the average-case version of BPP has a complete problem.

Computational complexity also provides sufficient conditions for the existence of (p-)optimal proof systems; however, these are not as widely believed as structural assumptions like NP $\neq$ coNP. Krajíček and Pudlák (1989) showed that the existence of optimal (resp., p-optimal) propositional proof systems is implied by NE=coNE (resp., E=NE), and Köbler, Messner, and Torán (2003) weakened these assumptions to double exponential time.

3. Positive results in different models

Other recent research concentrated on modified versions of the problem, where a number of surprising positive results have been obtained. Cook and Krajíček (2007) showed that (p-)optimal proof systems for tautologies exist if we allow just one bit of non-uniform advice. This result generalizes to arbitrary languages (Beyersdorff et al. 2011), but does not translate into optimal algorithms or acceptors. Hirsch et al. (2012) showed that optimal acceptors exist in a heuristic setting where we have a probability distribution on the complement of the language, but it is open whether this translates into optimal heuristic proof systems. Still another positive result was obtained by Pitassi and Santhanam (2010) who show that there exists an optimal quantified propositional proof system under a weak notion of simulation.

4. Relations to bounded arithmetic

Another interesting relation is to weak first-order arithmetic theories, so-called bounded arithmetic. Propositional proof systems are known to enjoy a close relationship to suitable theories of bounded arithmetic, e.g. extended Frege systems EF correspond to the theory $S^1_2$ . This correspondence has two facets: 1) proofs of first-order statements in $S^1_2$ can be translated into polynomial-size EF proofs and 2) every proof system for which $S^1_2$ can prove the consistency is simulated by EF. Therefore, from the point of view of $S^1_2$ , there exists an optimal propositional proof system, namely EF. Likewise, from the point of view of $S^1_2$ , there exists a complete disjoint NP-pair (the canonical pair of EF) etc.

5. So, do they exist?

In general, the question whether optimal proof systems exist is wide open; however, most researchers seem to conjecture a negative answer. Confirming such a negative answer seems out of reach with current techniques as this would imply a separation of complexity classes. On the other hand, while a positive answer would have interesting consequences (optimal problems for promise classes), these would not be as dramatic as e.g. a collapse of the polynomial hierarchy and therefore would not seem to be in sharp conflict with beliefs of complexity theorists. Thus, we will probably not see the answer to the question soon; however, research on this topic will hopefully continue to uncover interesting connections between complexity and logic.

This entry was posted on October 2, 2014 at 2:57 am and is filed under Proof systems. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

Speedup in Computational Complexity