Encoding 1-out-of-n constraint for SAT solvers

I'm using a SAT solver to encode a problem, and as part of the SAT instance, I have boolean variables $x_1,x_2,\dots,x_n$ where it is intended that exactly one of these should be true and the rest should be false. (I've sometimes seen this described as a "one-hot" encoding.)

I want to encode the constraint "exactly one out of $x_1,\dots,x_n$ must be true" in SAT. What is the best way to encode this constraint, to make the SAT solver run as efficiently as possible?

I can see many ways to encode this constraint:

-
Pairwise constraints. I could add pairwise constraints $\neg x_i \lor \neg x_j$ for all $i,j$ to ensure that at most one $x_i$ is true, and then add $x_1 \lor x_2 \lor \cdots \lor x_n$ to ensure that at least one is true.

This adds $\Theta(n^2)$ clauses and no extra boolean variables.

-
Binary encoding. I could introduce $\lg n$ new boolean variables $i_1,i_2,\dots,i_{\lg n}$ to represent (in binary) an integer $i$ such that $1 \le i \le n$ (adding a few boolean constraints to ensure that $i$ is in the desired range). Then, I can add constraints enforcing that $x_i$ is tree and that all other $x_j$'s are false. In other words, for each $j$, we add clauses enforcing that $i=j \Leftrightarrow x_j$.

This adds $\Theta(n \lg n)$ clauses and I don't know how many extra boolean variables.

-
Count the number of true values. I could implement a tree of boolean adder circuits and require that $x_1+x_2+\dots+x_n=1$, treating each $x_i$ as 0 or 1 instead of false or true, and use the Tseitin transform to convert the circuit to SAT clauses. A tree of half-adders suffices: constrain the carry output of each half-adder to be 0, and constrain the final output of the final half-adder in the tree to be 1. The tree can be chosen to be of any shape (balanced binary tree, or unbalanced, or whatever).

This can be done in $\Theta(n)$ gates and thus adds $\Theta(n)$ clauses and $\Theta(n)$ new boolean variables.

A special case of this approach is to introduce

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.

StackExchange Computer Science Q#13188, answer score: 15