Seminar Logic, Complexity, Games: Propositional Proof Complexity
WS 2022/23
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  KickoffMeeting 
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 superpolynomially large resolution refutations. Since then, a lot of effort has gone into proving such superpolynomial 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 coNP. It is known that these classes are equal if and only if there exists a proof system that admits a polynomialsize refutation for every unsatisfiable formula. Thus, an approach to separate NP from coNP (and thereby also P from NP) is to try and show that no such proof system exists. This longterm 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 nonIsomorphism  [Toran13] 
Lower Bounds for SmallDepth 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 NPHard 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 twentyseventh annual ACM symposium on Theory of computing, pp. 575–584, 1995. 
[BPU92]  S. Bellantoni, T. Pitassi, and A. Urquhart. Approximation and SmallDepth 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 TwentyEighth 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 ConstantDepth 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 nonIsomorphism. 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ć