Pseudo-Boolean Reasoning about States and Transitions to Certify Dynamic Programming and Decision Diagram Algorithms
Emir Demirović (TU Delft - Electrical Engineering, Mathematics and Computer Science)
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 - Electrical Engineering, Mathematics and Computer Science)
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