Document

On the Complexity of Branching Proofs

File

LIPIcs.CCC.2020.34.pdf
• Filesize: 0.7 MB
• 35 pages

Acknowledgements

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 As

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)
https://doi.org/10.4230/LIPIcs.CCC.2020.34

Abstract

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
Keywords
• Branching Proofs
• Cutting Planes
• Diophantine Approximation
• Integer Programming
• Stabbing Planes
• Tseitin Formulas

Metrics

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

References

1. Karen Aardal and Arjen K Lenstra. Hard equality constrained integer knapsacks. Mathematics of operations research, 29(3):724-738, 2004.
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.
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.
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.
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.
6. Vasek Chvatal. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete mathematics, 4(4):305-337, 1973.
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.
9. Daniel Dadush. Integer Programming, Lattice Algorithms, and Deterministic Volume Estimation. PhD thesis, Georgia Institute of Technology, 2012.
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.
11. Matteo Fischetti and Andrea Lodi. Local branching. Mathematical programming, 98(1-3):23-47, 2003.
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.
14. Miroslav Karamanov and Gérard Cornuéjols. Branching on general disjunctions. Mathematical Programming, 128(1-2):403-436, 2011.
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.
16. Bala Krishnamoorthy and Gábor Pataki. Column basis reduction and decomposable knapsack problems. Discrete Optimization, 6(3):242-270, 2009.
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.
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.
20. Gábor Pataki and Mustafa Tural. Basis reduction methods. Wiley Encyclopedia of Operations Research and Management Science, 2010.
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.
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.
24. Alexander Schrijver. Theory of Linear and Integer Programming. John Wiley &Sons, Inc., USA, 1986.