SAT formulation of the condition that an even number of a given set of variables must be set to true

Lets say I have a SAT problem with variables $x_1,...,x_n$. For a given subset of the variables I want to create a clause which forces an even number of the variables in $S$ to be true. Of course there is the brute force solution, but I would like a more efficient solution with as few clauses/variables as possible.

Let $\oplus$ be XOR, then your question is asking for $\bigoplus_{k=1}^n x_k = 0$. We can encode this efficiently without an exponential explosion in clauses by introducing new variables.

The basic premise is the following:

$$a = b \oplus c \quad\iff\quad a \oplus b \oplus c = 0$$

Assuming $a$ is the new variable this is equivalent to adding the following CNF clauses:

$$(\neg a \vee \neg b \vee \neg c) \,\wedge\, (\neg a \vee b \vee c) \,\wedge\, (a \vee \neg b \vee c) \,\wedge\, (a \vee b \vee \neg c)$$

Using the above construction we add the following clauses:

$$y_1 = x_1$$
$$y_2 = y_1 \oplus x_2$$
$$y_3 = y_2 \oplus x_3$$
$$\cdots$$

Finally we add the clause $\neg y_n$.

Total cost is $n$ additional variables and $4n + 1$ ternary CNF clauses. You can shave off a couple variables / clauses with a better base case for the recursion - I could not be bothered.

StackExchange Computer Science Q#165228, answer score: 6