# Convert $\sum x_i = y$ to 3-sat

I have a simple looking question. What is the most efficient conversion of $\sum_{i=1}^n x_i = y$ to 3-sat? Here $x_i$ is either $1$ or $0$ and $y$ is some positive integer.

Can you do better than making a SATISFIABILITY instance with $\binom{n}{y}$ clauses, each of which is the conjunction of $y$ positive literals and $n-y$ negative literals and then just feeding the whole thing into the Tseitin transform?

• Have you tried anything? Efficient in what sense? – Juho Sep 27 '13 at 13:59
• @Juho A naive method would make $\binom{n}{y}$ clauses with $y$ positive literals and $n-y$ negative literals each I was thinking. This is rather large as a function of $n$. – Lembik Sep 27 '13 at 14:02
• The sizes I gave are before the conversion into 3-sat of course which will presumably expand things again. – Lembik Sep 27 '13 at 14:11
• A closely related question has been posted on CSTheory. – D.W. Oct 2 '13 at 2:15

Many better techniques for enforcing cardinality constraints are described in this answer. For the special case $y=1$, see also Encoding 1-out-of-n constraint for SAT solvers. Read those links; they suggest more efficient conversions, though I'm not aware of any reason to expect that they are necessarily optimal, so they don't answer your question about the most efficient conversion.
Hint: Use a circuit for computing $\sum_{i=1}^n x_i$. Don't forget you're allowed to add variables!