# Simplest transformation from XOR to CNF SAT

What is the simplest way to transfrom $$a\newcommand*\xor{\oplus}b=c$$ to a CNF SAT expression with minimum number of clauses. The default transformation requires upto 9 clauses. I think we can do much better.

Lets start with transforming $$a\oplus b = True$$. This is simple enough, since it happens if and only if either one of $$a$$ or $$b$$ is $$True$$ and the other is $$False$$. We can easily encode it as follows:

$$(a\lor b)\land (\lnot a \lor \lnot b)$$

Now, to transform $$a\oplus b = c$$ we need two cases: one for when $$c=True$$ and the other for when $$c=False$$. We covered already the case for $$c=True$$, so now lets go through $$c=False$$. In this case, both $$a$$ and $$b$$ must be the same value. Notice that $$\lnot a \lor b$$ is equivalent to $$a\rightarrow b$$, and hence $$(\lnot a \lor b) \land (\lnot b \lor a)$$ is equivalent to $$(a\rightarrow b)\land (b \rightarrow a)$$ which is also equivalent to $$a\longleftrightarrow b$$. Hence, when $$c=False$$ we need the encoding to be:

$$(\lnot a \lor b) \land (a \lor \lnot b)$$

Combining the two is rather easy:

$$(a\lor b\lor \lnot c)\land (\lnot a\lor \lnot b\lor \lnot c) \land (\lnot a \lor b\lor c) \land (a \lor\lnot b\lor c)$$

I will leave it to you to prove that this is indeed equivalent to $$a\oplus b = c$$

:)

I'd like to offer a more straightforward method for transforming XOR equations into SAT.

step 1:

Regardless of the number of variables on the right side of the equality, we can shift them to the left by iteratively XOR-ing the same variables one by one. For example:

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

step 2:

Now, this equation implies that the count of 1s in $$a , b , c$$ must be even. We can express all the clauses for cases where the count of 1s is odd, corresponding to an odd number of negations:

$$(a \lor b \lor \neg c) \land (\neg a \lor \neg b \lor \neg c) \land (\neg a \lor b \lor c) \land (a \lor \neg b \lor c)$$

For any XOR equation with a length of k, we require exactly $$2^{k-1}$$ clauses to encode it.

• A XOR equation $x_1\oplus\dots\oplus x_{k+1}=0$, $k\ge3$, is equisatisfiable with $x_1\oplus\dots\oplus x_{k-1}\oplus y=0\land y\oplus x_k\oplus x_{k+1}=0$. Repeating this, and transforming the $3$-XOR equations into $3$-clauses, gives a $3$-CNF with only $4(k-2)$ clauses rather than a $k$-CNF with $2^{k-1}$ clauses. Commented Nov 27, 2023 at 10:58