Journal
CONSTRAINTS
Volume 26, Issue 1-4, Pages 26-55Publisher
SPRINGER
DOI: 10.1007/s10601-020-09318-x
Keywords
Pseudo-Boolean; Conflict-driven search; Cutting plane proofs; Integer Programming; Linear Programming; Cut generation; RoundingSat
Funding
- Swedish Research Council [2016-00782]
- Independent Research Fund Denmark [9040-00389B]
- Research Campus MODAL - German Federal Ministry of Education and Research (BMBF) [05M14ZAM, 05M20ZBM]
- National Science Foundation
Ask authors/readers for more resources
Inspired by mixed integer programming, a hybrid approach is proposed in this research that combines incremental LP solving with cut generation within the conflict-driven pseudo-Boolean search, significantly improving performance on a wide range of benchmarks. This approach marks the first time that MIP techniques are combined with full-blown conflict analysis operating directly on linear inequalities using the cutting planes method.
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.
Authors
I am an author on this paper
Click your name to claim this paper and add it to your profile.
Reviews
Recommended
No Data Available