Integration of lower bound estimates in pseudo-Boolean optimization

Linear pseudoBoolean optimization (PBO) has found applications in several areas, ranging from artificial intelligence to electronic design automation. Due to important advances in Boolean satisfiability (SAT), new algorithms for PBO have emerged, which are effective on highly constrained instances. However, those algorithms fail in dealing properly with the objective function of PBO. We propose an algorithm that uses lower bound estimation methods for pruning the search tree in integration with techniques from SAT algorithms. Moreover, we show that the utilization of lower bound estimates can dramatically improve the overall performance of PBO solvers for specific classes of instances. In addition, we describe how to apply nonchronological backtracking in the presence of conflicts that result from the bounding process, using different lower bound estimation methods.