Convert $\sum x_i = y$ to 3-sat
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.