Encoding 1-out-of-n constraint for SAT solvers
For the special case of k out of n variables true where k = 1, there is commander variable encoding as described in Efficient CNF Encoding for Selecting 1 to N Objects by Klieber and Kwon.  Simplified: Divide the variables into small groups and add clauses that cause a commander variable's state to imply that a group of variables is either all false or all-but-one false.  Then recursively apply the same algorithm to the commander variables.  At the end of the process demand that the exactly one of the handful of final commander variables be true.  The result is O(n) new clauses and O(n) new variables.

Given the ubiquity of two-watched-literals in DPLL based solvers, I think the O(n) clause growth is a decisive advantage over encoding schemes that would add more clauses.