Fast pseudo-Boolean constraint solver

Linear Pseudo-Boolean (LPB) constraints denote inequalities between arithmetic sums of weighted Boolean functions and pro-vide a significant extension of the modeling power of purely propo-sitional constraints. They can be used to compactly describe many discrete EDA problems with constraints on linearly combined, pa-rameterized weights, yet also offer efficient search strategies for proving or disproving whether a satisfying solution exists. Further-more, corresponding decision procedures can easily be extended for minimizing or maximizing an LPB objective function, thus pro-viding a core optimization method for many problems in logic and physical synthesis. In this paper we review how recent advances in satisfiability (SAT) search can be extended for pseudo-Boolean constraints and describe a new LPB solver that is based on gener-alized constraint propagation and conflict-based learning