Pseudo-Boolean Reasoning about States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms
E. Demirovic (TU Delft - Algorithmics)
Ciaran McCreesh (University of Glasgow)
Matthew J. McIlree (University of Glasgow)
Jakob Nordström (Lund University, University of Copenhagen)
Andy Oertel (University of Copenhagen, Lund University)
Konstantin Sidorov (TU Delft - Algorithmics)
More Info
expand_more
Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.
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.
help_outline