Sciweavers

Share
JAR
2011

A Framework for Certified Boolean Branch-and-Bound Optimization

8 years 5 months ago
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
Javier Larrosa, Robert Nieuwenhuis, Albert Olivera
Added 16 May 2011
Updated 16 May 2011
Type Journal
Year 2011
Where JAR
Authors Javier Larrosa, Robert Nieuwenhuis, Albert Oliveras, Enric Rodríguez-Carbonell
Comments (0)
books