Adequate encodings for high-level constraints are a key ingredient for the application of SAT technology. In particular, cardinality constraints state that at most (at least, or exactly) k out of n propositional variables can be true. They are crucial in many applications. Although sophisticated encodings for cardinality constraints exist, it is well known that for small n and k straightforward encodings without auxiliary variables sometimes behave better, and that the choice of the right trade-...
Abío, I. [et al.]. A parametric approach for smaller and better encodings of cardinality constraints. A: International Conference on Principles and Practice of Constraint Programming. "Principles and Practice of Constraint Programing - CP 2013 19th International Conference, CP 2012, Uppsala, Sweden, September 16-20, 2013, Proceedings". Uppsala: Springer, 2013, p. 80-96.