SAT 2004 START ConferenceManager    


Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization

Vasco M. Manquinho, Joćo Marques-Silva

Presented at The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004), Vancouver, BC, Canada, 10-13 May 2004


Abstract

Linear Pseudo-Boolean constraints offer a much more compact formalism to express significant boolean problems in several areas, ranging from Artificial Intelligence to Electronic Design Automation. This paper proposes a new algorithm for the Pseudo-Boolean Optimization Problem (PBO) which integrates features from recent advances in Boolean Satisfiability (SAT) and classical branch and bound algorithms. Moreover, the paper shows that the utilization of lower bound estimates can improve the overall performance of PBO solvers for different classes of instances. In addition, the paper describes how to apply non-chronological backtracking in the presence of conflicts that result from the bounding process. Finally, the paper also shows how the notion of Unique Implication Points (UIP), widely used in modern SAT solvers, can be generalized for PBO.


  
START Conference Manager (V2.47.2)
Maintainer: rrgerber@softconf.com