2 Search Results for "Helmert, Malte"

Document
DOI: 10.4230/LIPIcs.CP.2025.21
Practically Feasible Proof Logging for Pseudo-Boolean Optimization

Authors: Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract
Certifying solvers have long been standard for decision problems in Boolean satisfiability (SAT), allowing for proof logging and checking with very limited overhead, but developing similar tools for combinatorial optimization has remained a challenge. A recent promising approach covering a wide range of solving paradigms is pseudo-Boolean proof logging, but this has mostly consisted of proof-of-concept works far from delivering the performance required for real-world deployment. In this work, we present an efficient toolchain based on VeriPB and CakePB for formally verified pseudo-Boolean optimization. We implement proof logging for the full range of techniques in the state-of-the-art solvers RoundingSat and Sat4j, including core-guided search and linear programming integration with Farkas certificates and cut generation. Our experimental evaluation shows that proof logging and checking performance in this much more expressive paradigm is now quite close to the level of SAT solving, and hence is clearly practically feasible.
Cite as

Wietze Koops, Daniel Le Berre, Magnus O. Myreen, Jakob Nordström, Andy Oertel, Yong Kiam Tan, and Marc Vinyals. Practically Feasible Proof Logging for Pseudo-Boolean Optimization. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 21:1-21:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{koops_et_al:LIPIcs.CP.2025.21,
  author =	{Koops, Wietze and Le Berre, Daniel and Myreen, Magnus O. and Nordstr\"{o}m, Jakob and Oertel, Andy and Tan, Yong Kiam and Vinyals, Marc},
  title =	{{Practically Feasible Proof Logging for Pseudo-Boolean Optimization}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{21:1--21:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.21},
  URN =		{urn:nbn:de:0030-drops-238825},
  doi =		{10.4230/LIPIcs.CP.2025.21},
  annote =	{Keywords: proof logging, certifying algorithms, combinatorial optimization, certification, pseudo-Boolean solving, 0-1 integer linear programming}
}
Document
DOI: 10.4230/DagSemProc.09491.3
Landmarks, Critical Paths and Abstractions: What's the Difference Anyway?

Authors: Malte Helmert and Carmel Domshlak

Published in: Dagstuhl Seminar Proceedings, Volume 9491, Graph Search Engineering (2010)

Abstract
Current heuristic estimators for classical domain-independent planning are usually based on one of four ideas: delete relaxation, abstraction, critical paths, and, most recently, landmarks. Previously, these different ideas for deriving heuristic functions were largely unconnected. In my talk, I will show that these heuristics are in fact very closely related. Moreover, I will introduce a new admissible heuristic called the landmark cut heuristic which exploits this relationship. In our experiments, the landmark cut heuristic provides better estimates than other current admissible planning heuristics, especially on large problem instances.
Cite as

Malte Helmert and Carmel Domshlak. Landmarks, Critical Paths and Abstractions: What's the Difference Anyway?. In Graph Search Engineering. Dagstuhl Seminar Proceedings, Volume 9491, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{helmert_et_al:DagSemProc.09491.3,
  author =	{Helmert, Malte and Domshlak, Carmel},
  title =	{{Landmarks, Critical Paths and Abstractions: What's the Difference Anyway?}},
  booktitle =	{Graph Search Engineering},
  pages =	{1--2},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{9491},
  editor =	{Lubos Brim and Stefan Edelkamp and Erik A. Hansen and Peter Sanders},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09491.3},
  URN =		{urn:nbn:de:0030-drops-24324},
  doi =		{10.4230/DagSemProc.09491.3},
  annote =	{Keywords: Planning, heuristic search, heuristic functions}
}
  • Refine by Type
  • 2 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 1 2010

  • Refine by Author
  • 1 Domshlak, Carmel
  • 1 Helmert, Malte
  • 1 Koops, Wietze
  • 1 Le Berre, Daniel
  • 1 Myreen, Magnus O.
  • Show More...

  • Refine by Series/Journal
  • 1 LIPIcs
  • 1 DagSemProc

  • Refine by Classification
  • 1 Mathematics of computing → Combinatorial optimization
  • 1 Theory of computation → Logic and verification

  • Refine by Keyword
  • 1 0-1 integer linear programming
  • 1 Planning
  • 1 certification
  • 1 certifying algorithms
  • 1 combinatorial optimization
  • Show More...

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