## CMSC 39600-1: Propositional Proof Complexity (Topics in Theoretical Computer Science)

Course description

Winter09: Tuesday, Thursday 4:30pm-5:50pm (Ry 276)
• Office hours. For the time being, just drop by when I am in.
• Lecture notes are downloadable as a single PDF file (or TeX source if for any reasons you need individual lectures). Any comments, corrections and suggestions are most welcome.
• Questions for self-study (aka "homeworks").
• Open problems. The expected complexity of problems on this list varies from just hard to extremely hard. I, however, am avoiding here anything that is believed to be inaccessible with current methods.

1. For every $k>0$ there exists a $\Sigma_1^b(\alpha)$ formula $A$ such that $T_2^k(\alpha)\vdash A$ whereas $S_2^k(\alpha)\not\vdash A$ (see e.g. [18, Problem 6]; this source also contains a discussion of candidate $A$s).
2. For a fixed formula $A(x)$ (not necessarily bounded), define the hierarchy $\Sigma_k^b(A),\Pi_k^b(A)$ similarly to $\Sigma_k^b,\Pi_k^b$ but allowing one extra clause: every formula of the form $A(t)$ ($t$ any term) belongs to $\Sigma_0^b(A)\cup \Pi_0^b(A)$. The theories $S_2^k(A), T_2^k(A)$ are defined respectively. Does there exist a specific formula $A$ such that $S_2(A)$ is not finitely axiomatizable (or at least such that $S_2^1(A)\neq T_2^1(A)$)?
This problem has developed from a question asked in the class. An affirmative answer clearly implies that $S_2(\alpha)$ is not finitely axiomatizable, and an intended approach to this problem would be to try to take as $A$ an arithmetic definition of an oracle separating levels of the polynomial hierarchy.
3. Does $Res(2)$ have Feasible Interpolation Property (for the negative answer you can use any reasonable complexity assumption)?
4. The Existential Interpolation Property for a proof system $f$ means that whenever $A(x)\lor B(y)$ has an $f$-proof of size $s$ then either $A(x)$ or $B(y)$ has an $f$-proof of size polynomial in $s$.
Does the (Extended) Frege proof system possess EIP (again, modulo any reasonable complexity assumption in case of negative anwer)?
5. Is the resolution proof system quasi-automatizable (again, modulo assumptions)? (See e.g. .)
6. Let $\Delta$ be any fixed constant. Prove that with probability $1-o(1)$ a random CNF that has $n$ variables and $\Delta n$ clauses does not posses an $F_2$ (depth-2 Frege) refutation of polynomial size.
7. Does $onto-FPHP^\infty_n$ have a polynomial size bounded-depth Frege proof? ([17, Problem 2]; quasi-polynomial bounds are known.)
8. Does $onto-FPHP^\infty_n$ have a quasi-polynomial size $Res(t)$ proof for any constant $t$? ([17, Problems 3,4]; this is true if $t$ is allowed to grow polylogarithhmically in $n$).
9. We know that the minimal size of a resolution refutation of $onto-FPHP^\infty_n$ behaves as $\exp(n^{\epsilon})$, where $\epsilon\in [1/3,1/2]$. Determine the right value of $\epsilon$. ([17, Problem 5].)
10. Prove superpolynomial lower bounds for the system $F_d[p]$ ($p$ a prime), that is bounded-depth Frege augmented with counting connectives $MOD_p$ [18, Problem 10].
11. Find a "direct" proof of superpolynomial lower bounds for the Cutting Planes proof system.
12. Prove superpolynomial lower bounds for the DAG version of the Lovasz-Schrijver proof system $LS$.
13. Prove superlogarithmic lower bounds on the refutation rank for the system $LS_{\ast}$ that extends Lovasz-Schrijver by allowing the full power of the rule $f\geq 0, g\geq 0 \Longrightarrow fg\geq 0$, $f,g$ arbitrary linear forms. Precise definitions can be found in ; this paper also proves an $\Omega(\log n)$ bound.
14. Prove that there exist Nisan generators stretching $n$ bits to $2^{n^\epsilon}$ bits that are hard for Resolution. All definitions can be found in  (you can use any of the encodings described there), and it solves this problem for Resolution width. The best we can do at the moment in terms of Resolution size is $n^{3-\epsilon}$ bits .
• Literature. Unfortunately, I am not aware of any single "canonical" source that would comfortably cover all the material in our course. Recommended literature for its different portions will be posted on this page as we go along.

One good starting point might be the survey paper  by Nate Segerlind. It is (to the best of my knowledge) the most recent writing on the subject, it contains a comprehensive list of literature, and it includes recommendations for further reading, specifically indicating the topics where other surveys offer a different perspective.

