TITLE:
Learn to Relax: Integrating Integer Linear Programming with Conflict-Driven Search

 

ABSTRACT:
Pseudo-Boolean (PB) solvers optimize 0-1 integer linear programs by
extending the conflict-driven learning paradigm from SAT solving.
Though PB solvers should be exponentially more efficient than SAT
solvers in theory, in practice they can sometimes get hopelessly stuck
even when the relaxed linear program (LP) 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 PB search.  This hybrid approach, which for
the first time combines MIP techniques with full-blown conflict
analysis over linear inequalities using the cutting planes method,
significantly improves performance on a wide range of benchmarks,
approaching a “best of two worlds” scenario between SAT-style
conflict-driven search and MIP-style branch-and-cut.