\myheading{Proving bizarre XOR alternative using SAT solver}
\label{weird_XOR_SAT}

\renewcommand{\CURPATH}{proofs/XOR_SAT}

Now let's try to prove it using SAT.

We would build an electric circuit for $x \oplus y = -2*(x \& y) + (x + y)$ like that:

\iffalse
\begin{lstlisting}[basicstyle=\small]
x -+--- +---+
   |    |AND| --- +---+     
y -|-+- +---+     |MUL| --- +---+
   | |         -2 +---+     |ADD| --- +---+
   | |                  x - +---+     |ADD| --> out1 --- +------+
   | |                            y - +---+              |      |      
   | |                                                   |  EQ  | ---> must be true
   +-|- +---+                                            |      |      
     |  |XOR| --------------------------------> out2 --- +------+
     +- +---+
\end{lstlisting}
\fi

\begin{figure}[H]
\includesvg[width=\textwidth]{\CURPATH/1.svg}
\end{figure}

And now we can implement EQ block using XOR and OR:

\iffalse
\begin{lstlisting}[basicstyle=\small]
x -+--- +---+
   |    |AND| --- +---+     
y -|-+- +---+     |MUL| --- +---+
   | |         -2 +---+     |ADD| --- +---+
   | |                  x - +---+     |ADD| --> out1 --- +-------+
   | |                            y - +---+              |       |      +----+
   | |                                                   |  XOR  | ---> | OR | ---> must be 0
   +-|- +---+                                            |       |      +----+
     |  |XOR| --------------------------------> out2 --- +-------+
     +- +---+
\end{lstlisting}
\fi

\begin{figure}[H]
\includesvg[width=\textwidth]{\CURPATH/2.svg}
\end{figure}

So it has two parts: generic XOR block and a block which must be equivalent to XOR.
Then we compare its outputs using XOR and OR.
If outputs of these parts are always equal to each other for all possible x and y, output of the whole block must be 0.

I do otherwise, I'm trying to find such an input pair, for which output will be 1:

\begin{lstlisting}[style=custompy]
def chk1():
    input_bits=8

    s=SAT_lib.SAT_lib(False)

    x,y=s.alloc_BV(input_bits),s.alloc_BV(input_bits)
    step1=s.BV_AND(x,y)
    minus_2=[s.const_true]*(input_bits-1)+[s.const_false]
    product=s.multiplier(step1,minus_2)[input_bits:]
    result1=s.adder(s.adder(product, x)[0], y)[0]

    result2=s.BV_XOR(x,y)

    s.fix(s.OR(s.BV_XOR(result1, result2)), True)

    if s.solve()==False:
        print ("unsat")
        return

    print ("sat")
    print ("x=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(x)))
    print ("y=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(y)))
    print ("step1=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(step1)))
    print ("product=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(product)))
    print ("result1=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(result1)))
    print ("result2=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(result2)))
    print ("minus_2=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(minus_2)))
\end{lstlisting}

The full source code: \url{\RepoURL/\CURPATH/XOR_SAT.py}.

SAT solver returns "unsat", meaning, it couldn't find such a pair.
In other words, it couldn't find a counterexample.
So the circuit always outputs 0, for all possible inputs, meaning, outputs of two parts are always the same.

Modify the circuit, and the program will find such a state, and print it.

That circuit also called "miter".
According to Google translate, one meaning of the word is:

\begin{lstlisting}
a joint made between two pieces of wood or other material at an angle of 90°, such that the line of junction bisects this angle.
\end{lstlisting}

It's also slow, because multiplier block is used: so we use small 8-bit x's and y's.

But the whole thing can be rewritten: $x \oplus y = x+y - (x \& y)<<1$.
And subtraction is addition, but with one negated operand.
So, $x \oplus y = (-(x \& y))<<1 + (x + y)$ or
$x \oplus y = (x \& y)*2 - (x + y)$.

\iffalse
\begin{lstlisting}[basicstyle=\footnotesize]
x --- +---+     +---+     +---+
      |AND| --- |NEG| --- |<<1| -+ 
y --- +---+     +---+     +---+  +- +---+
                                    |ADD| --- +---+
                                x - +---+     |ADD| --> out1 --- +-------+
                                          y - +---+              |       |      +----+
                                                                 |  XOR  | ---> | OR | ---> must be 0
x --- +---+                                                      |       |      +----+
      |XOR| ------------------------------------------> out2 --- +-------+
y --- +---+
\end{lstlisting}
\fi

\begin{figure}[H]
\includesvg[width=\textwidth]{\CURPATH/3.svg}
\end{figure}

\TT{NEG} is negation block, in two's complement system.
It just inverts all bits and adds 1:

\begin{lstlisting}[style=custompy]
    def NEG(self, x):
        # invert all bits
        tmp=self.BV_NOT(x)
        # add 1
        one=self.alloc_BV(len(tmp))
        self.fix_BV(one,n_to_BV(1, len(tmp)))
        return self.adder(tmp, one)[0]
\end{lstlisting}

Shift by one bit does nothing except rewiring.

That works way faster, and can prove correctness for 64-bit x's and y's, or for even bigger input values:

\begin{lstlisting}[style=custompy]
def chk2():
    input_bits=64

    s=SAT_lib.SAT_lib(False)

    x,y=s.alloc_BV(input_bits),s.alloc_BV(input_bits)
    step1=s.BV_AND(x,y)
    step2=s.shift_left_1(s.NEG(step1))

    result1=s.adder(s.adder(step2, x)[0], y)[0]

    result2=s.BV_XOR(x,y)

    s.fix(s.OR(s.BV_XOR(result1, result2)), True)

    if s.solve()==False:
        print ("unsat")
        return

    print ("sat")
    print ("x=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(x)))
    print ("y=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(y)))
    print ("step1=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(step1)))
    print ("step2=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(step2)))
    print ("result1=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(result1)))
    print ("result2=%x" % SAT_lib.BV_to_number(s.get_BV_from_solution(result2)))
\end{lstlisting}

The source code: \url{\RepoURL/\CURPATH/XOR_SAT.py}.