A parametric approach for smaller and better encodings of cardinality constraints

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-off between minimizing either the number of variables or the number of clauses is highly application-dependent. Here we build upon previous work on Cardinality Networks to get the best of several worlds: we develop an arc-consistent encoding that, by recursively decomposing the constraint into smaller ones, allows one to decide which encoding to apply to each sub-constraint. This process minimizes a function λ·num- vars + num-clauses, where λ is a parameter that can be tuned by the user. Our careful experimental evaluation shows that (e.g., for λ = 5) this new technique produces much smaller encodings in variables and clauses, and indeed strongly improves SAT solvers' performance