New Encoding for Translating Pseudo-Boolean Constraints into SAT.
Amir Aavani, David G. M. Mitchell, Eugenia Ternovska · Symposium on Abstraction, Reformulation and Approximation · 2013
A Pseudo-Boolean (PB) constraint is a linear arithmetic constraint over Boolean variables. PB constraints are and widely used in declarative languages for expressing NP-hard search problems. While there are solvers for sets of PB constraints, there are also reasons to be interested in transforming these to propositional CNF formulas, and a number of methods for doing this have been reported. We introduce a new, two-step, method for transforming PB constraints to propositional CNF formulas. The first step re-writes each PB constraint as a conjunction of PB-Mod constraints, and the second transforms each PB-Mod constraint to CNF. The resulting CNF formulas are compact, and make effective use of unit propagation, in that unit propagation can derive facts from these CNF formulas which it cannot derive from the CNF formulas produced by other commonlyused transformation. We present a preliminary experimental evaluation of the method, using instances of the number partitioning problem as a benchmark set, which indicates that our method out-performs other transformations to CNF when the coefficients of the PB constraints are not small.