2 Search Results for "Smirnov, Pavel"

Document
DOI: 10.4230/LIPIcs.SAT.2022.13
Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization

Authors: Pavel Smirnov, Jeremias Berg, and Matti Järvisalo

Published in: LIPIcs, Volume 236, 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022)

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.
Cite as

Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Improvements to the Implicit Hitting Set Approach to Pseudo-Boolean Optimization. In 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 236, pp. 13:1-13:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)

Copy BibTex To Clipboard

@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-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2022.13},
  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}
}
Document
DOI: 10.4230/LIPIcs.CP.2021.51
Pseudo-Boolean Optimization by Implicit Hitting Sets

Authors: Pavel Smirnov, Jeremias Berg, and Matti Järvisalo

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)

Abstract
Recent developments in applying and extending Boolean satisfiability (SAT) based techniques have resulted in new types of approaches to pseudo-Boolean optimization (PBO), complementary to the more classical integer programming techniques. In this paper, we develop the first approach to pseudo-Boolean optimization based on instantiating the so-called implicit hitting set (IHS) approach, motivated by the success of IHS implementations for maximum satisfiability (MaxSAT). In particular, we harness recent advances in native reasoning techniques for pseudo-Boolean constraints, which enable efficiently identifying inconsistent assignments over subsets of objective function variables (i.e. unsatisfiable cores in the context of PBO), as a basis for developing a native IHS approach to PBO, and study the impact of various search techniques applicable in the context of IHS for PBO. Through an extensive empirical evaluation, we show that the IHS approach to PBO can outperform other currently available PBO solvers, and also provides a complementary approach to PBO when compared to classical integer programming techniques.
Cite as

Pavel Smirnov, Jeremias Berg, and Matti Järvisalo. Pseudo-Boolean Optimization by Implicit Hitting Sets. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 51:1-51:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{smirnov_et_al:LIPIcs.CP.2021.51,
  author =	{Smirnov, Pavel and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{Pseudo-Boolean Optimization by Implicit Hitting Sets}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{51:1--51:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.51},
  URN =		{urn:nbn:de:0030-drops-153429},
  doi =		{10.4230/LIPIcs.CP.2021.51},
  annote =	{Keywords: constraint optimization, pseudo-Boolean optimization, implicit hitting sets}
}
  • Refine by Author
  • 2 Berg, Jeremias
  • 2 Järvisalo, Matti
  • 2 Smirnov, Pavel

  • Refine by Classification
  • 2 Mathematics of computing → Combinatorial optimization
  • 2 Theory of computation → Constraint and logic programming

  • Refine by Keyword
  • 2 constraint optimization
  • 2 implicit hitting sets
  • 2 pseudo-Boolean optimization
  • 1 solution-improving search
  • 1 unsatisfiable cores

  • Refine by Type
  • 2 document

  • Refine by Publication Year
  • 1 2021
  • 1 2022

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact