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.
asked Aug 26, 2021 at 16:42 799 5 5 silver badges 11 11 bronze badgesLets 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$