Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning

Authors

  • Jo Devriendt Lund University University of Copenhagen KU Leuven
  • Stephan Gocht Lund University University of Copenhagen
  • Emir Demirović Delft University of Technology
  • Jakob Nordström University of Copenhagen Lund University
  • Peter J. Stuckey Monash University

DOI:

https://doi.org/10.1609/aaai.v35i5.16492

Keywords:

Constraint Optimization, Satisfiability, Solvers and Tools, Search

Abstract

Core-guided techniques have revolutionized Boolean satisfiability approaches to optimization problems (MaxSAT), but the process at the heart of these methods, strengthening bounds on solutions by repeatedly adding cardinality constraints, remains a bottleneck. Cardinality constraints require significant work to be re-encoded to SAT, and SAT solvers are notoriously weak at cardinality reasoning. In this work, we lift core-guided search to pseudo-Boolean (PB) solvers, which deal with more general PB optimization problems and operate natively with cardinality constraints. The cutting planes method used in such solvers allows us to derive stronger cardinality constraints, which yield better updates to solution bounds, and the increased efficiency of objective function reformulation also makes it feasible to switch repeatedly between lower-bounding and upper- bounding search. A thorough evaluation on applied and crafted benchmarks shows that our core-guided PB solver significantly improves on the state of the art in pseudo-Boolean optimization.

Downloads

Published

2021-05-18

How to Cite

Devriendt, J., Gocht, S., Demirović, E., Nordström, J., & Stuckey, P. J. (2021). Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning. Proceedings of the AAAI Conference on Artificial Intelligence, 35(5), 3750-3758. https://doi.org/10.1609/aaai.v35i5.16492

Issue

Section

AAAI Technical Track on Constraint Satisfaction and Optimization