Document Open Access Logo

Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning

Authors Gioni Mexi , Timo Berthold , Ambros Gleixner , Jakob Nordström

PDF
Thumbnail PDF

File

LIPIcs.CP.2023.27.pdf
  • Filesize: 0.8 MB
  • 19 pages

Document Identifiers

Author Details

Gioni Mexi
  • Zuse Institute Berlin, Germany
Timo Berthold
  • Fair Isaac Deutschland GmbH, Berlin, Germany
  • TU Berlin, Germany
Ambros Gleixner
  • HTW Berlin, Germany
  • Zuse Institute Berlin, Germany
Jakob Nordström
  • University of Copenhagen, Denmark
  • Lund University, Sweden

Funding

The work for this article has been conducted within the Research Campus Modal funded by the German Federal Ministry of Education and Research (BMBF grant numbers 05M14ZAM, 05M20ZBM).
  • Nordström, Jakob: supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B.

Acknowledgements

Part of this work was carried out while some of the authors participated in the extended reunion for the program Satisfiability: Theory, Practice, and Beyond at the Simons Institute for the Theory of Computing at UC Berkeley in the spring of 2023. This work has also benefited greatly from discussions during the Dagstuhl Seminar 22411 Theory and Practice of SAT and Combinatorial Solving.

Cite AsGet BibTex

