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.