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

Question

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?

Answer 1

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.

Answer 2

Hint: Use a circuit for computing $\sum_{i=1}^n x_i$. Don't forget you're allowed to add variables!