Search Results

Documents authored by Vandesande, Dieter

Document
Tool Paper
DOI: 10.4230/LIPIcs.SAT.2026.34
HitPBO: An Implicit Hitting Set Solver for Pseudo-Boolean Optimization (Tool Paper)

Authors: Hannes Ihalainen, Dieter Vandesande, André Schidler, Jeremias Berg, and Matti Järvisalo

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)

Abstract
We describe HitPBO 1.0, a from-scratch open-source C++ implementation of the implicit hitting set (IHS) approach to pseudo-Boolean optimization. Compared to earlier implementations, HitPBO adds a range of functionalities and search techniques, certificates, and support for various alternative solvers within IHS. We give an overview of the solver’s architecture and its functionalities.
Cite as

Hannes Ihalainen, Dieter Vandesande, André Schidler, Jeremias Berg, and Matti Järvisalo. HitPBO: An Implicit Hitting Set Solver for Pseudo-Boolean Optimization (Tool Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 34:1-34:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{ihalainen_et_al:LIPIcs.SAT.2026.34,
  author =	{Ihalainen, Hannes and Vandesande, Dieter and Schidler, Andr\'{e} and Berg, Jeremias and J\"{a}rvisalo, Matti},
  title =	{{HitPBO: An Implicit Hitting Set Solver for Pseudo-Boolean Optimization}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{34:1--34:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.34},
  URN =		{urn:nbn:de:0030-drops-263401},
  doi =		{10.4230/LIPIcs.SAT.2026.34},
  annote =	{Keywords: Pseudo-Boolean optimization, implicit hitting set approach, solvers}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.4
Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability

Authors: Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Proof logging has long been the established method to certify correctness of Boolean satisfiability (SAT) solvers, but has only recently been introduced for SAT-based optimization (MaxSAT). The focus of this paper is solution-improving search (SIS), in which a SAT solver is iteratively queried for increasingly better solutions until an optimal one is found. A challenging aspect of modern SIS solvers is that they make use of complex "without loss of generality" arguments that are quite involved to understand even at a human meta-level, let alone to express in a simple, machine-verifiable proof. In this work, we develop pseudo-Boolean proof logging methods for solution-improving MaxSAT solving, and use them to produce a certifying version of the state-of-the-art solver Pacose with VeriPB proofs. Our experimental evaluation demonstrates that this approach works in practice. We hope that this is yet another step towards general adoption of proof logging in MaxSAT solving.
Cite as

Jeremias Berg, Bart Bogaerts, Jakob Nordström, Andy Oertel, Tobias Paxian, and Dieter Vandesande. Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 4:1-4:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{berg_et_al:LIPIcs.CP.2024.4,
  author =	{Berg, Jeremias and Bogaerts, Bart and Nordstr\"{o}m, Jakob and Oertel, Andy and Paxian, Tobias and Vandesande, Dieter},
  title =	{{Certifying Without Loss of Generality Reasoning in Solution-Improving Maximum Satisfiability}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{4:1--4:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.4},
  URN =		{urn:nbn:de:0030-drops-206895},
  doi =		{10.4230/LIPIcs.CP.2024.4},
  annote =	{Keywords: proof logging, certifying algorithms, MaxSAT, solution-improving search, SAT-UNSAT, maximum satisfiability, combinatorial optimization, certification, pseudo-Boolean}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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