Olaf Beyersdorff surveys Optimal Proof Systems in the attached slides presented at the October 12-17, 2014 Dagstuhl Seminar on Optimal algorithms and proofs.

## Author Archive

### Optimal proof systems — a survey (slides by Olaf Beyersdorff)

October 16, 2014### On Some Conjectures in Proof Complexity (slides by Pavel Pudlák)

October 16, 2014Pavel Pudlák surveys open problems in Proof Complexity in the attached slides presented at the October 12-17, 2014 Dagstuhl Seminar on Optimal algorithms and proofs.

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

October 2, 2014This 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 ?

Formally, a proof system for is optimal, if for any proof of in any proof system for there exists a proof of in the system that is at most polynomially longer than . If this transformation of into can even be computed efficiently, then 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), NPcoNP (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 NPcoNP. 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 . This correspondence has two facets: 1) proofs of first-order statements in can be translated into polynomial-size EF proofs and 2) every proof system for which can prove the consistency is simulated by EF. Therefore, from the point of view of , there exists an optimal propositional proof system, namely EF. Likewise, from the point of view of , 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.

### Several Comments from Manuel Blum

September 13, 2012Dear Hunter — What a nice idea. And many of your examples below are both new to me and quite interesting. Thanks! And good luck! — manuel

…

While thinking about your blog, two things occurred to me that might be worth mentioning:

