Proving bizarre XOR alternative using SAT solver

(The following text has been moved to the article at https://yurichev.com/tmp/SAT_SMT_DRAFT.pdf.)

I once wrote about quite bizarre XOR alternative I've found using aha! superoptimizer: https://github.com/dennis714/SAT_SMT_article/blob/master/SMT/XOR_EN.tex. See also here: https://yurichev.com/writings/SAT_SMT_draft-EN.pdf.

In short, x^y = -2*(x&y) + (x+y) or x^y = x+y - (x&y)<<1.

I've proved it using Z3. Now let's try to prove it using SAT.

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

x --- +---+
|AND| --- +---+
y --- +---+     |MUL| --- +---+
x - +---+     |ADD| --> output1 --- +-------+
y - +---+                 |       |      +----+
|  XOR  | ---> | OR | ---> must be 0
x --- +---+                                               |       |      +----+
|XOR| --------------------------------> output2 --- +-------+
y --- +---+


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:

def chk1():
global clauses, last_var, const_false

clauses=[]
last_var=1

# allocate a single variable fixed to False:
const_false=create_var()
var_always(const_false,False)
const_true=create_var()
var_always(const_true,True)

input_bits=8

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

result2=BV_XOR(x,y)

var_always(OR(BV_XOR(result1, result2)), True)

solution=solve(clauses)
if solution==None:
print "unsat"
return

print "sat"
print "x=%x" % BV_to_number(get_BV_from_solution(x, solution))
print "y=%x" % BV_to_number(get_BV_from_solution(y, solution))
print "step1=%x" % BV_to_number(get_BV_from_solution(step1, solution))
print "product=%x" % BV_to_number(get_BV_from_solution(product, solution))
print "result1=%x" % BV_to_number(get_BV_from_solution(result1, solution))
print "result2=%x" % BV_to_number(get_BV_from_solution(result2, solution))
print "minus_2=%x" % BV_to_number(get_BV_from_solution(minus_2, solution))


( Many functions used here has been reused from my previous example: https://yurichev.com/blog/factor_SAT/ )

The full source code: https://github.com/dennis714/yurichev.com/blob/master/blog/XOR_SAT/XOR_SAT.py.

SAT solver returns "unsat", meaning, it could 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 of meaning of this word is:

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.


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^y = x+y - (x&y)<<1. And subtraction is addition, but with one negated operand. So, x^y = (-(x&y))<<1 + (x+y) or x^y = (x&y)*2 - (x+y).

x --- +---+     +---+     +---+
|AND| --- |NEG| --- |<<1| -+
y --- +---+     +---+     +---+  +- +---+
x - +---+     |ADD| --> output1 --- +-------+
y - +---+                 |       |      +----+
|  XOR  | ---> | OR | ---> must be 0
x --- +---+                                                         |       |      +----+
|XOR| ------------------------------------------> output2 --- +-------+
y --- +---+


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

def NEG(x):
# invert all bits
tmp=BV_NOT(x)
one=alloc_BV(len(tmp))
BV_always(one,n_to_BV(1, len(tmp)))


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:

def chk2():
global clauses, last_var, const_false, const_true

clauses=[]
last_var=1

# allocate a single variable fixed to False:
const_false=create_var()
var_always(const_false,False)
const_true=create_var()
var_always(const_true,True)

input_bits=64

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

result2=BV_XOR(x,y)

var_always(OR(BV_XOR(result1, result2)), True)

solution=solve(clauses)
if solution==None:
print "unsat"
return

print "sat"
print "x=%x" % BV_to_number(get_BV_from_solution(x, solution))
print "y=%x" % BV_to_number(get_BV_from_solution(y, solution))
print "step1=%x" % BV_to_number(get_BV_from_solution(step1, solution))
print "step2=%x" % BV_to_number(get_BV_from_solution(step2, solution))
print "result1=%x" % BV_to_number(get_BV_from_solution(result1, solution))
print "result2=%x" % BV_to_number(get_BV_from_solution(result2, solution))