Information

• Current information and course materials are available on our Moodle course page.

Organisation

The presentations will take place as a block seminar at the end of the semester.

• Language: you may choose between English and German
• Length of seminar paper: around 7 pages
• Duration of presentation: 25 minutes

Deadlines

18.10.2022	Kick-off-Meeting
09.12.2022	Ausarbeitung (erste Version)
23.01.2023	Ausarbeitung (finale Version)
20.02.2023	Folien
28.02.2023	Vorträge

Content

Propositional proof complexity is the study of syntactical logical proof systems and their power. Standard examples of such systems, that are introduced in the course "Mathematische Logik", are resolution and the sequent calculus. Such proof systems typically allow to prove the unsatisfiability of a given propositional formula by means of syntactic inference rules. For instance, the empty clause is derivable from a formula in conjunctive normal form using the resolution rule if and only if the original formula is unsatisfiable. Such a derivation of the empty clause is called a refutation of the formula. Now when we study the complexity of a proof system such as resolution, the questions that arise are of this kind:

Are there unsatisfiable formulas that have no short refutations? If so, how large is a shortest refutation in the worst case? Which proof systems admit efficient algorithms for computing refutations?

For resolution, the first two questions were answered in 1984 by Armin Haken, who proved that a propositional formulation of the pigeonhole principle only admits super-polynomially large resolution refutations. Since then, a lot of effort has gone into proving such super-polynomial lower bounds for more efficient proof systems as well. In this seminar, we will in particular also cover lower bounds for algebraic proof systems such as the Polynomial Calculus or the Cutting Planes proof system, which manipulate equations rather than logical formulas. Research in proof complexity is motivated by several aspects: First of all, it has a connection to practical computer science, as many SAT solvers are based on formal proof systems. Thus, lower bounds from proof complexity also imply lower bounds for certain SAT solvers, and conversely, the discovery of efficient proof systems can inspire new SAT solving algorithms.

In this seminar, however, the focus is mostly on the impact for theoretical computer science: Proof complexity can in principle help to solve the open question whether NP equals co-NP. It is known that these classes are equal if and only if there exists a proof system that admits a polynomial-size refutation for every unsatisfiable formula. Thus, an approach to separate NP from co-NP (and thereby also P from NP) is to try and show that no such proof system exists. This long-term goal is one of the reasons for the interest in lower bounds for the various proof systems.

Introductory Literature

We recommend the following survey article as an introduction to proof coplexity: [BP01]

Topics

Thema	Literatur
The Intractability of Resolution (a Lower Bound for the Pigeonhole Principle)	[Haken85]
On the Resolution Complexity of Graph non-Isomorphism	[Toran13]
Lower Bounds for Small-Depth Frege Proofs	[BPU92, Krajicek94]
Lower Bounds on Nullstellensatz Proofs via Designs	[Buss70]
Computing Polynomial Calculus Proofs with the Gröbner Basis Algorithm	[CEI96]
Lower Bounds for the Polynomial Calculus via the "Pigeon Dance"	[Razborov98]
Lower Bounds for Cutting Planes Proofs with Small Coefficients	[BPR95]
Hardness of Approximation for Finding Shortest Proofs	[ABMP01]
Circuit Complexity, Proof Complexity and Polynomial Identity Testing: The Ideal Proof System	[GP18]

Literature

[ABMP01]	M. Alekhnovich, S. Buss, S. Moran, and T. Pitassi. Minimum Propositional Proof Length is NP-Hard to Linearly Approximate. The Journal of Symbolic Logic, vol. 66(1), pp. 171–191, 2001.
[BP01]	P. Beame and T. Pitassi. Propositional Proof Complexity: Past, Present, and Future. In Current Trends in Theoretical Computer Science, Entering the 21th Century (G. Paun, G. Rozenberg, and A. Salomaa, Eds.), pp. 42–70. World Scientific, 2001.
[BPR95]	M. Bonet, T. Pitassi, and R. Raz. Lower Bounds for Cutting Planes Proofs with Small Coefficients. In Proceedings of the twenty-seventh annual ACM symposium on Theory of computing, pp. 575–584, 1995.
[BPU92]	S. Bellantoni, T. Pitassi, and A. Urquhart. Approximation and Small-Depth Frege Proofs. SIAM Journal on Computing, vol. 21(6), pp. 1161–1179, 1992.
[Buss70]	S. Buss. Lower Bounds on Nullstellensatz Proofs via Designs. , 1970.
[CEI96]	M. Clegg, J. Edmonds, and R. Impagliazzo. Using the Groebner basis algorithm to find proofs of unsatisfiability. In Proceedings of the Twenty-Eighth Annual ACM Symposium on Theory of Computing, pp. 174–183, 1996.
[GP18]	J. A. Grochow and T. Pitassi. Circuit Complexity, Proof Complexity, and Polynomial Identity Testing: The Ideal Proof System. Journal of the ACM (JACM), vol. 65(6), pp. 1–59, 2018.
[Haken85]	A. Haken. The intractability of resolution. Theoretical Computer Science, vol. 39, pp. 297–308, 1985.
[Krajicek94]	J. Krajíček. Lower Bounds to the Size of Constant-Depth Propositional Proofs. The Journal of Symbolic Logic, vol. 59(1), pp. 73–86, 1994.
[Razborov98]	A. A. Razborov. Lower Bounds for the Polynomial Calculus. computational complexity, vol. 7(4), pp. 291–324, 1998.
[Toran13]	J. Torán. On the Resolution Complexity of Graph non-Isomorphism. In International Conference on Theory and Applications of Satisfiability Testing, pp. 52–66, 2013.

Classification

• Informatik (B.Sc.)
• Mathematik (B.Sc.)
• Informatik (M.Sc.)
• Mathematik (M.Sc.)
• Grundlagen der Informatik (M.Sc.)
• Data Science (M.Sc.)
• Software Systems Engineering (M.Sc.)
• Media Informatics (M.Sc.)

Prerequisites

• Mathematical Logic
• for B.Sc. Computer Science: Module "Einführung in das wissenschaftliche Arbeiten (Proseminar)"

Contact

Erich Grädel, Benedikt Pago, Matthias Naaf, Lovro Mrkonjić