The only drawback of the survey  by Paul Beame and Toni Pitassi is that it is a little bit outdated. Due to natural limitations, lecture notes  by Paul Beame are not intended to be comprehensive. But if a topic is covered there, this is usually also one of the best expositions.

• Plans and progress. This course will consist of two parts: Bounded Arithmetic (Part I) and propositional proof complexity proper (Part II), with a significant accent on the latter (see also course description). While these two topics are well related ideologically, their intersection in terms of concepts and techniques is surprisingly small. This makes the two parts of our course practically independent.

Research on Bounded Arithmetic heavily uses standard machinery from mathematical logic (Gentzen-style calculus, cut elimination, Herbrand theorem etc.), while much of the propositional proof complexity is based upon combinatorial and algebraic techniques parallel to those employed in the circuit complexity and similar disciplines. It is not totally inconceivable that a certain part of the audience has developed a much better taste to the techniques of the second (combinatorial) kind. And, as a courtesy to these listeners, after a word (well, actually a few words) of introduction on January 6, and before immersing into the logical formalism for a few weeks, we will do preview of a sort. Namely, we will prove right away one basic result from the propositional part of the course known as width-size tradeoff for resolution (with applications). Our exposition will follow, more or less closely, the original paper ; this material is also covered in [1,3].

Several lectures in the second part will be devoted to outreach activity, that is, important by-products of research in the propositional proof complexity. We will certainly cover applications to:

1. integrality gaps of various LP/SDP relaxation procedures for integral programming (see [5,6] and extended follow-up literature);
2. learning theory .
• On January 8 I hope to finish our "preview", and the course will begin its systematic development. We will start doing Bounded Arithmetic (with many technical proofs omitted), and at this simple level we will hardly need much more than the original monograph . Motivated listeners can also consult more advanced sources  and [10, Chapter 5].

