[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. [doi: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. [doi:10.1287/moor.1040.0099]

[3]   Michael Alekhnovich and Alexander A. Razborov: Satisfiability, branch-width and Tseitin tautologies. Comput. Complexity, 20:649–678, 2011. Preliminary version in FOCS’02. [doi:10.1007/s00037-011-0033-1]

[4]   Albert Atserias, Maria Luisa Bonet, and Juan Luis Esteban: Lower bounds for the weak pigeonhole principle and random formulas beyond resolution. Inform. Comput., 176(2):136–152, 2002. [doi:10.1006/inco.2002.3114]

[5]   Albert Atserias, Massimo Lauria, and Jakob Nordström: Narrow proofs may be maximally long. ACM Trans. Comput. Logic, 17(3):19:1–30, 2016. [doi: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 Proc. 44th STOC, pp. 307–326. ACM Press, 2012. [doi:10.1145/2213977.2214006]

[7]   Amitabh Basu, Michele Conforti, Marco Di Summa, and Hongyi Jiang: Complexity of branch-and-bound and cutting planes in mixed-integer optimization. Math. Programming, 198(1):787–810, 2022. Preliminary version in IPCO’21. [doi:10.1007/s10107-022-01789-5]

[8]   Roberto J. Bayardo Jr. and Robert C. Schrag: Using CSP look-back techniques to solve real-world SAT instances. In Benjamin Kuipers and Bonnie L. Webber, editors, Proc. 14th National Conf. on Artificial Intelligence and 9th Innovative Applications of Artificial Intelligence Conf., AAAI’97/IAAI’97, pp. 203–208. AAAI Press / The MIT Press, 1997. Available at AAAI Library.

[9]   Paul Beame, Christopher Beck, and Russell Impagliazzo: Time-space tradeoffs in resolution: superpolynomial lower bounds for superlinear space. SIAM J. Comput., 45(4), 2016. Preliminary version in STOC’12. [doi:10.1137/130914085]

[10]   Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis Pankratov, Toniann Pitassi, and Robert Robere: Stabbing planes. In Proc. 9th Innovations in Theoret. Comp. Sci. Conf. (ITCS’18), pp. 10:1–20. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2018. [doi:10.4230/LIPIcs.ITCS.2018.10]

[11]   Chris Beck, Jakob Nordström, and Bangsheng Tang: Some trade-off results for polynomial calculus: Extended abstract. In Proc. 45th STOC, pp. 813–822. ACM Press, 2013. [doi:10.1145/2488608.2488711]

[12]   Eli Ben-Sasson and Avi Wigderson: Short proofs are narrow – resolution made simple. J. ACM, 48(2):149–169, 2001. [doi:10.1145/375827.375835]

[13]   Christoph Berkholz and Jakob Nordström: Supercritical space-width trade-offs for resolution. SIAM J. Comput., 49(1):98–118, 2020. [doi:10.1137/16M1109072]

[14]   Alexander Bockmayr, Friedrich Eisenbrand, Mark E. Hartmann, and Andreas S. Schulz: On the Chvátal rank of polytopes in the 0/1 cube. Discr. Appl. Math., 98(1–2):21–27, 1999. [doi:10.1016/S0166-218X(99)00156-0]

[15]   Merve Bodur, Alberto Del Pia, Santanu S. Dey, Marco Molinaro, and Sebastian Pokutta: Aggregation-based cutting-planes for packing and covering integer programs. Math. Programming, 171(1–2):331–359, 2018. [doi:10.1007/s10107-017-1192-x]

[16]   Maria Luisa Bonet and Nicola Galesi: Optimality of size-width tradeoffs for resolution. Comput. Complexity, 10(4):261–276, 2001. [doi:10.1007/s000370100000]

[17]   Maria Luisa Bonet, Toniann Pitassi, and Ran Raz: Lower bounds for cutting planes proofs with small coefficients. J. Symbolic Logic, 62(3):708–728, 1997. [doi:10.2307/2275569]

[18]   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. [doi:10.4086/toc.2006.v002a004]

[19]   Samuel R. Buss, Dima Grigoriev, Russell Impagliazzo, and Toniann Pitassi: Linear gaps between degrees for the polynomial calculus modulo distinct primes. J. Comput. System Sci., 62(2):267–289, 2001. [doi:10.1006/jcss.2000.1726]

[20]   Vašek Chvátal: Edmonds polytopes and a hierarchy of combinatorial problems. Discr. Math., 4(4):305–337, 1973. [doi:10.1016/0012-365X(73)90167-2]

[21]   Vašek Chvátal: Cutting-plane proofs and the stability number of a graph. Technical Report TR-84326, Inst. für Ökonometrie und Operations Research, Rhein. Friedrich-Wilhelms-Univ., 1984. Available on author’s webpage.

[22]   Vašek Chvátal, William Cook, and Mark Hartmann: On cutting-plane proofs in combinatorial optimization. Lin. Alg. Appl., 114–115:455–499, 1989. [doi:10.1016/0024-3795(89)90476-x]

[23]   Vašek Chvátal and Endre Szemerédi: Many hard examples for resolution. J. ACM, 35(4):759–768, 1988. [doi:10.1145/48014.48016]

[24]   Stephen A. Cook and Robert A. Reckhow: The relative efficiency of propositional proof systems. J. Symbolic Logic, 44(1):36–50, 1979. [doi:10.2307/2273702]

[25]   William J. Cook, Collette R. Coullard, and György Turán: On the complexity of cutting-plane proofs. Discr. Appl. Math., 18(1):25–38, 1987. [doi:10.1016/0166-218X(87)90039-4]

[26]   Gérard Cornuéjols and Yanjun Li: On the rank of mixed 0, 1 polyhedra. Math. Programming, 91(2):391–397, 2002. [doi:10.1007/s101070100250]

[27]   Daniel Dadush and Samarth Tiwari: On the complexity of branching proofs. In Proc. 35th Comput. Complexity Conf. (CCC’20, virtual conference), pp. 34:1–35. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2020. [doi:10.4230/LIPIcs.CCC.2020.34]

[28]   Adnan Darwiche: Recursive conditioning. Artificial Intelligence, 126(1–2):5–41, 2001. [doi:10.1016/S0004-3702(00)00069-2]

[29]   Martin Davis and Hilary Putnam: A computing procedure for quantification theory. J. ACM, 7(3):201–215, 1960. [doi:10.1145/321033.321034]

[30]   Rina Dechter: Bucket elimination: A unifying framework for processing hard and soft constraints. ACM Computing Surveys, 28(4es):61:1–5, 1996. [doi:10.1145/242224.242302]

[31]   Friedrich Eisenbrand and Andreas S. Schulz: Bounds on the Chvátal rank of polytopes in the 0/1-cube. Combinatorica, 23:245–261, 2003. Preliminary version in IPCO’99. [doi:10.1007/s00493-003-0020-5]

[32]   Yuval Filmus, Pavel Hrubeš, and Massimo Lauria: Semantic versus syntactic cutting planes. In Proc. 33rd Symp. Theoret. Aspects of Comp. Sci. (STACS’16), pp. 35:1–13. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2016. [doi:10.4230/LIPIcs.STACS.2016.35]

[33]   Matteo Fischetti and Andrea Lodi: Local branching. Math. Programming, 98(1–3):23–47, 2003. [doi:10.1007/s10107-003-0395-5]

[34]   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 Proc. 36th Comput. Complexity Conf. (CCC’21), pp. 6:1–30. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2021. [doi:10.4230/LIPIcs.CCC.2021.6]

[35]   Noah Fleming, Denis Pankratov, Toniann Pitassi, and Robert Robere: Random (log n)-CNFs are hard for cutting planes. J. ACM, 69(3):19:1–32, 2022. Preliminary version in FOCS’17. [doi:10.1145/3486680]

[36]    Ankit Garg, Mika Göös, Pritish Kamath, and Dmitry Sokolov: Monotone circuit lower bounds from resolution. Theory of Computing, 16(13):1–30, 2020. Preliminary version in STOC’18. [doi:10.4086/toc.2020.v016a013]

[37]   Michel X. Goemans and David P. Williamson: .879-approximation algorithms for MAX CUT and MAX 2SAT. In Proc. 26th STOC, pp. 422–431. ACM Press, 1994. [doi:10.1145/195058.195216]

[38]   Ralph E. Gomory: An algorithm for integer solutions to linear programs. In Robert L. Graves and Philip Wolfe, editors, Recent Advances in Mathematical Programming (1962), volume 64, pp. 269–302. McGraw-Hill, 1963. Available at ralphgomory.org, PDF page 286.

[39]   Mika Göös, Sajin Koroth, Ian Mertz, and Toniann Pitassi: Automating cutting planes is NP-hard. In Proc. 52nd STOC, pp. 68–77. ACM Press, 2020. [doi:10.1145/3357713.3384248]

[40]   Dima Grigoriev: Tseitin’s tautologies and lower bounds for Nullstellensatz proofs. In Proc. 39th FOCS, pp. 648–652. IEEE Comp. Soc., 1998. [doi:10.1109/SFCS.1998.743515]

[41]   Dima Grigoriev: Linear lower bound on degrees of Positivstellensatz calculus proofs for the parity. Theoret. Comput. Sci., 259(1–2):613–622, 2001. [doi:10.1016/S0304-3975(00)00157-2]

[42]   Pavel Hrubeš and Pavel Pudlák: Random formulas, monotone circuits, and interpolation. In Proc. 58th FOCS, pp. 121–131. IEEE Comp. Soc., 2017. [doi:10.1109/FOCS.2017.20]

[43]   Russell Impagliazzo, Toniann Pitassi, and Alasdair Urquhart: Upper and lower bounds for tree-like cutting planes proofs. In Proc. 9th Ann. ACM/IEEE Symp. on Logic in Computer Science (LICS’94), pp. 220–228. IEEE Comp. Soc., 1994. [doi:10.1109/LICS.1994.316069]

[44]   Miroslav Karamanov and Gérard Cornuéjols: Branching on general disjunctions. Math. Programming, 128(1–2):403–436, 2011. [doi:10.1007/s10107-009-0332-3]

[45]   Arist Kojevnikov: Improved lower bounds for tree-like resolution over linear inequalities. In João Marques-Silva and Karem A. Sakallah, editors, Proc. 10th Internat. Conf. Theory Appl. Satisfiability Testing (SAT’07), volume 4501 of LNCS, pp. 70–79. Springer, 2007. [doi:10.1007/978-3-540-72788-0_10]

[46]   Jan Krajícek: Discretely ordered modules as a first-order extension of the Cutting Planes proof system. J. Symbolic Logic, 63(4):1582–1596, 1998. [doi:10.2307/2586668]

[47]   Bala Krishnamoorthy and Gábor Pataki: Column basis reduction and decomposable knapsack problems. Discr. Optimization, 6(3):242–270, 2009. [doi:10.1016/j.disopt.2009.01.003]

[48]   Neha Lodha, Sebastian Ordyniak, and Stefan Szeider: A SAT approach to branchwidth. ACM Trans. Comput. Logic, 20(3):15:1–24, 2019. [doi:10.1145/3326159]

[49]    Ashutosh Mahajan and Theodore K. Ralphs: Experiments with branching using general disjunctions. In Operations Research and Cyber-Infrastructure (ORCS), pp. 101–118. Springer, 2009. [doi:10.1007/978-0-387-88843-9_6]

[50]   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. [doi:10.1137/16M106176X]

[51]   João P. Marques-Silva and Karem A. Sakallah: GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Computers, 48(5):506–521, 1999. [doi:10.1109/12.769433]

[52]   Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik: Chaff: Engineering an efficient SAT solver. In Proc. 38th Design Automation Conf. (DAC’01), pp. 530–535. ACM Press, 2001. [doi:10.1145/378239.379017]

[53]   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. [doi:10.1023/A:1011207119557]

[54]   Pablo A. Parrilo: Structured semidefinite programs and semialgebraic geometry methods in robustness and optimization. Ph. D. thesis, CalTech, 2000. Available on author’s website.

[55]   Sebastian Pokutta and Andreas S. Schulz: On the rank of cutting-plane proof systems. In Proc. 14th Integer Prog. Combinat. Optim. (IPCO’10), volume 6080 of LNCS, pp. 450–463. Springer, 2010. [doi:10.1007/978-3-642-13036-6_34]

[56]   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. [doi:10.1016/j.orl.2011.09.004]

[57]   Pavel Pudlák: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symbolic Logic, 62(3):981–998, 1997. [doi:10.2307/2275583]

[58]   Pavel Pudlák: Proofs as games. Amer. Math. Monthly, 107(6):541–550, 2000. [doi:10.1080/00029890.2000.12005233]

[59]   Alexander A. Razborov: A new kind of tradeoffs in propositional proof complexity. J. ACM, 63(2):16:1–14, 2016. [doi:10.1145/2858790]

[60]   Alexander A. Razborov: On the width of semialgebraic proofs and algorithms. Math. Oper. Res., 42(4):1106–1134, 2017. [doi:10.1287/moor.2016.0840]

[61]   Thomas Rothvoß and Laura Sanità: 0/1 polytopes with quadratic Chvátal rank. In Proc. 16th Integer Prog. Combinat. Optim. (IPCO’13), pp. 349–361. Springer, 2013. [doi:10.1007/978-3-642-36694-9_30]

[62]   Grant Schoenebeck: Linear level Lasserre lower bounds for certain k-CSPs. In Proc. 49th FOCS, pp. 593–602. IEEE Comp. Soc., 2008. [doi:10.1109/FOCS.2008.74]

[63]   Alexander Schrijver: On cutting planes. In Peter L. Hammer, editor, Combinatorics 79, volume 9 of Ann. Discr. Math., pp. 291–296. Elsevier, 1980. [doi:10.1016/S0167-5060(08)70085-2]