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?
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.