(The following text has been copypasted to the SAT/SMT by example.)

I once wrote about quite bizarre XOR alternative I've found using aha! superoptimizer: https://github.com/DennisYurichev/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| --- +---+ -2 +---+ |ADD| --- +---+ 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:] result1=adder(adder(product, x)[0], y)[0] 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/DennisYurichev/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 --- +---+ +---+ +---+ +- +---+ |ADD| --- +---+ 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) # add 1 one=alloc_BV(len(tmp)) BV_always(one,n_to_BV(1, len(tmp))) return adder(tmp, one)[0]

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)) result1=adder(adder(step2, x)[0], y)[0] 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))

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

Please drop me email about any bug(s) and suggestion(s):