Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

Learn to relax : Integrating 0-1 integer linear programming with pseudo-Boolean conflict-driven search

Devriendt, Jo LU ; Gleixner, Ambros and Nordström, Jakob LU (2021) In Constraints 26(44565). p.26-55
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... (More)

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.

(Less)
Please use this url to cite or link to this publication:
author
; and
organization
publishing date
type
Contribution to journal
publication status
published
subject
keywords
Conflict-driven search, Cut generation, Cutting plane proofs, Integer Programming, Linear Programming, Pseudo-Boolean, RoundingSat
in
Constraints
volume
26
issue
44565
pages
26 - 55
publisher
Springer
external identifiers
  • scopus:85100195550
ISSN
1383-7133
DOI
10.1007/s10601-020-09318-x
language
English
LU publication?
yes
id
e4218a40-cead-45f7-a954-9fa54c847136
date added to LUP
2021-02-12 12:58:37
date last changed
2022-05-12 18:19:34
@article{e4218a40-cead-45f7-a954-9fa54c847136,
  abstract     = {{<p>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.</p>}},
  author       = {{Devriendt, Jo and Gleixner, Ambros and Nordström, Jakob}},
  issn         = {{1383-7133}},
  keywords     = {{Conflict-driven search; Cut generation; Cutting plane proofs; Integer Programming; Linear Programming; Pseudo-Boolean; RoundingSat}},
  language     = {{eng}},
  month        = {{01}},
  number       = {{44565}},
  pages        = {{26--55}},
  publisher    = {{Springer}},
  series       = {{Constraints}},
  title        = {{Learn to relax : Integrating 0-1 integer linear programming with pseudo-Boolean conflict-driven search}},
  url          = {{http://dx.doi.org/10.1007/s10601-020-09318-x}},
  doi          = {{10.1007/s10601-020-09318-x}},
  volume       = {{26}},
  year         = {{2021}},
}