How can I rewrite this xor formula to generate cnf formulas $$
\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 ?
 A: 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.
