Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms
Demirović, Emir ; McCreesh, Ciaran ; McIlree, Matthew J. ; Nordström, Jakob LU ; Oertel, Andy LU
and Sidorov, Konstantin
(2024)
30th International Conference on Principles and Practice of Constraint Programming, CP 2024
307.
- Abstract
- Pseudo-Boolean proof logging has been used successfully to provide certificates of optimality from a variety of constraint- and satisifability-style solvers that combine reasoning with a backtracking or clause-learning search. Another paradigm, occurring in dynamic programming and decision diagram solving, instead reasons about partial states and possible transitions between them. We describe a framework for generating clean and efficient pseudo-Boolean proofs for these kinds of algorithm, and use it to produce certifying algorithms for knapsack, longest path, and interval scheduling. Because we use a common proof system, we can also reason about hybrid solving algorithms: we demonstrate this by providing proof logging for a dynamic... (More)
- Pseudo-Boolean proof logging has been used successfully to provide certificates of optimality from a variety of constraint- and satisifability-style solvers that combine reasoning with a backtracking or clause-learning search. Another paradigm, occurring in dynamic programming and decision diagram solving, instead reasons about partial states and possible transitions between them. We describe a framework for generating clean and efficient pseudo-Boolean proofs for these kinds of algorithm, and use it to produce certifying algorithms for knapsack, longest path, and interval scheduling. Because we use a common proof system, we can also reason about hybrid solving algorithms: we demonstrate this by providing proof logging for a dynamic programming based knapsack propagator inside a constraint programming solver. (Less)
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/c210f574-346e-4fed-882f-53941fff1097
- author
- Demirović, Emir
; McCreesh, Ciaran
; McIlree, Matthew J.
; Nordström, Jakob
LU
; Oertel, Andy
LU
and Sidorov, Konstantin
- organization
- publishing date
- 2024-08-29
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Leibniz International Proceedings in Informatics, LIPIcs
- editor
- Shaw, Paul
- volume
- 307
- article number
- 9
- pages
- 21 pages
- publisher
- Schloss Dagstuhl - Leibniz-Zentrum für Informatik
- conference name
- 30th International Conference on Principles and Practice of Constraint Programming, CP 2024
- conference location
- Girona, Spain
- conference dates
- 2024-09-02 - 2024-09-06
- external identifiers
-
- scopus:85203678920
- ISBN
- 978-3-95977-336-2
- DOI
- 10.4230/LIPIcs.CP.2024.9
- language
- English
- LU publication?
- yes
- id
- c210f574-346e-4fed-882f-53941fff1097
- date added to LUP
- 2024-09-09 10:52:35
- date last changed
- 2025-10-14 11:56:45
@inproceedings{c210f574-346e-4fed-882f-53941fff1097,
abstract = {{Pseudo-Boolean proof logging has been used successfully to provide certificates of optimality from a variety of constraint- and satisifability-style solvers that combine reasoning with a backtracking or clause-learning search. Another paradigm, occurring in dynamic programming and decision diagram solving, instead reasons about partial states and possible transitions between them. We describe a framework for generating clean and efficient pseudo-Boolean proofs for these kinds of algorithm, and use it to produce certifying algorithms for knapsack, longest path, and interval scheduling. Because we use a common proof system, we can also reason about hybrid solving algorithms: we demonstrate this by providing proof logging for a dynamic programming based knapsack propagator inside a constraint programming solver.}},
author = {{Demirović, Emir and McCreesh, Ciaran and McIlree, Matthew J. and Nordström, Jakob and Oertel, Andy and Sidorov, Konstantin}},
booktitle = {{Leibniz International Proceedings in Informatics, LIPIcs}},
editor = {{Shaw, Paul}},
isbn = {{978-3-95977-336-2}},
language = {{eng}},
month = {{08}},
publisher = {{Schloss Dagstuhl - Leibniz-Zentrum für Informatik}},
title = {{Pseudo-Boolean Reasoning About States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms}},
url = {{http://dx.doi.org/10.4230/LIPIcs.CP.2024.9}},
doi = {{10.4230/LIPIcs.CP.2024.9}},
volume = {{307}},
year = {{2024}},
}