Sciweavers

SAT
2004
Springer

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

13 years 9 months ago
Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization
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 nonchronological 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.
Vasco M. Manquinho, João P. Marques Silva
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where SAT
Authors Vasco M. Manquinho, João P. Marques Silva
Comments (0)