How can I rewrite this xor formula to generate cnf formulas

1.7k Views Asked by At

$$ \bigwedge_{c=1}^n\bigwedge_{i\epsilon S}\bigoplus_{r=1}^nX_{irc} $$ I have tried $$ \bigwedge_{c=1}^n\bigwedge_{i\epsilon S}\bigwedge_{r_1=1,r_2=1}^n(X_{ir_1c}\vee X_{ir_2c})\wedge(\neg X_{ir_1c}\vee \neg X_{ir_2c}) $$ But this does not work because A$\oplus$A is always false

Can you recomend some resources / tutorials on such notations ?

1

There are 1 best solutions below

1
On

Since the indices differ for each $X$, you never have the same term XOR-d with itself. To transform that formula to a CNF form, you just need to unpack those generalized operations. To avoid possible ambiguities I'm going to change the outer $n$ to $m$, since they might not be equal. Then:

$$\bigwedge_{c=1}^m\bigwedge_{i \in S}\bigoplus_{r=1}^n X_{irc}$$

$$\equiv \bigwedge_{c=1}^m\bigwedge_{i \in S} X_{i1c}\oplus \cdots \oplus X_{inc}$$

$$\equiv\bigwedge_{c=1}^m(X_{S_11c}\oplus \cdots \oplus X_{S_1nc})\land \cdots \land(X_{S_n1c}\oplus \cdots \oplus X_{S_nnc})$$

$$\equiv[(X_{S_111}\oplus \cdots \oplus X_{S_1n1})\land \cdots \land(X_{S_n11}\oplus \cdots \oplus X_{S_nn1})] \land \cdots \\\cdots \land [(X_{S_11m}\oplus \cdots \oplus X_{S_1nm})\land \cdots \land(X_{S_n1m}\oplus \cdots \oplus X_{S_nnm})]$$

Once you replace all $(\phi \oplus \psi)$ expressions with $[(\phi \lor \psi) \land \lnot(\phi \land \psi)]$s, you'll obtain a much longer formula consisting of conjunctions, disjunctions, and negations. By the familiar method you can then convert that to an equivalent formula in CNF.