1. If a function f(x) has speedup, then any lower bound on its computation can be improved by a corresponding amount. For example, if every program for computing f(x) can be sped up to run twice as fast (on all but a finite number of integers), then any lower bound G(x) on its run time can be raised from G(x) to 2G(x) (on all but a finite number of integers). For another example, if any program for computing f(x) can be sped up by a sqrt (so that any run time F(x) can be reduced to a runtime of at most sqrt(F(x)), then any lower bound G(x)on its run time can be raised to [G(x)]^2, etc. This is all easy to see.

2. Much harder to see is a curious relation between speedup and inductive inference, which has to do with inferring an algorithm from observation of the sequence of integers that it generates. Theorem: there exists an inductive inference algorithm for inferring all sequences that have optimal algorithms (i.e. have programs that cannot be sped up)! This was quite a surprise (and a breakthrough) for me. Still is. To explain it though, I’d have to explain inductive inference, etc, and this would take me a bit of time. Some day…

Anyway, thanks again for your blog.

Best wishes and warm regards,

manuel (blum)

### Combinatorial problems related to matrix multiplication (guest post by Chris Umans)

September 10, 2012Determining the exponent of matrix multiplication, , is one of the most prominent open problems in algebraic complexity. Strassen famously showed that in 1969, and after a sequence of works culminating in work of Stothers and Williams the best current upper bound is . It is believed that indeed , meaning that there is a family of algorithms with running time for every . In this sense, if , matrix multiplication exhibits “speedup”: there is no single best asymptotic algorithm, only a sequence of algorithms having running times , with approaching . In fact Coppersmith and Winograd showed in 1982 that this phenomenon occurs whatever the true value of is (two, or larger than two), a result that is often summarized by saying “the exponent of matrix multiplication is an infimum, not a minimum.”

Despite the algebraic nature of the matrix multiplication problem, many of the suggested routes to proving are combinatorial. This post is about connections between one such combinatorial conjecture (the “Strong Uniquely Solvable Puzzle” conjecture of Cohn, Kleinberg, Szegedy and Umans) and some more well-known combinatorial conjectures. These results appear in this recent paper with Noga Alon and Amir Shpilka.

### The cap set conjecture, a strengthening, and a weakening

We start with a well-known, and stubborn, combinatorial problem, the “cap-set problem.” A cap-set in is a subset of vectors in with the property that no three vectors (not all the same) sum to 0. The best lower bound is due to Edel. Let us denote by the “cap set conjecture” the assertion that one can actually find sets of size . It appears that there is no strong consensus on whether this conjecture is true or false, but one thing that we do know is that it is a popular blog topic (see here, here, here, and the end of this post).

Now it happens that the only triples of elements of that sum to 0 are and — triples that are “all the same, or all different.” So the cap set conjecture can be rephrased as the conjecture that there are large subsets of vectors in so that for any in the set (not all equal), there is some coordinate such that are “not all the same, and not all different.” Generalizing from this interpretation, we arrive at a family of much stronger assertions, one for each : let’s denote by the “ conjecture” the assertion that there are subsets of vectors in , of size with the property that for any in the set (not all equal), there is some coordinate such that are “not all the same, and not all different.” Such sets of size in imply size -size sets of this type in by viewing each symbol in as a block of symbols in , so the conjecture is stronger (i.e. it implies the cap-set conjecture). Indeed, if you play around with constructions you can see that as gets larger it seems harder and harder to have large sets avoiding triples of vectors for which every coordinate has “all different.” Thus one would probably guess that the conjecture is false.

One of the results in our paper is that the conjecture is in fact *equivalent* to falsifying the following well-known sunflower conjecture of Erdos-Szemeredi: there exists an such that any family of at least subsets of contains a 3-sunflower (i.e., three sets whose pairwise intersections are all equal).

So the intuition that the conjecture is false agrees with Erdos and Szemeredi’s intuition, which is a good sign.

Now let’s return to the cap-set conjecture in . Being a cap set is a condition on *all* triples of vectors in the set. If one restricts to a condition on only some of the triples of vectors, then a construction becomes potentially easier. We will be interested in a “multicolored” version in which vectors in the set are assigned one of three colors (say red, blue, green), and we only require that no triple of vectors sums to 0 with being red, being blue, and being green. But a moment’s thought reveals that the problem has become too easy: one can take (say) the red vectors to be all vectors beginning with , the green vectors to be all vectors beginning with , and the the blue vectors to be all vectors beginning with . A solution that seems to recover the original flavor of the problem, is to insist that the vectors come from a collection of red, green, blue triples with ; we then require that every red, green, blue triple *except those in the original collection* not sum to 0. So, let’s denote by the “multicolored cap-set conjecture” the assertion that there are subsets of *triples of vectors* from of size , with each triple summing to 0, and with the property that for any three triples in the set (not all equal), .

If is a cap set in , then the collection of triples constitutes a multicolored cap-set of the same size, so the multicolored version of the conjecture is indeed weaker (i.e. it is implied by the cap-set conjecture).

### A matrix multiplication conjecture between the two

The SUSP conjecture of Cohn, Kleinberg, Szegedy, and Umans is the following: there exist subsets of *triples of vectors* from of size , with each triple summing (in the integers) to the all-ones vector, and with the property that for any three triples in the set (not all equal), there is a coordinate such that .

The mysterious constant comes from the fact , and it is easy to see that one cannot have multiple triples with the same “ vector” (or , or …). More specifically, “most” triples that sum to the all-ones vector are balanced (meaning that each have weight ), and there can be at most balanced triples, without repeating an vector. So the conjecture is that there are actually subsets satisfying the requirements, whose sizes approach this easy upper bound.

If in the statement of the SUSP conjecture, one replaces “there is a coordinate such that ” with “there is a coordinate such that ” one gets the weaker “Uniquely Solvable Puzzle” conjecture instead of the “Strong Uniquely Solvable Puzzle” conjecture. Here one is supposed to interpret the triples as triples of “puzzle pieces” that fit together (i.e. their 1’s exactly cover the coordinates without overlap); the main requirement then ensures that no other way of “assembling the puzzle” fits together in this way, thus it is “uniquely solvable.” It is a consequence of the famous Coppersmith-Winograd paper that the Uniquely Solvable Puzzle conjecture is indeed true. Cohn, Kleinberg, Szegedy and Umans showed that if the stronger SUSP conjecture is true, then .

Two of the main results in our paper are that (1) the conjecture implies the SUSP conjecture, and (2) the SUSP conjecture implies the multicolored cap-set conjecture.

So by (1), *disproving the SUSP* conjecture is as hard as proving the Erdos-Szemeredi conjecture (which recall is equivalent to disproving the conjecture). Of course we hope the SUSP conjecture is true, but if it is not, it appears that will be difficult to prove.

And by (2), proving the SUSP conjecture entails proving the multicolored cap-set conjecture. So apart from being a meaningful weakening of the famous cap-set conjecture in , the multicolored cap-set conjecture can be seen as a “warm-up” to (hopefully) proving the SUSP conjecture and establishing . As a start, we show in our paper a lower bound of for multicolored cap-sets, which beats the lower bound of Edel for ordinary cap sets.

Returning to “speedup,” the topic of this blog, notice that the SUSP conjecture, as well as the cap-set, the multicolored cap-set, and the conjectures, all assert that there exist sets of size with certain properties, for various constants . In all cases is easily ruled out, and so all one can hope for is a sequence of sets, one for each , whose sizes approach as grows. If the SUSP conjecture is true, then it is this sequence of sets that directly corresponds to a sequence of matrix multiplication algorithms with running times for approaching . This would then be a concrete manifestation of the “speedup” phenomenon for matrix multiplication.

### Speedup in Computational Complexity

September 10, 2012Welcome to this new blog aimed at promoting discussion of speedup for natural computational problems, that is, the question in computational complexity of whether a problem has a best algorithm. The intention is to have a series of guest posts by researchers in the field and to provide a shared, user maintained bibliography of work on the topic.

I believe this blog is necessary because the topic is interesting and underappreciated. It is a fundamental property of a computational problem as to whether it does or does not have an optimal algorithm. While a few classic results on speedup versus optimality are widely known, such as Blum’s speedup for artificially constructed languages and Levin’s optimal NP search algorithm, other key results on speedup for natural problems are not familiar. For instance, there is no best Strassen-style bilinear identity for matrix multiplication. The existence of efficient algorithms for MM is linked to key problems in combinatorics such as the Erdos-Rado sunflower conjecture (see Alon et al) and efforts to lower the MM exponent have recently resumed. Curiously, four of the five problems with a gap between their monotone and nonmonotone circuit complexity rely upon integer or matrix multiplication, which are conjectured to have speedup. As another example, Stockmeyer’s PhD thesis presented a result on speedup for natural problems that had been virtually forgotten. It has also been established that if there is an infinitely often (i.o.) superpolynomial speedup for the time required to accept any (paddable) coNP-complete language, then all (paddable) coNP-complete languages have this speedup, which is equivalent to a superpolynomial speedup in proof length in propositional proof systems for tautologies.

I have argued that there is a correspondence between the properties “has no algorithm at all” and “has no best algorithm” by demonstrating that a resource-bounded version of the statement “no algorithm recognizes all non-halting Turing machines” is equivalent to an infinitely often (i.o.) superpolynomial speedup for the time required to accept any (paddable) coNP-complete language. A literature review on speedup can be found here.

Please feel free to contribute by commenting on blog posts or adding papers to the shared bibliography and also let me know if you would like to make a guest post on a topic of general interest or on your latest research.

Hunter Monroe