AAAI Publications, Tenth Symposium of Abstraction, Reformulation, and Approximation

Font Size: 
New Encoding for Translating Pseudo-Boolean Constraints into SAT
Amir Aavani, David Mitchell, Eugenia Ternovska

Last modified: 2013-06-19


A Pseudo-Boolean (PB) constraint is a linear arithmetic constraint over Boolean variables. PB constraints are convenient and widely used in expressing NP-complete problems. In this paper, we introduce a new, two-step, method for transforming PB constraints to propositional CNF formulas. The first step involves re-writing each PB constraint as a conjunction of PB-Mod constraints. The advantage is that PB-Mod constraints are easier to transform to CNF. In the second step, we translate each PB-Mod constraints, obtained in the previous step, into CNF. The resulting CNF formulas are small, and unit propagation can derive facts that it cannot derive using in the CNF formulas obtained by other commonly-used transformations. The Number Partitioning Problem, NPP, asks to decide whether a given set of integers can be partitioned into two subsets S and T such that the sum of the numbers in S equals the sum of the numbers in T. Expressing an instance of NPP as a PB-constraint is straight-forward. We used NPP as the benchmark in our experiments. The results show that our proposed methods outperform the other SAT-based encodings when the coefficients are large enough.


SAT; Encoding; PB-constraint; Arc-consistency

Full Text: PDF