On the Complexity of Branching Proofs

Authors Daniel Dadush, Samarth Tiwari

Thumbnail PDF


  • Filesize: 0.7 MB
  • 35 pages

Document Identifiers

Author Details

Daniel Dadush
  • Centrum Wiskunde &Informatica, Amsterdam, The Netherlands
Samarth Tiwari
  • Centrum Wiskunde &Informatica, Amsterdam, The Netherlands


The first author would like to deeply thank Noah Fleming, Denis Pankratov, Toni Pitassi and Robert Robere for posing the bit-size vs length question for SP and for very stimulating conversations while the author was visiting the University of Toronto. The authors are also very grateful for the comments from the anonymous reviewers, which have greatly helped us improve the quality of the presentation.

Cite AsGet BibTex

Daniel Dadush and Samarth Tiwari. On the Complexity of Branching Proofs. In 35th Computational Complexity Conference (CCC 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 169, pp. 34:1-34:35, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)


We consider the task of proving integer infeasibility of a bounded convex K in ℝⁿ using a general branching proof system. In a general branching proof, one constructs a branching tree by adding an integer disjunction 𝐚𝐱 ≤ b or 𝐚𝐱 ≥ b+1, 𝐚 ∈ ℤⁿ, b ∈ ℤ, at each node, such that the leaves of the tree correspond to empty sets (i.e., K together with the inequalities picked up from the root to leaf is empty). Recently, Beame et al (ITCS 2018), asked whether the bit size of the coefficients in a branching proof, which they named stabbing planes (SP) refutations, for the case of polytopes derived from SAT formulas, can be assumed to be polynomial in n. We resolve this question in the affirmative, by showing that any branching proof can be recompiled so that the normals of the disjunctions have coefficients of size at most (n R)^O(n²), where R ∈ ℕ is the radius of an 𝓁₁ ball containing K, while increasing the number of nodes in the branching tree by at most a factor O(n). Our recompilation techniques works by first replacing each disjunction using an iterated Diophantine approximation, introduced by Frank and Tardos (Combinatorica 1986), and proceeds by "fixing up" the leaves of the tree using judiciously added Chvátal-Gomory (CG) cuts. As our second contribution, we show that Tseitin formulas, an important class of infeasible SAT instances, have quasi-polynomial sized cutting plane (CP) refutations. This disproves a conjecture that Tseitin formulas are (exponentially) hard for CP. Our upper bound follows by recompiling the quasi-polynomial sized SP refutations for Tseitin formulas due to Beame et al, which have a special enumerative form, into a CP proof of the same length using a serialization technique of Cook et al (Discrete Appl. Math. 1987). As our final contribution, we give a simple family of polytopes in [0,1]ⁿ requiring exponential sized branching proofs.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
  • Branching Proofs
  • Cutting Planes
  • Diophantine Approximation
  • Integer Programming
  • Stabbing Planes
  • Tseitin Formulas


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


  1. Karen Aardal and Arjen K Lenstra. Hard equality constrained integer knapsacks. Mathematics of operations research, 29(3):724-738, 2004. Google Scholar
  2. W. Banaszczyk. Inequalities for convex bodies and polar reciprocal lattices in Rⁿ II: Application of K-convexity. Discrete and Computational Geometry, 16:305-311, 1996. Google Scholar
  3. Evelyn Martin Lansdowne Beale and John A Tomlin. Special facilities in a general mathematical programming system for non-convex problems using ordered sets of variables. OR, 69(447-454):99, 1970. Google Scholar
  4. Paul Beame. Proof complexity. In Steven Rudich and Avi Wigderson, editors, Computational Complexity Theory, volume 10 of IAS/Park City Mathematics Series, pages 199-246. American Mathematical Society, 2004. Google Scholar
  5. Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing planes. In 9th Innovations in Theoretical Computer Science, volume 94 of LIPIcs. Leibniz Int. Proc. Inform., pages Art. No. 10, 20. Schloss Dagstuhl. Leibniz-Zent. Inform., Wadern, 2018. Google Scholar
  6. Vasek Chvatal. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete mathematics, 4(4):305-337, 1973. Google Scholar
  7. W. Cook, C. R. Coullard, and Gy. Turán. On the complexity of cutting-plane proofs. Discrete Appl. Math., 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  8. Gérard Cornuéjols and Yanjun Li. Elementary closures for integer programs. Operations Research Letters, 28(1):1-8, 2001. Google Scholar
  9. Daniel Dadush. Integer Programming, Lattice Algorithms, and Deterministic Volume Estimation. PhD thesis, Georgia Institute of Technology, 2012. Google Scholar
  10. Daniel Dadush, Santanu S Dey, and Juan Pablo Vielma. On the chvátal-gomory closure of a compact convex set. Mathematical Programming, 145(1-2):327-348, 2014. Google Scholar
  11. Matteo Fischetti and Andrea Lodi. Local branching. Mathematical programming, 98(1-3):23-47, 2003. Google Scholar
  12. András Frank and Éva Tardos. An application of simultaneous Diophantine approximation in combinatorial optimization. Combinatorica, 7(1):49-65, 1987. URL: https://doi.org/10.1007/BF02579200.
  13. Ralph Gomory. An outline of an algorithm for solving integer programs. Bulletin of the American Mathematical Society, 64(5):275-278, 1958. Google Scholar
  14. Miroslav Karamanov and Gérard Cornuéjols. Branching on general disjunctions. Mathematical Programming, 128(1-2):403-436, 2011. Google Scholar
  15. Jan Krajíček. Discretely ordered modules as a first-order extension of the cutting planes proof system. The Journal of Symbolic Logic, 63(4):1582-1596, 1998. Google Scholar
  16. Bala Krishnamoorthy and Gábor Pataki. Column basis reduction and decomposable knapsack problems. Discrete Optimization, 6(3):242-270, 2009. Google Scholar
  17. H. W. Lenstra, Jr. Integer programming with a fixed number of variables. Math. Oper. Res., 8(4):538-548, 1983. URL: https://doi.org/10.1287/moor.8.4.538.
  18. Ashutosh Mahajan and Theodore K Ralphs. Experiments with branching using general disjunctions. In Operations Research and Cyber-Infrastructure, pages 101-118. Springer, 2009. Google Scholar
  19. Jonathan H Owen and Sanjay Mehrotra. Experimental results on using general disjunctions in branch-and-bound for general-integer linear programs. Computational optimization and applications, 20(2):159-170, 2001. Google Scholar
  20. Gábor Pataki and Mustafa Tural. Basis reduction methods. Wiley Encyclopedia of Operations Research and Management Science, 2010. Google Scholar
  21. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. The Journal of Symbolic Logic, 62(3):981-998, 1997. Google Scholar
  22. M. Rudelson. Distances between non-symmetric convex bodies and the MM^∗-estimate. Positivity, 4(2):161-178, 2000. URL: https://doi.org/10.1023/A:1009842406728.
  23. Wolfgang M. Schmidt. Diophantine approximation, volume 785 of Lecture Notes in Mathematics. Springer, Berlin, 1980. Google Scholar
  24. Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley &Sons, Inc., USA, 1986. Google Scholar