Pseudo-Boolean constraints are omnipresent in practical applications, and
thus a significant effort has been devoted to the development of good SAT
encoding techniques for them. Some of these encodings first construct a Binary
Decision Diagram (BDD) for the constraint, and then encode the BDD into a
propositional formula. These BDD-based approaches have some important
advantages, such as not being dependent on the size of the coefficients, or
being able to share the same BDD for representing many constraints.
We first focus on the size of the resulting BDDs, which was considered to be
an open problem in our research community. We report on previous work where it
was proved that there are Pseudo-Boolean constraints for which no polynomial
BDD exists. We also give an alternative and simpler proof assuming that NP is
different from Co-NP. More interestingly, here we also show how to overcome the
possible exponential blowup of BDDs by phcoefficient decomposition. This allows
us to give the first polynomial generalized arc-consistent ROBDD-based encoding
for Pseudo-Boolean constraints.
Finally, we focus on practical issues: we show how to efficiently construct
such ROBDDs, how to encode them into SAT with only 2 clauses per node, and
present experimental results that confirm that our approach is competitive with
other encodings and state-of-the-art Pseudo-Boolean solvers.

该研究论文主要研究了基于二元决策图的 Pseudo-Boolean 约束编码技术，提出了使用系数分解方法克服爆炸性增长问题，并给出了第一个多项式广义弧一致的 ROBDD 编码算法。