Help converting ANF to XORNF if even possible. This equivalence:
$C \leftrightarrow A · B$
can be written in ANF (algebraic normal form, where $+$ denotes $XOR$) as:
$\lnot((A · B) + C)$
One step further, interning the negation we get:
$(A · B) + \lnot C$
Can this clause be written in XORNF (conjunctions of XOR-disjunctions)? I fail to see how, conjunction distributes over $+$ but not vice-versa.
Edit: thoughts after some reading.
Fundamentally, this would work if there was a Shannon expansion dual form involving XORs, but as XOR is a non-unate function, there is none. Does this mean it is not possible at all? I don't know.
 A: $C \leftrightarrow A \cdot B$ is not expressible as conjunction of XORs (XOR-CNF).
Let's write $\#(f)$ for the number of satisfying assignments of $f$.
Suppose we have a function of variables $x_1,\ldots,x_n$.  The XOR of one or more of the literals of these variables (a XOR clause,) when seen as a function of $x_1,\ldots,x_n$ is true in exactly $2^{n-1}$ out of $2^n$ cases.    Therefore there is no way to represent a function $f(x_1,\ldots,x_n)$ with $2^{n-1}< \#(f) < 2^n$ as a conjunction of XORs.
Moreover, if $\#(f) = 2^{n-1}$, then $f$ is representable as a conjunction of XORs if and only if it is representable by one XOR clause.  If $f$ is $x_3 \leftrightarrow x_1 \cdot x_2$, then it essentially depends on all three variables.  Since $\#(f) = 2^{3-1}$, the single clause would also have to depend on all three variables.
This only leaves two choices for the clause: $(x_1 \oplus x_2 \oplus x_3)$ and $\neg(x_1 \oplus x_2 \oplus x_3)$.  Since $f$ equals neither, it is not representable in XOR-CNF form.
