Cut-Based Conflict Analysis in Mixed Integer Programming

References

• Achterberg T (2007a) Conflict analysis in mixed integer programming. Discrete Optim. 4(1):4–20.Crossref, Google Scholar
• Achterberg T (2007b) Constraint integer programming. Unpublished PhD thesis, Technische Universität, Berlin, Germany.Google Scholar
• Bayardo RJ Jr, Schrag R (1997) Using CSP look-back techniques to solve real-world SAT instances. Proc. 14th Natl. Conf. Artificial Intelligence (AAAI Press, Palo Alto, CA), 203–208.Google Scholar
• Beame P, Kautz H, Sabharwal A (2004) Towards understanding and harnessing the potential of clause learning. J. Artificial Intelligence Res. 22:319–351.Crossref, Google Scholar
• Blake A (1937) Canonical expressions in Boolean algebra. Unpublished PhD thesis, University of Chicago, Chicago.Google Scholar
• Bolusani S, Besançon M, Bestuzheva K, Chmiela A, Dionísio J, Donkiewicz T, van Doornmalen J, et al. (2024) The SCIP optimization suite 9.0. Preprint, submitted February 27, https://arxiv.org/abs/2402.17702.Google Scholar
• Brearley A, Mitra G, Williams HP (1975) Analysis of mathematical programming problems prior to applying the simplex algorithm. Math. Programming 8:54–83.Crossref, Google Scholar
• Buss SR, Nordström J (2021) Proof complexity and SAT solving. Biere A, Heule MJH, van Maaren H, Walsh T, eds. Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, 2nd ed., vol. 336 (IOS Press, Amsterdam), 233–350.Google Scholar
• Chai D, Kuehlmann A (2005) A fast pseudo-Boolean constraint solver. IEEE Trans. Comput. Aided Design Integrated Circuits Systems 24(3):305–317.Crossref, Google Scholar
• Chvátal V (1973) Edmonds polytopes and a hierarchy of combinatorial problems. Discrete Math. 4(4):305–337.Crossref, Google Scholar
• Cook W, Coullard CR, Turán G (1987) On the complexity of cutting-plane proofs. Discrete Appl. Math. 18(1):25–38.Crossref, Google Scholar
• Davey B, Boland N, Stuckey PJ (2002) Efficient intelligent backtracking using linear programming. INFORMS J. Comput. 14(4):373–386.Link, Google Scholar
• Davis M, Putnam H (1960) A computing procedure for quantification theory. J. ACM 7(3):201–215.Crossref, Google Scholar
• Davis M, Logemann G, Loveland D (1962) A machine program for theorem proving. Comm. ACM 5(7):394–397.Crossref, Google Scholar
• Devriendt J, Gleixner A, Nordström J (2021) Learn to relax: Integrating 0-1 integer linear programming with pseudo-Boolean conflict-driven search. Constraints 26(1–4):26–55.Crossref, Google Scholar
• Dixon HE, Ginsberg ML (2002) Inference methods for a pseudo-Boolean satisfiability solver. Proc. 18th Natl. Conf. Artificial Intelligence, Edmonton (AAAI Press, Palo Alto, CA), 635–640.Google Scholar
• Eén N, Sörensson N (2006) Translating pseudo-Boolean constraints into SAT. J. Satisfiability Boolean Model. Comput. 2(1–4):1–26.Google Scholar
• Elffers J, Nordström J (2018) Divide and conquer: Towards faster pseudo-Boolean solving. Proc. 27th Internat. Joint Conf. Artificial Intelligence (IJCAI), 1291–1299.Google Scholar
• Gleixner A, Hendel G, Gamrath Get al.(2021) MIPLIB 2017: Data-driven compilation of the 6th mixed-integer programming library. Math. Programming Comput. 13:443–490.Crossref, Google Scholar
• Gocht S, Nordström J, Yehudayoff A (2019) On division versus saturation in pseudo-Boolean solving. Proc. 28th Internat. Joint Conf. Artificial Intelligence (IJCAI), 1711–1718.Google Scholar
• Gomory RE (1960) An algorithm for the mixed integer problem. Research Memorandum RM-2597, The RAND Corporation, Santa Monica, CA.Google Scholar
• Haken A (1985) The intractability of resolution. Theoret. Comput. Sci. 39(2–3):297–308.Crossref, Google Scholar
• Hojny C, Gally T, Habeck O, Lüthen H, Matter F, Pfetsch ME, Schmitt A (2020) Knapsack polytopes: A survey. Ann. Oper. Res. 292:469–517.Crossref, Google Scholar
• Hooker JN (1988) Generalized resolution and cutting planes. Ann. Oper. Res. 12(1):217–239.Crossref, Google Scholar
• Hooker JN (1992) Generalized resolution for 0-1 linear inequalities. Ann. Math. Artificial Intelligence 6(1):271–286.Google Scholar
• Joshi S, Martins R, Manquinho VM (2015) Generalized totalizer encoding for pseudo-Boolean constraints. Proc. 21st Internat. Conf. Principles Practice Constraint Programming, Lecture Notes in Computer Science, vol. 9255 (Springer, Cham, Switzerland), 200–209.Google Scholar
• Jovanovic D, de Moura L (2013) Cutting to the chase solving linear integer arithmetic. J. Automated Reasoning 51(1):79–108.Crossref, Google Scholar
• Le Berre D, Parrain A (2010) The Sat4j library, release 2.2. J. Satisfiability Boolean Model. Comput. 7(2–3):59–64.Crossref, Google Scholar
• Lodi A, Tramontani A (2013) Performance variability in mixed-integer programming. Theory Driven by Influential Applications (INFORMS, Catonsville, MD), 1–12.Link, Google Scholar
• Marchand H, Wolsey LA (2001) Aggregation and mixed integer rounding to solve MIPs. Oper. Res. 49(3):363–371.Link, Google Scholar
• Marques-Silva JP, Sakallah KA (1999) GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5):506–521.Crossref, Google Scholar
• Martins R, Manquinho VM, Lynce I (2014) Open-WBO: A modular MaxSAT solver. Proc. 17th Internat. Conf. Theory Appl. Satisfiability Testing, Lecture Notes in Computer Science, vol. 8561 (Springer, Cham, Switzerland), 438–445.Google Scholar
• Mexi G, Berthold T, Gleixner A, Nordström J (2023) Improving conflict analysis in MIP solvers by pseudo-Boolean reasoning. Proc. 29th Internat. Conf. Principles Practice Constraint Programming, Toronto, Canada, Leibniz International Proceedings in Informatics, vol. 280, 27:1–26:19.Google Scholar
• Mexi G, Serrano F, Berthold T, Gleixner A, Nordström J (2025) Cut-based conflict analysis in mixed integer programming. https://doi.org/10.1287/ijoc.2024.0999.cd, https://github.com/INFORMSJoC/2024.0999.Google Scholar
• Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: Engineering an efficient SAT solver. Proc. 38th Design Automation Conf. (IEEE, Piscataway, NJ), 530–535.Google Scholar
• Robinson JA (1965) A machine-oriented logic based on the resolution principle. J. ACM 12(1):23–41.Crossref, Google Scholar
• Sakai M, Nabeshima H (2015) Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers. IEICE Trans. Inform. Systems 98-D(6):1121–1127.Crossref, Google Scholar
• Sandholm T, Shields R (2006) Nogood learning for mixed integer programming. Workshop Hybrid Methods Branching Rules Combin. Optim. (Montréal, Canada), 21–22.Google Scholar
• Sheini HM, Sakallah KA (2006) Pueblo: A hybrid pseudo-Boolean SAT solver. J. Satisfiability Boolean Model. Comput. 2(1–4):165–189.Crossref, Google Scholar
• Stallman RM, Sussman GJ (1977) Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial Intelligence 9(2):135–196.Google Scholar
• Urquhart A (1987) Hard examples for resolution. J. ACM 34(1):209–219.Crossref, Google Scholar
• Williams HP (1976) Fourier-Motzkin elimination extension to integer programming problems. J. Combin. Theory Ser. A 21(1):118–123.Crossref, Google Scholar
• Witzig J, Berthold T, Heinz S (2021) Computational aspects of infeasibility analysis in mixed integer programming. Math. Programming Comput. 13(4):753–785.Crossref, Google Scholar