In [ ]:
%install_ext https://raw.github.com/cjdrake/ipython-magic/master/gvmagic.py
In [ ]:
%load_ext gvmagic
In [ ]:
from pyeda.inter import *
In [ ]:
from pyeda.logic.addition import ripple_carry_add as RCA
from pyeda.logic.addition import kogge_stone_add as KSA
In [ ]:
A = exprvars('a', 32)
B = exprvars('b', 32)
In [ ]:
S_rca, C_rca = RCA(A, B)
S_ksa, C_ksa = KSA(A, B)
The expression tree is very different:
In [ ]:
%dotobjs S_rca[2].simplify(), S_ksa[2].simplify()
If XOR(f, g) is UNSAT, functions f and g are equivalent.
But sum bit 9 is a deep expression. Converting to CNF is impossible, so use backtracking:
In [ ]:
f = Xor(S_rca[9], S_ksa[9])
In [ ]:
%timeit f.satisfy_one()
Let's see if we can do better using the Tseitin transformation, and PicoSAT extension:
In [ ]:
g = f.tseitin()
In [ ]:
%timeit g.satisfy_one()
Success!
Verify that both functions returned UNSAT:
In [ ]:
assert f.satisfy_one() is None and g.satisfy_one() is None
In [ ]: