Document Open Access Logo

On the Power and Limitations of Branch and Cut

Authors Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, Avi Wigderson

PDF
Thumbnail PDF

File

LIPIcs.CCC.2021.6.pdf
  • Filesize: 0.84 MB
  • 30 pages

Document Identifiers

Author Details

Noah Fleming
  • University of Toronto, Canada
  • Simons Institute, Berkeley, CA, USA
Mika Göös
  • EPFL, Lausanne, Switzerland
Russell Impagliazzo
  • University of California, San Diego, CA, USA
Toniann Pitassi
  • University of Toronto, Canada
  • IAS, Princeton, NJ, USA
Robert Robere
  • McGill University, Montréal, Canada
Li-Yang Tan
  • Standford University, CA, USA
Avi Wigderson
  • IAS, Princeton, NJ, USA

Funding

  • Impagliazzo, Russell: Research supported by NSF and the Simons Foundation.
  • Pitassi, Toniann: Research supported by NSERC, NSF Grant No. CCF-1900460 and the IAS school of mathematics.
  • Robere, Robert: Research supported by the Charles Simonyi Endowment, and indirectly supported by the National Science Foundation Grant No. CCF-1900460.
  • Tan, Li-Yang: Research supported by NSF grant CCF-192179 and NSF CAREER award CCF-1942123.
  • Wigderson, Avi: Research partially supported by NSF grant CCF-1900460.

Acknowledgements

N.F. would like to thank Albert Atserias for some corrections to an earlier version of this paper.

Cite AsGet BibTex

Noah Fleming, Mika Göös, Russell Impagliazzo, Toniann Pitassi, Robert Robere, Li-Yang Tan, and Avi Wigderson. On the Power and Limitations of Branch and Cut. In 36th Computational Complexity Conference (CCC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 200, pp. 6:1-6:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CCC.2021.6

Abstract

The Stabbing Planes proof system [Paul Beame et al., 2018] was introduced to model the reasoning carried out in practical mixed integer programming solvers. As a proof system, it is powerful enough to simulate Cutting Planes and to refute the Tseitin formulas - certain unsatisfiable systems of linear equations od 2 - which are canonical hard examples for many algebraic proof systems. In a recent (and surprising) result, Dadush and Tiwari [Daniel Dadush and Samarth Tiwari, 2020] showed that these short refutations of the Tseitin formulas could be translated into quasi-polynomial size and depth Cutting Planes proofs, refuting a long-standing conjecture. This translation raises several interesting questions. First, whether all Stabbing Planes proofs can be efficiently simulated by Cutting Planes. This would allow for the substantial analysis done on the Cutting Planes system to be lifted to practical mixed integer programming solvers. Second, whether the quasi-polynomial depth of these proofs is inherent to Cutting Planes. In this paper we make progress towards answering both of these questions. First, we show that any Stabbing Planes proof with bounded coefficients (SP*) can be translated into Cutting Planes. As a consequence of the known lower bounds for Cutting Planes, this establishes the first exponential lower bounds on SP*. Using this translation, we extend the result of Dadush and Tiwari to show that Cutting Planes has short refutations of any unsatisfiable system of linear equations over a finite field. Like the Cutting Planes proofs of Dadush and Tiwari, our refutations also incur a quasi-polynomial blow-up in depth, and we conjecture that this is inherent. As a step towards this conjecture, we develop a new geometric technique for proving lower bounds on the depth of Cutting Planes proofs. This allows us to establish the first lower bounds on the depth of Semantic Cutting Planes proofs of the Tseitin formulas.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof complexity
Keywords
  • Proof Complexity
  • Integer Programming
  • Cutting Planes
  • Branch and Cut
  • Stabbing Planes

Metrics

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

References

  1. Karen Aardal, Robert E. Bixby, Cor A. J. Hurkens, Arjen K. Lenstra, and Job W. Smeltink. Market split and basis reduction: Towards a solution of the cornuéjols-dawande instances. INFORMS J. Comput., 12(3):192-202, 2000. URL: https://doi.org/10.1287/ijoc.12.3.192.12635.
  2. Karen Aardal and Arjen K. Lenstra. Hard equality constrained integer knapsacks. Math. Oper. Res., 29(3):724-738, 2004. URL: https://doi.org/10.1287/moor.1040.0099.
  3. Michael Alekhnovich and Alexander A. Razborov. Satisfiability, branch-width and tseitin tautologies. In 43rd Symposium on Foundations of Computer Science (FOCS 2002), 16-19 November 2002, Vancouver, BC, Canada, Proceedings, pages 593-603. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/SFCS.2002.1181983.
  4. Albert Atserias, Maria Luisa Bonet, and Juan Luis Esteban. Lower bounds for the weak pigeonhole principle and random formulas beyond resolution. Inf. Comput., 176(2):136-152, 2002. URL: https://doi.org/10.1006/inco.2002.3114.
  5. Albert Atserias, Massimo Lauria, and Jakob Nordström. Narrow proofs may be maximally long. ACM Trans. Comput. Log., 17(3):19:1-19:30, 2016. URL: https://doi.org/10.1145/2898435.
  6. Boaz Barak, Fernando G. S. L. Brandão, Aram Wettroth Harrow, Jonathan A. Kelner, David Steurer, and Yuan Zhou. Hypercontractivity, sum-of-squares proofs, and their applications. In Proceedings of the 44th Symposium on Theory of Computing Conference, STOC 2012, New York, NY, USA, May 19 - 22, 2012, pages 307-326, 2012. URL: https://doi.org/10.1145/2213977.2214006.
  7. Paul Beame, Christopher Beck, and Russell Impagliazzo. Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. 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 213-232. ACM, 2012. URL: https://doi.org/10.1145/2213977.2213999.
  8. Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere. Stabbing planes. In 9th Innovations in Theoretical Computer Science Conference, ITCS 2018, January 11-14, 2018, Cambridge, MA, USA, pages 10:1-10:20, 2018. URL: https://doi.org/10.4230/LIPIcs.ITCS.2018.10.
  9. Chris Beck, Jakob Nordström, and Bangsheng Tang. Some trade-off results for polynomial calculus: extended abstract. In Dan Boneh, Tim Roughgarden, and Joan Feigenbaum, editors, Symposium on Theory of Computing Conference, STOC'13, Palo Alto, CA, USA, June 1-4, 2013, pages 813-822. ACM, 2013. URL: https://doi.org/10.1145/2488608.2488711.
  10. Eli Ben-Sasson and Avi Wigderson. Short proofs are narrow - resolution made simple. J. ACM, 48(2):149-169, 2001. URL: https://doi.org/10.1145/375827.375835.
  11. Christoph Berkholz and Jakob Nordström. Supercritical space-width trade-offs for resolution. SIAM J. Comput., 49(1):98-118, 2020. URL: https://doi.org/10.1137/16M1109072.
  12. Alexander Bockmayr, Friedrich Eisenbrand, Mark E. Hartmann, and Andreas S. Schulz. On the chvátal rank of polytopes in the 0/1 cube. Discret. Appl. Math., 98(1-2):21-27, 1999. URL: https://doi.org/10.1016/S0166-218X(99)00156-0.
  13. Merve Bodur, Alberto Del Pia, Santanu S. Dey, Marco Molinaro, and Sebastian Pokutta. Aggregation-based cutting-planes for packing and covering integer programs. Math. Program., 171(1-2):331-359, 2018. URL: https://doi.org/10.1007/s10107-017-1192-x.
  14. Maria Luisa Bonet and Nicola Galesi. Optimality of size-width tradeoffs for resolution. Comput. Complex., 10(4):261-276, 2001. URL: https://doi.org/10.1007/s000370100000.
  15. Maria Luisa Bonet, Toniann Pitassi, and Ran Raz. Lower bounds for cutting planes proofs with small coefficients. J. Symb. Log., 62(3):708-728, 1997. URL: https://doi.org/10.2307/2275569.
  16. Joshua Buresh-Oppenheim, Nicola Galesi, Shlomo Hoory, Avner Magen, and Toniann Pitassi. Rank bounds and integrality gaps for cutting planes procedures. Theory of Computing, 2(4):65-90, 2006. URL: https://doi.org/10.4086/toc.2006.v002a004.
  17. Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi. Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. Syst. Sci., 62(2):267-289, 2001. URL: https://doi.org/10.1006/jcss.2000.1726.
  18. Vasek Chvátal. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Mathematics, 4(4):305-337, 1973. URL: https://doi.org/10.1016/0012-365X(73)90167-2.
  19. Vašek Chvátal. Cutting-plane proofs and the stability number of a graph. Inst. für Ökonometrie und Operations Research, Rhein. Friedrich-Wilhelms-Univ., 1984. Google Scholar
  20. Vašek Chvátal, William Cook, and Mark Hartmann. On cutting-plane proofs in combinatorial optimization. Linear algebra and its applications, 114:455-499, 1989. Google Scholar
  21. Vasek Chvátal and Endre Szemerédi. Many hard examples for resolution. J. ACM, 35(4):759-768, 1988. URL: https://doi.org/10.1145/48014.48016.
  22. Stephen A. Cook and Robert A. Reckhow. The relative efficiency of propositional proof systems. J. Symb. Log., 44(1):36-50, 1979. URL: https://doi.org/10.2307/2273702.
  23. William J. Cook, Collette R. Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, 1987. URL: https://doi.org/10.1016/0166-218X(87)90039-4.
  24. Gérard Cornuéjols and Yanjun Li. On the rank of mixed 0, 1 polyhedra. Math. Program., 91(2):391-397, 2002. URL: https://doi.org/10.1007/s101070100250.
  25. Daniel Dadush and Samarth Tiwari. On the complexity of branching proofs. In Shubhangi Saraf, editor, 35th Computational Complexity Conference, CCC 2020, July 28-31, 2020, Saarbrücken, Germany (Virtual Conference), volume 169 of LIPIcs, pages 34:1-34:35. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.CCC.2020.34.
  26. Adnan Darwiche. Recursive conditioning. Artif. Intell., 126(1-2):5-41, 2001. URL: https://doi.org/10.1016/S0004-3702(00)00069-2.
  27. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. J. ACM, 7(3):201-215, 1960. URL: https://doi.org/10.1145/321033.321034.
  28. Rina Dechter. Bucket elimination: A unifying framework for processing hard and soft constraints. ACM Comput. Surv., 28(4es):61, 1996. URL: https://doi.org/10.1145/242224.242302.
  29. Friedrich Eisenbrand and Andreas S. Schulz. Bounds on the chvátal rank of polytopes in the 0/1-cube. In Gérard Cornuéjols, Rainer E. Burkard, and Gerhard J. Woeginger, editors, Integer Programming and Combinatorial Optimization, 7th International IPCO Conference, Graz, Austria, June 9-11, 1999, Proceedings, volume 1610 of Lecture Notes in Computer Science, pages 137-150. Springer, 1999. URL: https://doi.org/10.1007/3-540-48777-8_11.
  30. Yuval Filmus, Pavel Hrubes, and Massimo Lauria. Semantic versus syntactic cutting planes. In Nicolas Ollinger and Heribert Vollmer, editors, 33rd Symposium on Theoretical Aspects of Computer Science, STACS 2016, February 17-20, 2016, Orléans, France, volume 47 of LIPIcs, pages 35:1-35:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.STACS.2016.35.
  31. Matteo Fischetti and Andrea Lodi. Local branching. Math. Program., 98(1-3):23-47, 2003. URL: https://doi.org/10.1007/s10107-003-0395-5.
  32. Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere. Random Θ(log n)-CNFs are hard for cutting planes. In 58th IEEE Annual Symposium on Foundations of Computer Science, FOCS 2017, Berkeley, CA, USA, October 15-17, 2017, pages 109-120, 2017. URL: https://doi.org/10.1109/FOCS.2017.19.
  33. 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: https://doi.org/10.1145/3188745.3188838.
  34. Michel X. Goemans and David P. Williamson. .879approximationn algorithms for max cut and max 2sat. In Proceedings of the Twenty-sixth Annual ACM Symposium on Theory of Computing, STOC '94, pages 422-431, New York, NY, USA, 1994. ACM. URL: https://doi.org/10.1145/195058.195216.
  35. Ralph E Gomory. An algorithm for integer solutions to linear programs. Recent advances in mathematical programming, 64(260-302):14, 1963. Google Scholar
  36. Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi. Automating cutting planes is np-hard. In Konstantin Makarychev, Yury Makarychev, Madhur Tulsiani, Gautam Kamath, and Julia Chuzhoy, editors, Proccedings of the 52nd Annual ACM SIGACT Symposium on Theory of Computing, STOC 2020, Chicago, IL, USA, June 22-26, 2020, pages 68-77. ACM, 2020. URL: https://doi.org/10.1145/3357713.3384248.
  37. Dima Grigoriev. Tseitin’s tautologies and lower bounds for nullstellensatz proofs. In 39th Annual Symposium on Foundations of Computer Science, FOCS '98, November 8-11, 1998, Palo Alto, California, USA, pages 648-652. IEEE Computer Society, 1998. URL: https://doi.org/10.1109/SFCS.1998.743515.
  38. Dima Grigoriev. Linear lower bound on degrees of positivstellensatz calculus proofs for the parity. Theor. Comput. Sci., 259(1-2):613-622, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00157-2.
  39. 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: https://doi.org/10.1109/FOCS.2017.20.
  40. 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: https://doi.org/10.1109/LICS.1994.316069.
  41. Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Benjamin Kuipers and Bonnie L. Webber, editors, Proceedings of the Fourteenth National Conference on Artificial Intelligence and Ninth Innovative Applications of Artificial Intelligence Conference, AAAI 97, IAAI 97, July 27-31, 1997, Providence, Rhode Island, USA, pages 203-208. AAAI Press / The MIT Press, 1997. URL: http://www.aaai.org/Library/AAAI/1997/aaai97-032.php.
  42. Miroslav Karamanov and Gérard Cornuéjols. Branching on general disjunctions. Math. Program., 128(1-2):403-436, 2011. URL: https://doi.org/10.1007/s10107-009-0332-3.
  43. Arist Kojevnikov. Improved lower bounds for tree-like resolution over linear inequalities. In João Marques-Silva and Karem A. Sakallah, editors, Theory and Applications of Satisfiability Testing - SAT 2007, 10th International Conference, Lisbon, Portugal, May 28-31, 2007, Proceedings, volume 4501 of Lecture Notes in Computer Science, pages 70-79. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-72788-0_10.
  44. Jan Krajícek. 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
  45. Bala Krishnamoorthy and Gábor Pataki. Column basis reduction and decomposable knapsack problems. Discret. Optim., 6(3):242-270, 2009. URL: https://doi.org/10.1016/j.disopt.2009.01.003.
  46. Neha Lodha, Sebastian Ordyniak, and Stefan Szeider. A SAT approach to branchwidth. ACM Trans. Comput. Log., 20(3):15:1-15:24, 2019. URL: https://doi.org/10.1145/3326159.
  47. 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
  48. Adam W. Marcus, Daniel A. Spielman, and Nikhil Srivastava. Interlacing families IV: bipartite ramanujan graphs of all sizes. SIAM J. Comput., 47(6):2488-2509, 2018. URL: https://doi.org/10.1137/16M106176X.
  49. Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik. Chaff: Engineering an efficient SAT solver. In Proceedings of the 38th Design Automation Conference, DAC 2001, Las Vegas, NV, USA, June 18-22, 2001, pages 530-535. ACM, 2001. URL: https://doi.org/10.1145/378239.379017.
  50. Jonathan H. Owen and Sanjay Mehrotra. Experimental results on using general disjunctions in branch-and-bound for general-integer linear programs. Comput. Optim. Appl., 20(2):159-170, 2001. URL: https://doi.org/10.1023/A:1011207119557.
  51. Pablo A Parrilo. Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. PhD thesis, California Institute of Technology, 2000. Google Scholar
  52. Sebastian Pokutta and Andreas S. Schulz. On the rank of cutting-plane proof systems. In Friedrich Eisenbrand and F. Bruce Shepherd, editors, Integer Programming and Combinatorial Optimization, 14th International Conference, IPCO 2010, Lausanne, Switzerland, June 9-11, 2010. Proceedings, volume 6080 of Lecture Notes in Computer Science, pages 450-463. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-13036-6_34.
  53. Sebastian Pokutta and Andreas S. Schulz. Integer-empty polytopes in the 0/1-cube with maximal gomory-chvátal rank. Oper. Res. Lett., 39(6):457-460, 2011. URL: https://doi.org/10.1016/j.orl.2011.09.004.
  54. Pavel Pudlák. Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log., 62(3):981-998, 1997. URL: https://doi.org/10.2307/2275583.
  55. Pavel Pudlák. Proofs as games. The American Mathematical Monthly, 107(6):541-550, 2000. URL: https://doi.org/10.1080/00029890.2000.12005233.
  56. Alexander A. Razborov. A new kind of tradeoffs in propositional proof complexity. J. ACM, 63(2):16:1-16:14, 2016. URL: https://doi.org/10.1145/2858790.
  57. Alexander A. Razborov. On the width of semialgebraic proofs and algorithms. Math. Oper. Res., 42(4):1106-1134, 2017. URL: https://doi.org/10.1287/moor.2016.0840.
  58. Thomas Rothvoß and Laura Sanita. 0/1 polytopes with quadratic chvátal rank. In International Conference on Integer Programming and Combinatorial Optimization, pages 349-361. Springer, 2013. Google Scholar
  59. Grant Schoenebeck. Linear level lasserre lower bounds for certain k-csps. In 49th Annual IEEE Symposium on Foundations of Computer Science, FOCS 2008, October 25-28, 2008, Philadelphia, PA, USA, pages 593-602. IEEE Computer Society, 2008. URL: https://doi.org/10.1109/FOCS.2008.74.
  60. A. Schrijver. On cutting planes. In Peter L. Hammer, editor, Combinatorics 79, volume 9 of Annals of Discrete Mathematics, pages 291-296. Elsevier, 1980. URL: https://doi.org/10.1016/S0167-5060(08)70085-2.
  61. João P. Marques Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506-521, 1999. URL: https://doi.org/10.1109/12.769433.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact