A Lower Bound on DNNF Encodings of Pseudo-Boolean Constraints
  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.
