Towards an optimal CNF encoding of boolean cardinality constraints

Abstract

We consider the problem of encoding Boolean cardinality constraints in conjunctive normal form (CNF). Boolean cardinality constraints are formulae expressing that at most (resp. at least) k out of n propositional variables are true. We give two novel encodings that improve upon existing results, one which requires only 7n clauses and 2n auxiliary variables, and another one demanding O(n · k) clauses, but with the advantage that inconsistencies can be detected in linear time by unit propagation alone. Moreover, we prove a linear lower bound on the number of required clauses for any such encoding. © Springer-Verlag Berlin Heidelberg 2005.