Gioni Mexi, Timo Berthold, Ambros Gleixner, and Jakob Nordström. Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning. In 29th International Conference on Principles and Practice of Constraint Programming (CP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 280, pp. 27:1-27:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CP.2023.27

Abstract

Conflict analysis has been successfully generalized from Boolean satisfiability (SAT) solving to mixed integer programming (MIP) solvers, but although MIP solvers operate with general linear inequalities, the conflict analysis in MIP has been limited to reasoning with the more restricted class of clausal constraint. This is in contrast to how conflict analysis is performed in so-called pseudo-Boolean solving, where solvers can reason directly with 0-1 integer linear inequalities rather than with clausal constraints extracted from such inequalities. In this work, we investigate how pseudo-Boolean conflict analysis can be integrated in MIP solving, focusing on 0-1 integer linear programs (0-1 ILPs). Phrased in MIP terminology, conflict analysis can be understood as a sequence of linear combinations and cuts. We leverage this perspective to design a new conflict analysis algorithm based on mixed integer rounding (MIR) cuts, which theoretically dominates the state-of-the-art division-based method in pseudo-Boolean solving. We also report results from a first proof-of-concept implementation of different pseudo-Boolean conflict analysis methods in the open-source MIP solver SCIP. When evaluated on a large and diverse set of 0-1 ILP instances from MIPLIB2017, our new MIR-based conflict analysis outperforms both previous pseudo-Boolean methods and the clause-based method used in MIP. Our conclusion is that pseudo-Boolean conflict analysis in MIP is a promising research direction that merits further study, and that it might also make sense to investigate the use of such conflict analysis to generate stronger no-goods in constraint programming.

Subject Classification

ACM Subject Classification
  • Theory of computation → Discrete optimization
  • Mathematics of computing → Solvers
Keywords
  • Integer programming
  • pseudo-Boolean solving
  • conflict analysis
  • cutting planes proof system
  • mixed integer rounding
  • division
  • saturation

Metrics

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

References

  1. Tobias Achterberg. Conflict analysis in mixed integer programming. Discrete Optimization, 4(1):4-20, March 2007. Google Scholar
  2. Tobias Achterberg. Constraint Integer Programming. PhD thesis, Technische Universität Berlin, 2007. Available at URL: https://opus4.kobv.de/opus4-zib/files/1112/Achterberg_Constraint_Integer_Programming.pdf.
  3. Roberto J. Bayardo Jr. and Robert Schrag. Using CSP look-back techniques to solve real-world SAT instances. In Proceedings of the 14th National Conference on Artificial Intelligence (AAAI '97), pages 203-208, July 1997. Google Scholar
  4. Paul Beame, Henry Kautz, and Ashish Sabharwal. Towards understanding and harnessing the potential of clause learning. Journal of Artificial Intelligence Research, 22:319-351, December 2004. Preliminary version in IJCAI '03. Google Scholar
  5. Timo Berthold, Stefan Heinz, and Marc Pfetsch. Solving Pseudo-Boolean problems with SCIP, 2008. Google Scholar
  6. Timo Berthold, Stefan Heinz, and Marc E Pfetsch. Nonlinear Pseudo-Boolean optimization: relaxation or propagation? In Theory and Applications of Satisfiability Testing-SAT 2009: 12th International Conference, SAT 2009, Swansea, UK, June 30-July 3, 2009. Proceedings 12, pages 441-446. Springer, 2009. Google Scholar
  7. Ksenia Bestuzheva, Mathieu Besançon, Wei-Kun Chen, Antonia Chmiela, Tim Donkiewicz, Jasper van Doornmalen, Leon Eifler, Oliver Gaul, Gerald Gamrath, Ambros Gleixner, et al. The SCIP Optimization Suite 8.0. arXiv preprint arXiv:2112.08872, 2021. Google Scholar
  8. Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors. Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications. IOS Press, 2nd edition, February 2021. Google Scholar
  9. Archie Blake. Canonical Expressions in Boolean Algebra. PhD thesis, University of Chicago, 1937. Google Scholar
  10. AL Brearley, Gautam Mitra, and H Paul Williams. Analysis of mathematical programming problems prior to applying the simplex algorithm. Mathematical programming, 8:54-83, 1975. Google Scholar
  11. Samuel R. Buss and Jakob Nordström. Proof complexity and SAT solving. In Armin Biere, Marijn J. H. Heule, Hans van Maaren, and Toby Walsh, editors, Handbook of Satisfiability, volume 336 of Frontiers in Artificial Intelligence and Applications, chapter 7, pages 233-350. IOS Press, 2nd edition, February 2021. Google Scholar
  12. Donald Chai and Andreas Kuehlmann. A fast pseudo-Boolean constraint solver. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 24(3):305-317, March 2005. Preliminary version in DAC '03. Google Scholar
  13. Vasek Chvátal. Edmonds polytopes and a hierarchy of combinatorial problems. Discrete mathematics, 4(4):305-337, 1973. Google Scholar
  14. William Cook, Collette Rene Coullard, and György Turán. On the complexity of cutting-plane proofs. Discrete Applied Mathematics, 18(1):25-38, November 1987. Google Scholar
  15. Gérard Cornuéjols and Yanjun Li. Elementary closures for integer programs. Operations Research Letters, 28(1):1-8, 2001. URL: https://doi.org/10.1016/S0167-6377(00)00067-5.
  16. Martin Davis, George Logemann, and Donald Loveland. A machine program for theorem proving. Communications of the ACM, 5(7):394-397, July 1962. Google Scholar
  17. Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, 7(3):201-215, 1960. Google Scholar
  18. Theodorus Jozef Dekker. A floating-point technique for extending the available precision. Numerische Mathematik, 18(3):224-242, 1971. Google Scholar
  19. Jo Devriendt, Ambros Gleixner, and Jakob Nordström. Learn to relax: Integrating 0-1 integer linear programming with pseudo-Boolean conflict-driven search. Constraints, 26(1-4):26-55, October 2021. Preliminary version in CPAIOR '20. Google Scholar
  20. Jo Devriendt, Stephan Gocht, Emir Demirović, Jakob Nordström, and Peter Stuckey. Cutting to the core of pseudo-Boolean optimization: Combining core-guided search with cutting planes reasoning. In Proceedings of the 35th AAAI Conference on Artificial Intelligence (AAAI '21), pages 3750-3758, February 2021. Google Scholar
  21. Niklas Eén and Niklas Sörensson. Translating pseudo-Boolean constraints into SAT. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):1-26, March 2006. Google Scholar
  22. Jan Elffers, Jesús Giráldez-Cru, Jakob Nordström, and Marc Vinyals. Using combinatorial benchmarks to probe the reasoning power of pseudo-Boolean solvers. In Proceedings of the 21st International Conference on Theory and Applications of Satisfiability Testing (SAT '18), volume 10929 of Lecture Notes in Computer Science, pages 75-93. Springer, July 2018. Google Scholar
  23. Jan Elffers and Jakob Nordström. Divide and conquer: Towards faster pseudo-Boolean solving. In Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI '18), pages 1291-1299, July 2018. Google Scholar
  24. Matthew L Ginsberg. Dynamic backtracking. Journal of artificial intelligence research, 1:25-46, 1993. Google Scholar
  25. Ambros Gleixner, Gregor Hendel, Gerald Gamrath, Tobias Achterberg, Michael Bastubbe, Timo Berthold, Philipp M. Christophel, Kati Jarck, Thorsten Koch, Jeff Linderoth, Marco Lübbecke, Hans D. Mittelmann, Derya Ozyurt, Ted K. Ralphs, Domenico Salvagnin, and Yuji Shinano. MIPLIB 2017: Data-Driven Compilation of the 6th Mixed-Integer Programming Library. Mathematical Programming Computation, 13:443-490, 2021. URL: https://doi.org/10.1007/s12532-020-00194-3.
  26. Stephan Gocht, Jakob Nordström, and Amir Yehudayoff. On division versus saturation in pseudo-Boolean solving. In Proceedings of the 28th International Joint Conference on Artificial Intelligence (IJCAI '19), pages 1711-1718, August 2019. Google Scholar
  27. Ralph E. Gomory. An algorithm for the mixed integer problem. Technical Report P-1885, The RAND Corporation, June 1960. Google Scholar
  28. Armin Haken. The intractability of resolution. Theoretical Computer Science, 39(2-3):297-308, August 1985. Google Scholar
  29. John N. Hooker. Generalized resolution and cutting planes. Annals of Operations Research, 12(1):217-239, December 1988. Google Scholar
  30. John N. Hooker. Generalized resolution for 0-1 linear inequalities. Annals of Mathematics and Artificial Intelligence, 6(1):271-286, March 1992. Google Scholar
  31. Yuejun Jiang, Thomas Richards, and Barry Richards. Nogood backmarking with min-conflict repair in constraint satisfaction and optimization. In Principles and Practice of Constraint Programming: Second International Workshop, PPCP'94 Rosario, Orcas Island, WA, USA, May 2-4, 1994 Proceedings, pages 21-39. Springer, 1994. Google Scholar
  32. Dejan Jovanovic and Leonardo de Moura. Cutting to the chase solving linear integer arithmetic. Journal of Automated Reasoning, 51(1):79-108, June 2013. Preliminary version in CADE-23. Google Scholar
  33. Daniel Le Berre, Pierre Marquis, and Romain Wallon. On weakening strategies for PB solvers. In Proceedings of the 23rd International Conference on Theory and Applications of Satisfiability Testing (SAT '20), volume 12178 of Lecture Notes in Computer Science, pages 322-331. Springer, July 2020. Google Scholar
  34. Daniel Le Berre and Anne Parrain. The Sat4j library, release 2.2. Journal on Satisfiability, Boolean Modeling and Computation, 7:59-64, July 2010. Google Scholar
  35. Vincent Liew, Paul Beame, Jo Devriendt, Jan Elffers, and Jakob Nordström. Verifying properties of bit-vector multiplication using cutting planes reasoning. In Proceedings of the 20th Conference on Formal Methods in Computer-Aided Design (FMCAD '20), pages 194-204, September 2020. Google Scholar
  36. Andrea Lodi and Andrea Tramontani. Performance variability in mixed-integer programming. In Theory driven by influential applications, pages 1-12. INFORMS, 2013. Google Scholar
  37. Hugues Marchand and Laurence A Wolsey. Aggregation and mixed integer rounding to solve mips. Operations research, 49(3):363-371, 2001. Google Scholar
  38. João P. Marques-Silva and Karem A. Sakallah. GRASP: A search algorithm for propositional satisfiability. IEEE Transactions on Computers, 48(5):506-521, May 1999. Preliminary version in ICCAD '96. Google Scholar
  39. Ruben Martins, Vasco M. Manquinho, and Inês Lynce. Open-WBO: A modular MaxSAT solver. In Proceedings of the 17th International Conference on Theory and Applications of Satisfiability Testing (SAT '14), volume 8561 of Lecture Notes in Computer Science, pages 438-445. Springer, July 2014. Google Scholar
  40. 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 '01), pages 530-535, June 2001. Google Scholar
  41. Robert Nieuwenhuis. The IntSat method for integer linear programming. In Proceedings of the 20th International Conference on Principles and Practice of Constraint Programming (CP '14), volume 8656 of Lecture Notes in Computer Science, pages 574-589. Springer, September 2014. Google Scholar
  42. John Alan Robinson. A machine-oriented logic based on the resolution principle. Journal of the ACM, 12(1):23-41, January 1965. Google Scholar
  43. Masahiko Sakai and Hidetomo Nabeshima. Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers. IEICE Transactions on Information and Systems, 98-D(6):1121-1127, June 2015. Google Scholar
  44. Tuomas Sandholm and Robert Shields. Nogood learning for mixed integer programming. In Workshop on Hybrid Methods and Branching Rules in Combinatorial Optimization, Montréal, volume 20, pages 21-22, 2006. Google Scholar
  45. Buser Say, Jo Devriendt, Jakob Nordström, and Peter Stuckey. Theoretical and experimental results for planning with learned binarized neural network transition models. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP '20), volume 12333 of Lecture Notes in Computer Science, pages 917-934. Springer, September 2020. Google Scholar
  46. Hossein M. Sheini and Karem A. Sakallah. Pueblo: A hybrid pseudo-Boolean SAT solver. Journal on Satisfiability, Boolean Modeling and Computation, 2(1-4):165-189, March 2006. Preliminary version in DATE '05. Google Scholar
  47. Richard M Stallman and Gerald J Sussman. Forward reasoning and dependency-directed backtracking in a system for computer-aided circuit analysis. Artificial intelligence, 9(2):135-196, 1977. Google Scholar
  48. Jakob Witzig, Timo Berthold, and Stefan Heinz. Computational aspects of infeasibility analysis in mixed integer programming. Technical Report 19-54, ZIB, Takustr. 7, 14195 Berlin, 2019. Google Scholar
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