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.

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

1 Answer 1


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.

  • $\begingroup$ great, exactly what i was looking for. $\endgroup$
    – Sander
    Commented Jan 25 at 13:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.