IntSat: integer linear programming by conflict-driven constraint learning

References

• T. Achterberg, Conflict analysis in mixed integer programming, Disc. Optim. 4 (2007), pp. 4–20.
   Web of Science ®Google Scholar
• R. Asín, M. Bezem, and R. Nieuwenhuis, Improving intsat by expressing disjunctions of bounds as linear constraints, AI Commun. 29 (2016), pp. 205–209.
   Web of Science ®Google Scholar
• B. Aspvall, M.F. Plass, and R.E. Tarjan, A linear-time algorithm for testing the truth of certain quantified Boolean formulas, Inf. Process. Lett. 8 (1979), pp. 121–123.
   Web of Science ®Google Scholar
• G. Audemard and L. Simon, Predicting Learnt Clauses Quality in Modern SAT Solvers, in Proceedings of the 21st International. Joint Conference on Artificial Intelligence, Morgan Kaufmann Publishers Inc., IJCAI '09, San Francisco, CA, USA, 2009, pp. 399–404.
   Google Scholar
• A. Biere, M.J.H. Heule, H. van Maaren, and T. Walsh (eds.), Handbook of Satisfiability, Frontiers in Artificial Intelligence and Applications, Vol. 185, IOS Press, 2009 February.
   Google Scholar
• R. Bixby, Optimization: Past, Present and Future with Dr. Robert Bixby (2021). Available at https://www.youtube.com/watch?v=_R8-nt5NyiE.
   Google Scholar
• A.L. Brearley, G. Mitra, and H.P. Williams, Analysis of mathematical programming problems prior to applying the simplex algorithm, Math. Program 8 (1975), pp. 54–83.
   Web of Science ®Google Scholar
• M. Bromberger, A Reduction from Unbounded Linear Mixed Arithmetic Problems into Bounded Problems, in Automated Reasoning–9th International Joint Conference, IJCAR 2018, D. Galmiche, S. Schulz, and R. Sebastiani, eds., LNCS Vol. 10900, Springer, 2018, pp. 329–345.
   Google Scholar
• M. Bromberger, T. Sturm, and C. Weidenbach, A complete and terminating approach to linear integer solving, J. Symb. Comput. 100 (2020), pp. 102–136.
   Web of Science ®Google Scholar
• H. Brown, L. Zuo, and D. Gusfield, Comparing Integer Linear Programming to SAT-Solving for Hard Problems in Computational and Systems Biology, in AlCoB, LNCS Vol. 12099, Springer, 2020, pp. 63–76.
   Google Scholar
• D. Chai and A. Kuehlmann, A fast pseudo-Boolean constraint solver, IEEE Trans. CAD Integr Circuits Syst 24 (2005), pp. 305–317.
   Web of Science ®Google Scholar
• S.A. Cook, The Complexity of Theorem-Proving Procedures, in Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC '71, ACM, NY, USA, 1971, pp. 151–158.
   Google Scholar
• M. Davis, G. Logemann, and D. Loveland, A machine program for theorem-proving, Commun. ACM 5 (1962), pp. 394–397.
   Web of Science ®Google Scholar
• M. Davis and H. Putnam, A computing procedure for quantification theory, J. ACM 7 (1960), pp. 201–215.
   Web of Science ®Google Scholar
• J. Elffers and J. Nordström, Divide and Conquer: Towards Faster Pseudo-Boolean Solving, in Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI 2018, July 13–19, 2018, Stockholm, Sweden, J. Lang, ed., ijcai.org, 2018, pp. 1291–1299.
   Google Scholar
• A. Haken, The intractability of resolution, Theor. Comput. Sci. 39 (1985), pp. 297–308.
   Web of Science ®Google Scholar
• D. Jovanovic and L.M. de Moura, Cutting to the chase–solving linear integer arithmetic, J. Autom. Reasoning 51 (2013), pp. 79–108.
   Google Scholar
• R. Nieuwenhuis, The IntSat Method for Integer Linear Programming, in Principles and Practice of Constraint Programming, 20th Int. Conf., CP'14, LNCS 8656. 2014, pp. 574–589.
   Google Scholar
• R. Nieuwenhuis, A. Oliveras, and C. Tinelli, Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T), J. ACM 53 (2006), pp. 937–977.
   Web of Science ®Google Scholar
• K. Pipatsrisawat and A. Darwiche, On the Power of Clause-Learning SAT Solvers with Restarts, in Principles and Practice of Constraint Programming, 15th Int. Conf., CP '09, LNCS Vol. 5732, Springer, 2009, pp. 654–668.
   Google Scholar
• J. Witzig, T. Berthold, and S. Heinz, Experiments with Conflict Analysis in Mixed Integer Programming, in Integration of AI and OR Techniques in Constraint Programming–14th International Conference, CPAIOR 2017, Padua, Italy, June 5-8, 2017, Proceedings, D. Salvagnin and M. Lombardi, eds., Lecture Notes in Computer Science Vol. 10335, Springer, 2017, pp. 211–220.
   Google Scholar
• J. Witzig, T. Berthold, and S. Heinz, Computational aspects of infeasibility analysis in mixed integer programming, Math. Program. Comput. 13 (2021), pp. 753–785.
   Web of Science ®Google Scholar