@article{WeberSagerGleixner2019, author = {Weber, Tobias and Sager, Sebastian and Gleixner, Ambros}, title = {Solving Quadratic Programs to High Precision using Scaled Iterative Refinement}, volume = {11}, journal = {Mathematical Programming Computation}, publisher = {Springer Berlin Heidelberg}, doi = {10.1007/s12532-019-00154-6}, pages = {421 -- 455}, year = {2019}, abstract = {Quadratic optimization problems (QPs) are ubiquitous, and solution algorithms have matured to a reliable technology. However, the precision of solutions is usually limited due to the underlying floating-point operations. This may cause inconveniences when solutions are used for rigorous reasoning. We contribute on three levels to overcome this issue. First, we present a novel refinement algorithm to solve QPs to arbitrary precision. It iteratively solves refined QPs, assuming a floating-point QP solver oracle. We prove linear convergence of residuals and primal errors. Second, we provide an efficient implementation, based on SoPlex and qpOASES that is publicly available in source code. Third, we give precise reference solutions for the Maros and M{\´e}sz{\´a}ros benchmark library.}, language = {en} } @misc{EiflerGleixnerPulaj2021, author = {Eifler, Leon and Gleixner, Ambros and Pulaj, Jonad}, title = {A Safe Computational Framework for Integer Programming applied to Chv{\´a}tal's Conjecture}, issn = {1438-0064}, url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-84444}, year = {2021}, abstract = {We describe a general and safe computational framework that provides integer programming results with the degree of certainty that is required for machine-assisted proofs of mathematical theorems. At its core, the framework relies on a rational branch-and-bound certificate produced by an exact integer programming solver, SCIP, in order to circumvent floating-point roundoff errors present in most state-of-the-art solvers for mixed-integer programs. The resulting certificates are self-contained and checker software exists that can verify their correctness independently of the integer programming solver used to produce the certificate. This acts as a safeguard against programming errors that may be present in complex solver software. The viability of this approach is tested by applying it to finite cases of Chv{\´a}tal's conjecture, a long-standing open question in extremal combinatorics. We take particular care to verify also the correctness of the input for this specific problem, using the Coq formal proof assistant. As a result we are able to provide a first machine-assisted proof that Chv{\´a}tal's conjecture holds for all downsets whose union of sets contains seven elements or less.}, language = {en} } @article{EiflerGleixnerPulaj2022, author = {Eifler, Leon and Gleixner, Ambros and Pulaj, Jonad}, title = {A Safe Computational Framework for Integer Programming applied to Chv{\´a}tal's Conjecture}, volume = {48}, journal = {ACM Transactions on Mathematical Software}, number = {2}, doi = {10.1145/3485630}, year = {2022}, abstract = {We describe a general and safe computational framework that provides integer programming results with the degree of certainty that is required for machine-assisted proofs of mathematical theorems. At its core, the framework relies on a rational branch-and-bound certificate produced by an exact integer programming solver, SCIP, in order to circumvent floating-point roundoff errors present in most state-of-the-art solvers for mixed-integer programs.The resulting certificates are self-contained and checker software exists that can verify their correctness independently of the integer programming solver used to produce the certificate. This acts as a safeguard against programming errors that may be present in complex solver software. The viability of this approach is tested by applying it to finite cases of Chv{\´a}tal's conjecture, a long-standing open question in extremal combinatorics. We take particular care to verify also the correctness of the input for this specific problem, using the Coq formal proof assistant. As a result we are able to provide a first machine-assisted proof that Chv{\´a}tal's conjecture holds for all downsets whose union of sets contains seven elements or less.}, language = {en} } @article{EiflerGleixner2022, author = {Eifler, Leon and Gleixner, Ambros}, title = {A computational status update for exact rational mixed integer programming}, journal = {Mathematical Programming}, publisher = {Springer}, doi = {10.1007/s10107-021-01749-5}, year = {2022}, abstract = {The last milestone achievement for the roundoff-error-free solution of general mixed integer programs over the rational numbers was a hybrid-precision branch-and-bound algorithm published by Cook, Koch, Steffy, and Wolter in 2013. We describe a substantial revision and extension of this framework that integrates symbolic presolving, features an exact repair step for solutions from primal heuristics, employs a faster rational LP solver based on LP iterative refinement, and is able to produce independently verifiable certificates of optimality. We study the significantly improved performance and give insights into the computational behavior of the new algorithmic components. On the MIPLIB 2017 benchmark set, we observe an average speedup of 10.7x over the original framework and 2.9 times as many instances solved within a time limit of two hours.}, language = {en} } @article{EiflerNicolasThouveninGleixner2024, author = {Eifler, Leon and Nicolas-Thouvenin, Jules and Gleixner, Ambros}, title = {Combining Precision Boosting with LP Iterative Refinement for Exact Linear Optimization}, journal = {INFORMS Journal on Computing}, doi = {10.1287/ijoc.2023.0409}, year = {2024}, abstract = {This article studies a combination of the two state-of-the-art algorithms for the exact solution of linear programs (LPs) over the rational numbers, i.e., without any roundoff errors or numerical tolerances. By integrating the method of precision boosting inside an LP iterative refinement loop, the combined algorithm is able to leverage the strengths of both methods: the speed of LP iterative refinement, in particular in the majority of cases when a double-precision floating-point solver is able to compute approximate solutions with small errors, and the robustness of precision boosting whenever extended levels of precision become necessary. We compare the practical performance of the resulting algorithm with both puremethods on a large set of LPs and mixed-integer programs (MIPs). The results show that the combined algorithm solves more instances than a pure LP iterative refinement approach, while being faster than pure precision boosting. When embedded in an exact branch-and-cut framework for MIPs, the combined algorithm is able to reduce the number of failed calls to the exact LP solver to zero, while maintaining the speed of the pure LP iterative refinement approach.}, language = {en} } @misc{EiflerNicolasThouveninGleixner2023, author = {Eifler, Leon and Nicolas-Thouvenin, Jules and Gleixner, Ambros}, title = {Combining Precision Boosting with LP Iterative Refinement for Exact Linear Optimization}, issn = {1438-0064}, url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-92573}, year = {2023}, abstract = {This article studies a combination of the two state-of-the-art algorithms for the exact solution of linear programs (LPs) over the rational numbers, i.e., without any roundoff errors or numerical tolerances. By integrating the method of precision boosting inside an LP iterative refinement loop, the combined algorithm is able to leverage the strengths of both methods: the speed of LP iterative refinement, in particular in the majority of cases when a double-precision floating-point solver is able to compute approximate solutions with small errors, and the robustness of precision boosting whenever extended levels of precision become necessary. We compare the practical performance of the resulting algorithm with both puremethods on a large set of LPs and mixed-integer programs (MIPs). The results show that the combined algorithm solves more instances than a pure LP iterative refinement approach, while being faster than pure precision boosting. When embedded in an exact branch-and-cut framework for MIPs, the combined algorithm is able to reduce the number of failed calls to the exact LP solver to zero, while maintaining the speed of the pure LP iterative refinement approach.}, language = {en} } @article{BolusaniBesanconGleixneretal.2024, author = {Bolusani, Suresh and Besan{\c{c}}on, Mathieu and Gleixner, Ambros and Berthold, Timo and D'Ambrosio, Claudia and Mu{\~n}oz, Gonzalo and Paat, Joseph and Thomopulos, Dimitri}, title = {The MIP workshop 2023 computational competition on reoptimization}, volume = {16}, journal = {Mathematical Programming Computation}, doi = {10.1007/s12532-024-00256-w}, pages = {255 -- 266}, year = {2024}, abstract = {This paper describes the computational challenge developed for a computational competition held in 2023 for the 20th anniversary of the Mixed Integer Programming Workshop. The topic of this competition was reoptimization, also known as warm starting, of mixed integer linear optimization problems after slight changes to the input data for a common formulation. The challenge was to accelerate the proof of optimality of the modified instances by leveraging the information from the solving processes of previously solved instances, all while creating high-quality primal solutions. Specifically, we discuss the competition's format, the creation of public and hidden datasets, and the evaluation criteria. Our goal is to establish a methodology for the generation of benchmark instances and an evaluation framework, along with benchmark datasets, to foster future research on reoptimization of mixed integer linear optimization problems.}, language = {en} } @inproceedings{EiflerWitzigGleixner2024, author = {Eifler, Leon and Witzig, Jakob and Gleixner, Ambros}, title = {Branch and cut for partitioning a graph into a cycle of clusters}, volume = {14594}, booktitle = {Combinatorial Optimization. ISCO 2024}, doi = {10.1007/978-3-031-60924-4_8}, pages = {97 -- 108}, year = {2024}, abstract = {In this paper we study formulations and algorithms for the cycle clustering problem, a partitioning problem over the vertex set of a directed graph with nonnegative arc weights that is used to identify cyclic behavior in simulation data generated from nonreversible Markov state models. Here, in addition to partitioning the vertices into a set of coherent clusters, the resulting clusters must be ordered into a cycle such as to maximize the total net flow in the forward direction of the cycle. We provide a problem-specific binary programming formulation and compare it to a formulation based on the reformulation-linearization technique (RLT). We present theoretical results on the polytope associated with our custom formulation and develop primal heuristics and separation routines for both formulations. In computational experiments on simulation data from biology we find that branch and cut based on the problem-specific formulation outperforms the one based on RLT.}, language = {en} } @inproceedings{GhannamMexiLametal.2024, author = {Ghannam, Mohammed and Mexi, Gioni and Lam, Edward and Gleixner, Ambros}, title = {Branch and price for the length-constrained cycle partition problem}, booktitle = {Proceedings of INFORMS Optimization Society Conference}, year = {2024}, language = {en} } @inproceedings{BestuzhevaGleixnerAchterberg2023, author = {Bestuzheva, Ksenia and Gleixner, Ambros and Achterberg, Tobias}, title = {Efficient Separation of RLT Cuts for Implicit and Explicit Bilinear Products}, volume = {13904}, booktitle = {Integer Programming and Combinatorial Optimization. IPCO 2023.}, publisher = {Springer, Cham}, doi = {10.1007/978-3-031-32726-1_2}, pages = {14 -- 28}, year = {2023}, abstract = {The reformulation-linearization technique (RLT) is a prominent approach to constructing tight linear relaxations of non-convex continuous and mixed-integer optimization problems. The goal of this paper is to extend the applicability and improve the performance of RLT for bilinear product relations. First, a method for detecting bilinear product relations implicitly contained in mixed-integer linear programs is developed based on analyzing linear constraints with binary variables, thus enabling the application of bilinear RLT to a new class of problems. Our second contribution addresses the high computational cost of RLT cut separation, which presents one of the major difficulties in applying RLT efficiently in practice. We propose a new RLT cutting plane separation algorithm which identifies combinations of linear constraints and bound factors that are expected to yield an inequality that is violated by the current relaxation solution. A detailed computational study based on implementations in two solvers evaluates the performance impact of the proposed methods.}, language = {en} } @inproceedings{MexiBertholdGleixneretal.2023, author = {Mexi, Gioni and Berthold, Timo and Gleixner, Ambros and Nordstr{\"o}m, Jakob}, title = {Improving Conflict Analysis in MIP Solvers by Pseudo-Boolean Reasoning}, volume = {280}, booktitle = {29th International Conference on Principles and Practice of Constraint Programming (CP 2023)}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik}, doi = {10.4230/LIPIcs.CP.2023.27}, pages = {27:1 -- 27:19}, year = {2023}, 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.}, language = {en} } @article{BestuzhevaGleixnerVigerske2023, author = {Bestuzheva, Ksenia and Gleixner, Ambros and Vigerske, Stefan}, title = {A Computational Study of Perspective Cuts}, volume = {15}, journal = {Mathematical Programming Computation}, doi = {10.1007/s12532-023-00246-4}, pages = {703 -- 731}, year = {2023}, abstract = {The benefits of cutting planes based on the perspective function are well known for many specific classes of mixed-integer nonlinear programs with on/off structures. However, we are not aware of any empirical studies that evaluate their applicability and computational impact over large, heterogeneous test sets in general-purpose solvers. This paper provides a detailed computational study of perspective cuts within a linear programming based branch-and-cut solver for general mixed-integer nonlinear programs. Within this study, we extend the applicability of perspective cuts from convex to nonconvex nonlinearities. This generalization is achieved by applying a perspective strengthening to valid linear inequalities which separate solutions of linear relaxations. The resulting method can be applied to any constraint where all variables appearing in nonlinear terms are semi-continuous and depend on at least one common indicator variable. Our computational experiments show that adding perspective cuts for convex constraints yields a consistent improvement of performance, and adding perspective cuts for nonconvex constraints reduces branch-and-bound tree sizes and strengthens the root node relaxation, but has no significant impact on the overall mean time.}, language = {en} } @article{GemanderChenWeningeretal.2020, author = {Gemander, Patrick and Chen, Wei-Kun and Weninger, Dieter and Gottwald, Leona and Gleixner, Ambros}, title = {Two-row and two-column mixed-integer presolve using hashing-based pairing methods}, volume = {8}, journal = {EURO Journal on Computational Optimization}, number = {3-4}, doi = {10.1007/s13675-020-00129-6}, pages = {205 -- 240}, year = {2020}, abstract = {In state-of-the-art mixed-integer programming solvers, a large array of reduction techniques are applied to simplify the problem and strengthen the model formulation before starting the actual branch-and-cut phase. Despite their mathematical simplicity, these methods can have significant impact on the solvability of a given problem. However, a crucial property for employing presolve techniques successfully is their speed. Hence, most methods inspect constraints or variables individually in order to guarantee linear complexity. In this paper, we present new hashing-based pairing mechanisms that help to overcome known performance limitations of more powerful presolve techniques that consider pairs of rows or columns. Additionally, we develop an enhancement to one of these presolve techniques by exploiting the presence of set-packing structures on binary variables in order to strengthen the resulting reductions without increasing runtime. We analyze the impact of these methods on the MIPLIB 2017 benchmark set based on an implementation in the MIP solver SCIP.}, language = {en} } @article{EiflerGleixner2023, author = {Eifler, Leon and Gleixner, Ambros}, title = {Safe and Verified Gomory Mixed Integer Cuts in a Rational MIP Framework}, volume = {34}, journal = {SIAM Journal on Optimization}, number = {1}, doi = {10.1137/23M156046X}, year = {2023}, abstract = {This paper is concerned with the exact solution of mixed-integer programs (MIPs) over the rational numbers, i.e., without any roundoff errors and error tolerances. Here, one computational bottleneck that should be avoided whenever possible is to employ large-scale symbolic computations. Instead it is often possible to use safe directed rounding methods, e.g., to generate provably correct dual bounds. In this work, we continue to leverage this paradigm and extend an exact branch-and-bound framework by separation routines for safe cutting planes, based on the approach first introduced by Cook, Dash, Fukasawa, and Goycoolea in 2009. Constraints are aggregated safely using approximate dual multipliers from an LP solve, followed by mixed-integer rounding to generate provably valid, although slightly weaker inequalities. We generalize this approach to problem data that is not representable in floating-point arithmetic, add routines for controlling the encoding length of the resulting cutting planes, and show how these cutting planes can be verified according to the VIPR certificate standard. Furthermore, we analyze the performance impact of these cutting planes in the context of an exact MIP framework, showing that we can solve 21.5\% more instances and reduce solving times by 26.8\% on the MIPLIB 2017 benchmark test set.}, language = {en} } @misc{EiflerGleixner2023, author = {Eifler, Leon and Gleixner, Ambros}, title = {Safe and Verified Gomory Mixed Integer Cuts in a Rational MIP Framework}, issn = {1438-0064}, url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-90159}, year = {2023}, abstract = {This paper is concerned with the exact solution of mixed-integer programs (MIPs) over the rational numbers, i.e., without any roundoff errors and error tolerances. Here, one computational bottleneck that should be avoided whenever possible is to employ large-scale symbolic computations. Instead it is often possible to use safe directed rounding methods, e.g., to generate provably correct dual bounds. In this work, we continue to leverage this paradigm and extend an exact branch-and-bound framework by separation routines for safe cutting planes, based on the approach first introduced by Cook, Dash, Fukasawa, and Goycoolea in 2009. Constraints are aggregated safely using approximate dual multipliers from an LP solve, followed by mixed-integer rounding to generate provably valid, although slightly weaker inequalities. We generalize this approach to problem data that is not representable in floating-point arithmetic, add routines for controlling the encoding length of the resulting cutting planes, and show how these cutting planes can be verified according to the VIPR certificate standard. Furthermore, we analyze the performance impact of these cutting planes in the context of an exact MIP framework, showing that we can solve 21.5\% more instances and reduce solving times by 26.8\% on the MIPLIB 2017 benchmark test set.}, language = {en} } @misc{BestuzhevaGleixnerVigerske2021, author = {Bestuzheva, Ksenia and Gleixner, Ambros and Vigerske, Stefan}, title = {A Computational Study of Perspective Cuts}, issn = {1438-0064}, url = {http://nbn-resolving.de/urn:nbn:de:0297-zib-81821}, year = {2021}, abstract = {The benefits of cutting planes based on the perspective function are well known for many specific classes of mixed-integer nonlinear programs with on/off structures. However, we are not aware of any empirical studies that evaluate their applicability and computational impact over large, heterogeneous test sets in general-purpose solvers. This paper provides a detailed computational study of perspective cuts within a linear programming based branch-and-cut solver for general mixed-integer nonlinear programs. Within this study, we extend the applicability of perspective cuts from convex to nonconvex nonlinearities. This generalization is achieved by applying a perspective strengthening to valid linear inequalities which separate solutions of linear relaxations. The resulting method can be applied to any constraint where all variables appearing in nonlinear terms are semi-continuous and depend on at least one common indicator variable. Our computational experiments show that adding perspective cuts for convex constraints yields a consistent improvement of performance, and adding perspective cuts for nonconvex constraints reduces branch-and-bound tree sizes and strengthens the root node relaxation, but has no significant impact on the overall mean time.}, language = {en} } @article{DevriendtGleixnerNordstroem2021, author = {Devriendt, Jo and Gleixner, Ambros and Nordstr{\"o}m, Jakob}, title = {Learn to Relax: Integrating 0-1 Integer Linear Programming with Pseudo-Boolean Conflict-Driven Search}, volume = {26}, journal = {Constraints}, doi = {10.1007/s10601-020-09318-x}, pages = {26 -- 55}, year = {2021}, abstract = {Conflict-driven pseudo-Boolean solvers optimize 0-1 integer linear programs by extending the conflict-driven clause learning (CDCL) paradigm from SAT solving. Though pseudo-Boolean solvers have the potential to be exponentially more efficient than CDCL solvers in theory, in practice they can sometimes get hopelessly stuck even when the linear programming (LP) relaxation is infeasible over the reals. Inspired by mixed integer programming (MIP), we address this problem by interleaving incremental LP solving with cut generation within the conflict-driven pseudo-Boolean search. This hybrid approach, which for the first time combines MIP techniques with full-blown conflict analysis operating directly on linear inequalities using the cutting planes method, significantly improves performance on a wide range of benchmarks, approaching a "best-of-both-worlds" scenario between SAT-style conflict-driven search and MIP-style branch-and-cut.}, language = {en} } @article{ŠofranacGleixnerPokutta2022, author = {Šofranac, Boro and Gleixner, Ambros and Pokutta, Sebastian}, title = {An Algorithm-independent Measure of Progress for Linear Constraint Propagation}, volume = {27}, journal = {Constraints}, doi = {10.1007/s10601-022-09338-9}, pages = {432 -- 455}, year = {2022}, language = {en} } @article{EiflerGleixner2024, author = {Eifler, Leon and Gleixner, Ambros}, title = {Safe and verified Gomory mixed integer cuts in a rational MIP framework}, volume = {34}, journal = {SIAM Journal on Optimization}, number = {1}, doi = {10.1137/23M156046X}, year = {2024}, abstract = {This paper is concerned with the exact solution of mixed-integer programs (MIPs) over the rational numbers, i.e., without any roundoff errors and error tolerances. Here, one computational bottleneck that should be avoided whenever possible is to employ large-scale symbolic computations. Instead it is often possible to use safe directed rounding methods, e.g., to generate provably correct dual bounds. In this work, we continue to leverage this paradigm and extend an exact branch-and-bound framework by separation routines for safe cutting planes, based on the approach first introduced by Cook, Dash, Fukasawa, and Goycoolea in 2009 [INFORMS J. Comput., 21 (2009), pp. 641-649]. Constraints are aggregated safely using approximate dual multipliers from an LP solve, followed by mixed-integer rounding to generate provably valid, although slightly weaker inequalities. We generalize this approach to problem data that is not representable in floating-point arithmetic, add routines for controlling the encoding length of the resulting cutting planes, and show how these cutting planes can be verified according to the VIPR certificate standard. Furthermore, we analyze the performance impact of these cutting planes in the context of an exact MIP framework, showing that we can solve 21.5\% more instances to exact optimality and reduce solving times by 26.8\% on the MIPLIB 2017 benchmark test set.}, language = {en} } @inproceedings{GhannamGleixner2023, author = {Ghannam, Mohammed and Gleixner, Ambros}, title = {Hybrid genetic search for dynamic vehicle routing with time windows}, booktitle = {Proceedings of Conference of the Society for Operations Research in Germany}, year = {2023}, language = {en} } @inproceedings{HoenOertelGleixneretal.2024, author = {Hoen, Alexander and Oertel, Andy and Gleixner, Ambros and Nordstr{\"o}m, Jakob}, title = {Certifying MIP-based presolve reductions for 0-1 integer linear programs}, volume = {14742}, booktitle = {Integration of Constraint Programming, Artificial Intelligence, and Operations Research. CPAIOR 2024}, doi = {10.1007/978-3-031-60597-0_20}, year = {2024}, abstract = {It is well known that reformulating the original problem can be crucial for the performance of mixed-integer programming (MIP) solvers. To ensure correctness, all transformations must preserve the feasibility status and optimal value of the problem, but there is currently no established methodology to express and verify the equivalence of two mixed-integer programs. In this work, we take a first step in this direction by showing how the correctness of MIP presolve reductions on - integer linear programs can be certified by using (and suitably extending) the VeriPB tool for pseudo-Boolean proof logging. Our experimental evaluation on both decision and optimization instances demonstrates the computational viability of the approach and leads to suggestions for future revisions of the proof format that will help to reduce the verbosity of the certificates and to accelerate the certification and verification process further.}, language = {en} }