Two major considerations when encoding pseudo-Boolean (PB) constraints into SAT are the size of the encoding and its propagation strength, that is, the guarantee that it has a good behaviour under unit propagation. Several encodings with propagation strength guarantees rely upon prior compilation of the constraints into DNNF (decomposable negation normal form), BDD (binary decision diagram), or some other sub-variants. However it has been shown that there exist PB-constraints whose ordered BDD (OBDD) representations, and thus the inferred CNF encodings, all have exponential size. Since DNNFs are more succinct than OBDDs, preferring encodings via DNNF to avoid size explosion seems a legitimate choice. Yet in this paper, we prove the existence of PB-constraints whose DNNFs all require exponential size.

翻译：在将伪Boolean(PB)限制编码成SAT时,两个主要考虑因素是编码的大小及其传播强度,即保证其在单位传播中行为良好。几个带有传播力度保障的编码依赖于事先将限制编入DNNF(非可反常格式)、BDD(二进制决定图)或其他一些次变量。然而,已经表明存在PB-约束,其订购的BDD(OBDD)表示方式,从而推导的CNF编码都具有指数大小。由于DNF比OBDDs更简洁,通过DNNF将编码改为DNF以避免规模爆炸似乎是合理的选择。然而,在本文中,我们证明存在PB-约束,其DNFs都需要指数大小。