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 x 1  ...  x n , with an arbitrary cost function , 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...

Full description

Saved in:
Bibliographic Details
Published in:Journal of automated reasoning 2011, Vol.46 (1), p.81-102
Main Authors: Larrosa, Javier, Nieuwenhuis, Robert, Oliveras, Albert, Rodríguez-Carbonell, Enric
Format: Article
Language:English
Subjects:
Algorithms
Artificial Intelligence
Automated reasoning
Boolean algebra
Computer Science
Cost engineering
Cost function
Mathematical Logic and Formal Languages
Mathematical Logic and Foundations
Mathematical models
Optimization
Proving
Symbolic and Algebraic Manipulation
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We consider optimization problems of the form ( S , cost ), where S is a clause set over Boolean variables x 1  ...  x n , with an arbitrary cost function , 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 procedures for such problems. For this purpose we introduce , 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 . Since many of the existing approaches for solving these problems can be seen as instances, allows one to formally reason about them in a simple way and exploit the enhancements of given here, in particular its uniform method for generating independently verifiable optimality proofs.
ISSN:0168-7433
1573-0670
DOI:10.1007/s10817-010-9176-z