A fast pseudo-Boolean constraint solver

摘要

Linear pseudo-Boolean (LPB) constraints denote inequalities between arithmetic sums of weighted Boolean functions and provide a significant extension of the modeling power of purely propositional constraints. They can be used to compactly describe many discrete electronic design automation problems with constraints on linearly combined, weighted Boolean variables, yet also offer efficient search strategies for proving or disproving whether a satisfying solution exists. Furthermore, corresponding decision procedures can easily be extended for minimizing or maximizing an LPB objective function, thus providing a core optimization method for many problems in logic and physical synthesis. In this paper, we review how recent advances in satisfiability search can be extended for pseudo-Boolean constraints and describe a new LPB solver that is based on generalized constraint propagation and conflict-based learning. We present a comparison with other, state-of-the-art LPB solvers which demonstrates the overall efficiency of our method.