A Framework for Certified Boolean Branch-and-Bound Optimization

We consider optimization problems of the form (S, cost), where S is a clause set over Boolean variables x1 . . . xn, with an arbitrary cost function cost: Bn → R, and the aim is to find a model A of S such that cost(A) is minimized. Here we study the generation of proofs of optimality in the context of branch-and-bound es for such problems. For this purpose we introduce DPLLBB, 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, SATrelated optimization problems are in the scope of DPLLBB. Since many of the existing approaches for solving these problems can be seen as instances, DPLLBB allows one to formally reason about them in a simple way and exploit the enhancements of DPLLBB given here, in particular its uniform method for generating independently verifiable optimality proofs. Keywords SAT · Optimization · Proofs

• Type: Journal
• Year: 2011
• Where: JAR
• Authors: Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
• Keywords: Arbitrary Cost Function, JAR 2011, Optimization Problems, Problems