On the CNF encoding of cardinality constraints and beyond
Olivier Bailleux · arXiv (Cornell University) · 2010
In this report, we propose a quick survey of the currently known techniques for encoding a Boolean cardinality constraint into a CNF formula, and we discuss about the relevance of these encodings. We also propose models to facilitate analysis and design of CNF encodings for Boolean constraints.