License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.SAT.2022.13
URN: urn:nbn:de:0030-drops-166871
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16687/
Go to the corresponding LIPIcs Volume Portal

Smirnov, Pavel ; Berg, Jeremias ; Järvisalo, Matti

Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization

pdf-format:
LIPIcs-SAT-2022-13.pdf (1 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{smirnov_et_al:LIPIcs.SAT.2022.13,
  author =	{Smirnov, Pavel and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization}},
  booktitle =	{25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)},
  pages =	{13:1--13:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-242-6},
  ISSN =	{1868-8969},
  year =	{2022},
  volume =	{236},
  editor =	{Meel, Kuldeep S. and Strichman, Ofer},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2022/16687},
  URN =		{urn:nbn:de:0030-drops-166871},
  doi =		{10.4230/LIPIcs.SAT.2022.13},
  annote =	{Keywords: constraint optimization, pseudo-Boolean optimization, implicit hitting sets, solution-improving search, unsatisfiable cores}
}

Keywords: constraint optimization, pseudo-Boolean optimization, implicit hitting sets, solution-improving search, unsatisfiable cores
Collection: 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)
Issue Date: 2022
Date of publication: 28.07.2022
Supplementary Material: Software (Source Code and Experiment Data): https://bitbucket.org/coreo-group/pbo-ihs-solver/

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI