Proof Complexity of Natural Formulas via Communication Arguments

Authors Dmitry Itsykson , Artur Riazanov

Thumbnail PDF


  • Filesize: 1.05 MB
  • 34 pages

Document Identifiers

Author Details

Dmitry Itsykson
  • St. Petersburg Department of Steklov Mathematical Institute of, Russian Academy of Sciences, Russia
Artur Riazanov
  • St. Petersburg Department of Steklov Mathematical Institute of, Russian Academy of Sciences, Russia


The authors are grateful to Anastasia Sofronova, Svyatoslav Gryaznov, Danil Sagunov, Petr Smirnov, Dmitry Sokolov, and Jakob Nordström for fruitful discussions and useful comments. We also thank the anonymous referees for useful comments and corrections. Dmitry Itsykson is a Young Russian Mathematics award winner and would like to thank sponsors and jury of the contest.

Cite AsGet BibTex

Dmitry Itsykson and Artur Riazanov. Proof Complexity of Natural Formulas via Communication Arguments. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 3:1-3:34, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


A canonical communication problem Search(φ) is defined for every unsatisfiable CNF φ: an assignment to the variables of φ is partitioned among the communicating parties, they are to find a clause of φ falsified by this assignment. Lower bounds on the randomized k-party communication complexity of Search(φ) in the number-on-forehead (NOF) model imply tree-size lower bounds, rank lower bounds, and size-space tradeoffs for the formula φ in the semantic proof system T^{cc}(k,c) that operates with proof lines that can be computed by k-party randomized communication protocol using at most c bits of communication [Göös and Pitassi, 2014]. All known lower bounds on Search(φ) (e.g. [Beame et al., 2007; Göös and Pitassi, 2014; Russell Impagliazzo et al., 1994]) are realized on ad-hoc formulas φ (i.e. they were introduced specifically for these lower bounds). We introduce a new communication complexity approach that allows establishing proof complexity lower bounds for natural formulas. First, we demonstrate our approach for two-party communication and apply it to the proof system Res(⊕) that operates with disjunctions of linear equalities over 𝔽₂ [Dmitry Itsykson and Dmitry Sokolov, 2014]. Let a formula PM_G encode that a graph G has a perfect matching. If G has an odd number of vertices, then PM_G has a tree-like Res(⊕)-refutation of a polynomial-size [Dmitry Itsykson and Dmitry Sokolov, 2014]. It was unknown whether this is the case for graphs with an even number of vertices. Using our approach we resolve this question and show a lower bound 2^{Ω(n)} on size of tree-like Res(⊕)-refutations of PM_{K_{n+2,n}}. Then we apply our approach for k-party communication complexity in the NOF model and obtain a Ω(1/k 2^{n/2k - 3k/2}) lower bound on the randomized k-party communication complexity of Search(BPHP^{M}_{2ⁿ}) w.r.t. to some natural partition of the variables, where BPHP^{M}_{2ⁿ} is the bit pigeonhole principle and M = 2ⁿ+2^{n(1-1/k)}. In particular, our result implies that the bit pigeonhole requires exponential tree-like Th(k) proofs, where Th(k) is the semantic proof system operating with polynomial inequalities of degree at most k and k = 𝒪(log^{1-ε} n) for some ε > 0. We also show that BPHP^{2ⁿ+1}_{2ⁿ} superpolynomially separates tree-like Th(log^{1-ε} m) from tree-like Th(log m), where m is the number of variables in the refuted formula.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Theory of computation → Communication complexity
  • bit pigeonhole principle
  • disjointness
  • multiparty communication complexity
  • perfect matching
  • proof complexity
  • randomized communication complexity
  • Resolution over linear equations
  • tree-like proofs


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Paul Beame, Toniann Pitassi, and Nathan Segerlind. Lower bounds for Lovász-Schrijver systems and beyond follow from multiparty communication complexity. SIAM J. Comput., 37(3):845–869, 2007. Google Scholar
  2. Paul Beame and Søren Riis. More on the relative strength of counting principles. In Paul Beam and Samuel R. Buss, editors, Proof Complexity and Feasible Arithmetics, Proceedings of a DIMACS Workshop, New Brunswick, New Jersey, USA, April 21-24, 1996, volume 39 of DIMACS Series in Discrete Mathematics and Theoretical Computer Science, pages 13-35. DIMACS/AMS, 1996. URL:
  3. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. The Journal of Symbolic Logic, 44(1):36-50, 1979. Google Scholar
  4. William Cook, Collette R. Coullard, and Gy. Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. Google Scholar
  5. Stefan S. Dantchev, Nicola Galesi, and Barnaby Martin. Resolution and the binary encoding of combinatorial principles. In Amir Shpilka, editor, 34th Computational Complexity Conference, CCC 2019, July 18-20, 2019, New Brunswick, NJ, USA, volume 137 of LIPIcs, pages 6:1-6:25. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. URL:
  6. Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random Θ(log n)-CNFs are hard for cutting planes. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 109-120. IEEE Computer Society, 2017. URL:
  7. Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov. Monotone circuit lower bounds from resolution. In Ilias Diakonikolas, David Kempe, and Monika Henzinger, editors, Proceedings of the 50th Annual ACM SIGACT Symposium on Theory of Computing, STOC 2018, Los Angeles, CA, USA, June 25-29, 2018, pages 902-911. ACM, 2018. URL:
  8. Michal Garlík and Leszek Aleksander Kolodziejczyk. Some subsystems of constant-depth frege with parity. ACM Trans. Comput. Log., 19(4):29:1-29:34, 2018. URL:
  9. Mika Göös and Toniann Pitassi. Communication lower bounds via critical block sensitivity. In Proceedings of the Forty-Sixth Annual ACM Symposium on Theory of Computing, STOC ’14, page 847–856, New York, NY, USA, 2014. Association for Computing Machinery. URL:
  10. Pavel Hrubes and Pavel Pudlák. Random formulas, monotone circuits, and interpolation. In Chris Umans, editor, 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 121-131. IEEE Computer Society, 2017. URL:
  11. Pavel Hrubes and Pavel Pudlák. A note on monotone real circuits. Inf. Process. Lett., 131:15-19, 2018. URL:
  12. Trinh Huynh and Jakob Nordström. On the virtue of succinct proofs: amplifying communication complexity hardness to time-space trade-offs in proof complexity. In Howard J. Karloff and Toniann Pitassi, editors, Proceedings of the 44th Symposium on Theory of Computing Conference, STOC 2012, New York, NY, USA, May 19 - 22, 2012, pages 233-248. ACM, 2012. URL:
  13. Russell Impagliazzo, Toniann Pitassi, and Alasdair Urquhart. Upper and lower bounds for tree-like cutting planes proofs. In Proceedings of the Ninth Annual Symposium on Logic in Computer Science (LICS '94), Paris, France, July 4-7, 1994, pages 220-228. IEEE Computer Society, 1994. URL:
  14. Dmitry Itsykson and Dmitry Sokolov. Lower bounds for splittings by linear combinations. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Computer Science 2014 - 39th International Symposium, MFCS 2014, Budapest, Hungary, August 25-29, 2014. Proceedings, Part II, volume 8635 of Lecture Notes in Computer Science, pages 372-383. Springer, 2014. URL:
  15. Dmitry Itsykson and Dmitry Sokolov. Resolution over linear equations modulo two. Annals of Pure and Applied Logic, 171(1), January 2020. URL:
  16. Bala Kalyanasundaram and Georg Schnitger. The probabilistic communication complexity of set intersection. SIAM J. Discret. Math., 5(4):545-557, 1992. URL:
  17. Mauricio Karchmer and Avi Wigderson. Monotone circuits for connectivity require super-logarithmic depth. SIAM J. Discret. Math., 3(2):255-265, 1990. URL:
  18. H. Kesten. An introduction to probability theory and its applications, volume i, (william feller). SIAM Review, 11(1):96-96, 1969. URL:
  19. Erfan Khaniki. On proof complexity of resolution over polynomial calculus. Electronic Colloquium on Computational Complexity (ECCC), 27:34, 2020. URL:
  20. Jan Krajíček. Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic. J. Symb. Log., 62(2):457-486, 1997. URL:
  21. Jan Krajíček. An exponential lower bound for a constraint propagation proof system based on ordered binary decision diagrams. J. Symb. Log., 73(1):227-237, 2008. URL:
  22. Jan Krajíček. Randomized feasible interpolation and monotone circuits with a local oracle. J. Mathematical Logic, 18(2):1850012:1-1850012:27, 2018. URL:
  23. Jan Krajíček. Proof complexity, volume 170. Cambridge University Press, 2019. Google Scholar
  24. Eyal Kushilevitz and Noam Nisan. Communication complexity. Cambridge University Press, 1997. Google Scholar
  25. Edward I Nechiporuk. A boolean function. Engl. transl. in Sov. Phys. Dokl., 10:591-593, 1966. Google Scholar
  26. Vsevolod Oparin. Tight upper bound on splitting by linear combinations for pigeonhole principle. In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satisfiability Testing - SAT 2016 - 19th International Conference, Bordeaux, France, July 5-8, 2016, Proceedings, volume 9710 of Lecture Notes in Computer Science, pages 77-84. Springer, 2016. URL:
  27. Fedor Part and Iddo Tzameret. Resolution with counting: Dag-like lower bounds and different moduli. In Thomas Vidick, editor, 11th Innovations in Theoretical Computer Science Conference, ITCS 2020, January 12-14, 2020, Seattle, Washington, USA, volume 151 of LIPIcs, pages 19:1-19:37. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL:
  28. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. URL:
  29. Ran Raz and Pierre McKenzie. Separation of the monotone NC hierarchy. Combinatorica, 19(3):403-435, 1999. URL:
  30. Ran Raz and Avi Wigderson. Monotone circuits for matching require linear depth. J. ACM, 39(3):736–744, 1992. URL:
  31. Alexander A. Sherstov. The multiparty communication complexity of set disjointness. In Proceedings of the forty-fourth annual ACM symposium on Theory of computing, pages 525-548, 2012. Google Scholar
  32. Alexander A. Sherstov. Communication lower bounds using directional derivatives. J. ACM, 61(6), December 2014. URL:
  33. Dmitry Sokolov. Dag-like communication and its applications. In Computer Science - Theory and Applications - 12th International Computer Science Symposium in Russia, CSR 2017, Kazan, Russia, June 8-12, 2017, Proceedings, pages 294-307, 2017. URL: