Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning - Devriendt, Jo; Gocht, Stephan; Demirović, Emir; Nordström, Jakob; Stuckey, Peter J. (Proceedings of the AAAI Conference on Artificial Intelligence, 2021)
Core-guided techniques have revolutionized Boolean satisfiabilityapproaches to optimization problems (MaxSAT), but the process atthe heart of these methods, strengthening bounds on solutions byrepeatedly adding cardinality constraints, remains a bottleneck.Cardinality constraints require significant work to be re-encoded toSAT, 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 problemsand operate natively with cardinality constraints. The cutting planesmethod used in such solvers allows us to derive stronger cardinalityconstraints, which yield better updates to solution bounds, and theincreased efficiency of objective function reformulation also makes itfeasible to switch repeatedly between lower-bounding and upper-bounding search. A thorough evaluation on applied and craftedbenchmarks shows that our core-guided PB solver significantlyimproves on the state of the art in pseudo-Boolean optimization.