2026-07-24T09:32:19Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:16687 2024-03-06T10:58:03Z ddc:004 open_access

Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization Smirnov, Pavel Berg, Jeremias Järvisalo, Matti constraint optimization pseudo-Boolean optimization implicit hitting sets solution-improving search unsatisfiable cores The development of practical approaches to efficiently reasoning over pseudo-Boolean constraints has recently increasing attention as a natural generalization of Boolean satisfiability (SAT) solving. Analogously, solvers for pseudo-Boolean optimization draw inspiration from techniques developed for maximum satisfiability (MaxSAT) solving. Recently, the first practical solver lifting the implicit hitting set (IHS) approach - one of the most efficient approaches in modern MaxSAT solving - to the realm of PBO was developed, employing a PB solver as a core extractor together with an integer programming solver as a hitting set solver. In this work, we make practical improvements to the IHS approach to PBO. We propose the integration of solution-improving search to the PBO-IHS approach, resulting in a hybrid approach to PBO which makes use of both types of search towards an optimal solution. Furthermore, we explore the potential of different variants of core extraction within PBO-IHS - including recent advances in PB core extraction, allowing for extracting more general PB constraints compared to the at-least-one constraints typically relied on in IHS - in speeding up PBO-IHS search. We show that the empirical efficiency of PBO-IHS - recently shown to outperform other specialized PBO solvers - is further improved by the integration of these techniques. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Pavel Smirnov and Jeremias Berg and Matti Järvisalo 2022 Is Part Of LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.SAT.2022.13 urn:nbn:de:0030-drops-166871 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.13 eng https://creativecommons.org/licenses/by/4.0/legalcode