Example

Using the constraints and computations specified in the binary, we'll write a Z3 script to give us our good serial.

In [1]:
# Imports

import z3

Initialisation

In [2]:
# Initialising required variables

# Z3's solver engine
s = z3.Solver()

We have to create an array such that operations could be done on it for the first transformation loop.

In [3]:
# Declare a bitvector variable 
x = z3.BitVec('x', 8)

# 'sexpr' method shows the internal representation.
(x + 2).sexpr()
Out[3]:
'(bvadd x #x02)'

Which translates to: bit vector addition of x with the integral value 2.

In [4]:
# Input serial array of length 13, since the serial length is 13.
serial = []

for i in range(13):
    serial.append(z3.BitVec("serial_{}".format(i), 32))

serial
Out[4]:
[serial_0,
 serial_1,
 serial_2,
 serial_3,
 serial_4,
 serial_5,
 serial_6,
 serial_7,
 serial_8,
 serial_9,
 serial_10,
 serial_11,
 serial_12]
In [5]:
# v4 initialised with 3.
running_sum = [3]

Constraints

Implementing constraints for the value boundations on every character in the input.

In [6]:
for digit in serial:
    s.add(z3.And(digit>48, digit<=57))

Check value of running sum at every iteration.

In [7]:
# Append sum to a running sums array, and add it as a constraint at every interation.
for i in range((len(serial)-1)):
    current_sum = z3.BitVec("sum_{}".format(i), 32)
    s.add(current_sum==running_sum[-1]+((2*running_sum[-1])^(serial[i]-48)))
    running_sum.append(current_sum)
    
running_sum[-1]
Out[7]:
sum_11

Constraint on the last digit of the serial.

In [8]:
s.add(serial[-1]==(running_sum[-1]%10+48))

Constraint Solving

Check if the problem is satisfiable.

In [9]:
s.check()
Out[9]:
sat
In [10]:
if s.check() == z3.sat:
    m = s.model()
m
Out[10]:
[sum_3 = 247, sum_0 = 10, sum_5 = 2215, sum_6 = 6646, sum_7 = 19940, sum_1 = 27, sum_8 = 59823, sum_2 = 82, sum_9 = 179465, sum_4 = 736, sum_10 = 538396, serial_0 = 49, serial_5 = 55, serial_4 = 55, serial_11 = 52, serial_9 = 52, serial_3 = 49, serial_12 = 50, serial_10 = 49, serial_8 = 51, serial_7 = 50, serial_1 = 53, serial_6 = 49, serial_2 = 49, sum_11 = 1615192]

Cleaning up and representing the answer in a readable form:

In [11]:
# Now m is a map. We dereference the values of serial required from it.
print("Serial object:", serial)

inp = []
for digit in serial:
    # 'as_long' method used to convert vector value to long type.
    print("Value of", digit, "is:", m[digit])
    inp.append(m[digit].as_long())
    
inp

Serial object: [serial_0, serial_1, serial_2, serial_3, serial_4, serial_5, serial_6, serial_7, serial_8, serial_9, serial_10, serial_11, serial_12]
Value of serial_0 is: 49
Value of serial_1 is: 53
Value of serial_2 is: 49
Value of serial_3 is: 49
Value of serial_4 is: 55
Value of serial_5 is: 55
Value of serial_6 is: 49
Value of serial_7 is: 50
Value of serial_8 is: 51
Value of serial_9 is: 52
Value of serial_10 is: 49
Value of serial_11 is: 52
Value of serial_12 is: 50
Out[11]:
[49, 53, 49, 49, 55, 55, 49, 50, 51, 52, 49, 52, 50]

These bytes give you the value of the good serial. Convert the ordinal values to their ASCII equivalents.

In [12]:
solution = "".join([chr(x) for x in inp])
solution
Out[12]:
'1511771234142'