History

Please fill in your query. A complete syntax description you will find on the General Help page.
A framework for certified Boolean branch-and-bound optimization. (English)
J. Autom. Reasoning 46, No. 1, 81-102 (2011).
Summary: We consider optimization problems of the form $(S, \text{cost})$, where $S$ is a clause set over Boolean variables $x_{1} \dots x_{n}$, with an arbitrary cost function $\text{cost} \colon \mathbb{B}^n \rightarrow \mathbb{R}$, and the aim is to find a model $A$ of $S$ such that $\text{cost}(A)$ is minimized. Here we study the generation of proofs of optimality in the context of branch-and-bound procedures for such problems. For this purpose we introduce {{\tt DPLL}}$_{\text{{{\tt BB}}}}$, an abstract DPLL-based branch-and-bound algorithm that can model optimization concepts such as cost-based propagation and cost-based backjumping. Most, if not all, SAT-related optimization problems are in the scope of {{\tt DPLL}}$_{\text{{{\tt BB}}}}$. Since many of the existing approaches for solving these problems can be seen as instances, {{\tt DPLL}}$_{\text{{{\tt BB}}}}$ allows one to formally reason about them in a simple way and exploit the enhancements of {{\tt DPLL}}$_{\text{{{\tt BB}}}}$ given here, in particular its uniform method for generating independently verifiable optimality proofs.
Keywords: SAT; optimization