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.

• Type: Conference
• Year: 2004
• Where: SAT
• Authors: Vasco M. Manquinho, João P. Marques Silva
• Keywords: Paper, Pseudo-Boolean Optimization Problem, SAT 2004, Significant Boolean Problems