solv.py

from z3 import *


x0 = BitVec('x0',8)
x1 = BitVec('x1',8)

x2 = BitVec('x2',8)
x3 = BitVec('x3',8)

x4 = BitVec('x4',8)
x5 = BitVec('x5',8)

x6 = BitVec('x6',8)
x7 = BitVec('x7',8)

x8 = BitVec('x8',8)
x9 = BitVec('x9',8)

x10 = BitVec('x10',8) # 10
x11 = BitVec('x11',8) # 11

x12 = BitVec('x12',8) # 12
x13 = BitVec('x13',8) # 13

x14 = BitVec('x14',8) #14
x15 = BitVec('x15',8) #15

s = Solver()

_vars = [x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11,x12,x13,x14,x15]

a = [115, 29, 32, 68, 106, 108, 89, 76, 21, 71, 78, 51, 75, 1, 55, 102]

'''
b[0] = x[2] ^ x[3] ^ x[4] ^ x[8] ^ x[11] ^ x[14]
b[1] = x[0] ^ x[1] ^ x[8] ^ x[11] ^ x[13] ^ x[14]
b[2] = x[0] ^ x[1] ^ x[2] ^ x[4] ^ x[5] ^ x[8] ^ x[9] ^ x[10] ^ x[13] ^ x[14] ^ x[15]
b[3] = x[5] ^ x[6] ^ x[8] ^ x[9] ^ x[10] ^ x[12] ^ x[15]
b[4] = x[1] ^ x[6] ^ x[7] ^ x[8] ^ x[12] ^ x[13] ^ x[14] ^ x[15]
b[5] = x[0] ^ x[4] ^ x[7] ^ x[8] ^ x[9] ^ x[10] ^ x[12] ^ x[13] ^ x[14] ^ x[15]
b[6] = x[1] ^ x[3] ^ x[7] ^ x[9] ^ x[10] ^ x[11] ^ x[12] ^ x[13] ^ x[15]
b[7] = x[0] ^ x[1] ^ x[2] ^ x[3] ^ x[4] ^ x[8] ^ x[10] ^ x[11] ^ x[14]
b[8] = x[1] ^ x[2] ^ x[3] ^ x[5] ^ x[9] ^ x[10] ^ x[11] ^ x[12]
b[9] = x[6] ^ x[7] ^ x[8] ^ x[10] ^ x[11] ^ x[12] ^ x[15]
b[10] = x[0] ^ x[3] ^ x[4] ^ x[7] ^ x[8] ^ x[10] ^ x[11] ^ x[12] ^ x[13] ^ x[14] ^ x[15]
b[11] = x[0] ^ x[2] ^ x[4] ^ x[6] ^ x[13]
b[12] = x[0] ^ x[3] ^ x[6] ^ x[7] ^ x[10] ^ x[12] ^ x[15]
b[13] = x[2] ^ x[3] ^ x[4] ^ x[5] ^ x[6] ^ x[7] ^ x[11] ^ x[12] ^ x[13] ^ x[14]
b[14] = x[1] ^ x[2] ^ x[3] ^ x[5] ^ x[7] ^ x[11] ^ x[13] ^ x[14] ^ x[15]
b[15] = x[1] ^ x[3] ^ x[5] ^ x[9] ^ x[10] ^ x[11] ^ x[13] ^ x[15]
'''
s.add(x2 ^ x3 ^ x4 ^ x8 ^ x11 ^ x14 == a[0])
s.add(x0 ^ x1 ^ x8 ^ x11 ^ x13 ^ x14 == a[1])
s.add(x0 ^ x1 ^ x2 ^ x4 ^ x5 ^ x8 ^ x9 ^ x10 ^ x13 ^ x14 ^ x15 == a[2])
s.add(x5 ^ x6 ^ x8 ^ x9 ^ x10 ^ x12 ^ x15 == a[3])
s.add(x1 ^ x6 ^ x7 ^ x8 ^ x12 ^ x13 ^ x14 ^ x15 == a[4])
s.add(x0 ^ x4 ^ x7 ^ x8 ^ x9 ^ x10 ^ x12 ^ x13 ^ x14 ^ x15 == a[5])
s.add(x1 ^ x3 ^ x7 ^ x9 ^ x10 ^ x11 ^ x12 ^ x13 ^ x15 == a[6])
s.add(x0 ^ x1 ^ x2 ^ x3 ^ x4 ^ x8 ^ x10 ^ x11 ^ x14 == a[7])
s.add(x1 ^ x2 ^ x3 ^ x5 ^ x9 ^ x10 ^ x11 ^ x12 == a[8])
s.add(x6 ^ x7 ^ x8 ^ x10 ^ x11 ^ x12 ^ x15 == a[9])
s.add(x0 ^ x3 ^ x4 ^ x7 ^ x8 ^ x10 ^ x11 ^ x12 ^ x13 ^ x14 ^ x15 == a[10])
s.add(x0 ^ x2 ^ x4 ^ x6 ^ x13 == a[11])
s.add(x0 ^ x3 ^ x6 ^ x7 ^ x10 ^ x12 ^ x15 == a[12])
s.add(x2 ^ x3 ^ x4 ^ x5 ^ x6 ^ x7 ^ x11 ^ x12 ^ x13 ^ x14 == a[13])
s.add(x1 ^ x2 ^ x3 ^ x5 ^ x7 ^ x11 ^ x13 ^ x14 ^ x15 == a[14])
s.add(x1 ^ x3 ^ x5 ^ x9 ^ x10 ^ x11 ^ x13 ^ x15 == a[15])

print(s.check())

m = s.model()

w = [chr((m.eval(_vars[i])).as_long()) for i in range(16)]
print(''.join(w))
#print ('{0};{1};{2};{3};{4};{5};{6};{7};{8};{9};{10};{11};{12};{13};{14};{15}'.format(m[x0],m[x1],m[x2],m[x3],m[x4],m[x5],m[x6],m[x7],m[x8],m[x9],m[x10],m[x11],m[x12],m[x13],m[x14],m[x15]))