A lower bound on CNF encodings of the at-most-one constraint

Petr Kučera, Petr Savický, Vojtěch Vorel

Constraint "at most one" is a basic cardinality constraint which requires that at most one of its $n$ boolean inputs is set to $1$. This constraint is widely used when translating…