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 boolean variables $y_1,\dots,y_n$, with the idea that $y_i$ should contain the value of $x_1 \lor x_2 \lor \cdots \lor x_i$.  This intent can be enforced by adding the clauses $y_i \lor \neg x_i$, $y_i \lor \neg y_{i-1}$, and $\neg y_i \lor x_i \lor y_{i-1}$ (where we treat $y_0$ as a synonym for false) for $i=1,\dots,n$.  Next, we can add the restrictions $\neg y_i \lor \neg x_{i+1}$ for $i=1,2,\dots,n-1$.  This is basically equivalent to the Tseitin transform of a half-adder tree, where the tree has a maximally unbalanced shape.Butterfly network. I could build a butterfly network on $n$ bits, constrain the $n$-bit input to be $000\cdots 01$, constrain the $n$-bit output to be $x_1 x_2 \cdots x_n$, and treat each 2-bit butterfly gate as an independent gate that either swaps or does not swap its input with the decision of which to do based upon a fresh new boolean variable that is left unconstrained.  Then, I can apply the Tseitin transform to convert the circuit to SAT clauses.This requires $\Theta(n \lg n)$ gates and thus adds $\Theta(n \lg n)$ clauses and $\Theta(n \lg n)$ new boolean variables.Are there any other methods I have overlooked?  Which one should I use?  Has anyone tested this or tried them experimentally, or does anyone have any experience with any of these?  Is the number of clauses and/or the number of new boolean variables a good stand-in metric for estimating the impact of this on SAT solver performance, or if not, what metric would you use?I just noticed that this answer has some references on enforcing cardinality constraints for SAT, i.e., enforcing the constraint that exactly $k$ out of the $n$ variables are true.  So, my question comes down to a special case where $k=1$.  Maybe the literature on cardinality constraints will help shed light on my question.
Encoding 1-out-of-n constraint for SAT solvers
satisfiability;sat solvers;applied theory