Well, after all we will cover (or at least mention) on January 20 some of more modern material. The original papers are [11,12] (RSUV-isomorphism),  (Ferreira's version of Bounded Arithmetic),  (conditional collapse of the BA hierarchy) and [15,16] (more witnessing theorems). For January 22:  (survey on the complexity of the pigeonhole principle) and  (specifically covers the transition from Bounded Arithmetic to the propositional world).

On January 27 we will begin doing our first block in Propositional Proof Complexity: Interpolation, Automatizability and Applications to Learning. Some of the original references are [20--25].

On February 17 we will begin a new topic: Complexity of the Pigeon-Hole-Principle. See  for a comprehensive survey; our proof of lower bounds for constant-depth Frege follows (more or less closely) .

On February 24 we will proceed to our next large block: Algebraic and Geometric Models. The best source I am aware of that nicely covers algebraic models (notably, Nullstellensatz and Polynomial Calculus) is . For a catalogue of geometric systems see , and the original sources for Cutting Planes lower bounds are [28,29]. The lower bound on the LS rank is from .

And on March 10 we will begin wrapping this course up with our last topic, Independence of Circuit Lower Bounds and Pseudorandom Generators. See Introduction in . The reduction to the Pigeon Hole Principle is from [32, Section 4].

### References

1. N. Segerlind, The complexity of propositional proofs, The Bulletin of Symbolic Logic, volume 13, number 4, pages 482-537, 2007.
2. P. Beame, T. Pitassi, Propositional proof complexity: Past, present, and future, Current trends in theoretical computer science: Entering the 21st century , World Scientific Publishing, 2001, pp. 42–70. Available at Beame's home page.
3. P. Beame, Proof complexity, Computational Complexity Theory, volume 10 of IAS/Park City mathematics series, pages 199-246. American Mathematical Society, 2004. Available at Beame's home page.
4. E. Ben-Sasson, A. Wigderson, Short Proofs Are Narrow—Resolution Made Simple, Journal of the ACM, Vol. 48, No. 2, March 2001, pp. 149 –169.
5. J. Buresh-Oppenheim, N. Galesi, S. Hoory, A. Magen and T. Pitassi, Rank Bounds and Integrality Gaps for Cutting Planes Procedures, Theory of Computing, volume 2, 2006, pp. 65-90.
6. S. Arora, B. Bollobas, L. Lovasz, I. Tourlakis, Proving integrality gaps without knowing the linear program, Theory of Computing, Vol. 2, p. 19-51, 2006
7. M. Alekhnovich, M. Braverman, V. Feldman, A. R. Klivans, T. Pitassi, Learnability and automatizability, Proceedings of the 45th Annual IEEE Symposium on Foundations of Computer Science, 2004, pages 621 - 630.
8. S. Buss, Bounded Arithmetic, Napoli : Bibliopolis, 1986, 221 p. Available at Buss's home page.
9. J. Krajicek, Bounded arithmetic, propositional logic, and complexity theory, Cambridge University Press, 1995.
10. P. Hajek, P. Pudlak, Metamathematics of first-order arithmetic, Springer-Verlag, 1993.
11. G. Takeuti, RSUV isomorphism, Arithmetic, Proof Theory and Computational Complexity, eds. P. Clote and J. Krajicek, Oxford University Press, 1993, pages 364-386
12. A. Razborov, An equivalence between second order bounded domain bounded arithmetic and first order bounded arithmetic, Arithmetic, Proof Theory and Computational Complexity, eds. P. Clote and J. Krajicek, Oxford University Press, 1993, pages 247-277
13. F. Ferreira, Polynomial time computable arithmetic and conservative extensions, Ph.D., The Pennsylvania State University, 1988, 176 pages
14. J. Krajícek, P. Pudlak, G. Takeuti, Bounded Arithmetic and the Polynomial Hierarchy, Ann. Pure Appl. Logic, 1991, 52(1-2): 143-153
15. S. Buss, J. Krajicek, An application of Boolean complexity to separation problems in Bounded arithmetic, Proceedings of the London Mathematical Society, 69(1994), pages 1-21
16. A. Beckmann, S. Buss, Polynomial Local Search in the Polynomial Hierarchy and Witnessing in Fragments of Bounded Arithmetic, 2008, preprint downloadable from Buss's home page
17. A. Razborov, Proof Complexity of Pigeonhole Principles, in Proceedings of the 5th Developments in Language Theory Conference, Lecture Notes in Computer Science, vol. 2295, 2002, pages 100-116.
18. P. Pudlak, Twelve problems in proof complexity, Proc. 3rd International Computer Science Symposyum in Russia, CSR 2008, LNCS 5010, pp.13-27.
19. S. Buss, Bounded Arithmetic and Propositional Proof Complexity, in Logic of Computation, edited by H. Schwichtenberg. Springer-Verlag, Berlin, 1997, pp. 67-122.
20. A. Razborov, On Provably Disjoint NP-pairs, Basic Research in Computer Science Center, 1994.
21. J. Krajicek, P. Pudlak, Some consequences of cryptographical conjectures for S_2^1 and EF, Information and Computation, vol. 140 (1998), no. 1, pp. 82-94.
22. M. Alekhnovich, A. Razborov, Resolution Is Not Automatizable Unless W[P] Is Tractable, SIAM J. Comput. 38(4): 1347-1363 (2008)
23. M. Alekhnovich, M. Braverman, V. Feldman, A. Klivans, T. Pitassi, The complexity of properly learning simple concept classes, J. Comput. Syst. Sci., 74(1): 16-34 (2008).
24. M. Alekhnovich, A. Razborov, Satisfiability, Branch-Width and Tseitin Tautologies, Proc. of the 43rd IEEE FOCS, 2002, pages 593-603.
25. K. Eickmeyer, M. Grohe, M. Grüber, Approximation of natural W[P]-complete minimisation problems is hard, Proceedings of the 23rd IEEE Conference on Computational Complexity (CCC'08), pp.8-18, 2008.
26. P. Beame, S. Riis, More on the relative strength of counting principles, In Paul W. Beame and Samuel R. Buss, editors, Proof Complexity and Feasible Arithmetics, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 13-35. American Mathematical Society, 1998.
27. D. Grigoriev, E. Hirsch, D.Pasechnik, Complexity of semi-algebraic proofs, Moscow Mathematical Journal, 2(4): 647-679, 2002.
28. Bonet, M., Pitassi, T. and Raz, R., Lower bounds for Cutting Planes proofs with small coefficients, Journal of Symbolic Logic, Vol. 62, No. 3, pp. 708-728, 1997.
29. P. Pudlak, Lower bounds for resolution and cutting planes proofs and monotone computations, J. of Symb. Logic, 62(3), 1997, pp.981-998.
30. J. Buresh-Oppenheim, N. Galesi, S. Hoory, A. Magen, T. Pitassi, Rank Bounds and Integrality Gaps for Cutting Planes Procedures, Theory of Computing, Volume 2 (2006), Article 4, pp. 65-90.
31. A. Razborov, Pseudorandom Generators Hard for k-DNF Resolution and Polynomial Calculus Resolution, manuscript. Available at my home page.
32. A. Razborov, Resolution Lower Bounds for Perfect Matching Principles, Journal of Computer and System Sciences, Vol. 69, No 1, 2004, pages 3-27.
33. M. Alekhnovich, E. Ben-Sasson, A. Razborov, A. Wigderson, Pseudorandom Generators in Propositional Proof Complexity, SIAM Journal on Computing, Vol. 34, No 1, 2004, pages 67-88.
34. J. Krajicek, Dual weak pigeonhole principle, pseudo-surjective functions, and provability of circuit lower bounds, J. of Symbolic Logic, 69(1), (2004), pp.265-286.