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.

• I assume you want a solution that's efficient in CNF?
– orlp
Commented Jan 25 at 11:57
• yes, as few variable/clauses as possible Commented Jan 25 at 12:59
• This is a duplicate of cs.stackexchange.com/questions/143462/… Commented Jan 26 at 10:45

1 Answer

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.

• great, exactly what i was looking for. Commented Jan 25 at 13:00