I’ve always had fun using tools like Z3 and angr. They work almost like magic. You tell them what you want and after some unreasonable amount of time the solution appears.

The OverTheWire Advent Bonanza 2019 CTF featured one of these nice problems which could be easily solved using Z3.

So I took the oppurtunity.

Sudo Sudoku - day 5

The description said:

Santa’s little helpers are notoriously good at solving Sudoku puzzles, so they made a special variant…

    1 2 3   4 5 6   7 8 9  
  +-------+-------+-------+
A | . . . | . . . | . . 1 |
B | . 1 2 | . . . | . . . |
C | . . . | . . . | 2 . . |
  +-------+-------+-------+
D | . . . | . . . | . . 2 |
E | . 2 . | . . . | . . . |
F | . . . | . . . | . . . |
  +-------+-------+-------+
G | . . . | . . . | 1 2 . |
H | 1 . . | . . 2 | . . . |
I | . . . | 1 . . | . . . |
  +-------+-------+-------+

In addition to the standard Sudoku puzzle above, the following equations must also hold:

B9 + B8 + C1 + H4 + H4 = 23
A5 + D7 + I5 + G8 + B3 + A5 = 19
I2 + I3 + F2 + E9 = 15
I7 + H8 + C2 + D9 = 26
I6 + A5 + I3 + B8 + C3 = 20
I7 + D9 + B6 + A8 + A3 + C4 = 27
C7 + H9 + I7 + B2 + H8 + G3 = 31
D3 + I8 + A4 + I6 = 27
F5 + B8 + F8 + I7 + F1 = 33
A2 + A8 + D7 + E4 = 21
C1 + I4 + C2 + I1 + A4 = 20
F8 + C1 + F6 + D3 + B6 = 25

If you then read the numbers clockwise starting from A1 to A9, to I9, to I1 and back to A1, you end up with a number with 32 digits. Enclose that in AOTW{…} to get the flag.

The solution

Here we create an instance of a Z3 solver. It’s purpose is to keep track of all of the constraints we throw at it.

s = z3.Solver()

Now we create symbolic variables. Each one of them represents single integer in the sudoku grid.

x_axis = [1, 2, 3, 4, 5, 6, 7, 8, 9]
y_axis = [chr(x) for x in range(ord('A'), ord('J'))]

sudoku = [[0]*9 for i in range(9)]

for idx, var in enumerate(itertools.product(y_axis, x_axis)):
    sudoku[int(idx / 9)][idx % 9] = z3.Int(f'{var[0]}{var[1]}')

It’s time to apply the constraints! Let’s begin with the basic sudoku rules. All of the values must be between 1 and 9.

for ar in sudoku:
    for var in ar:
        s.add(z3.And(var <= 9, var >= 1))

Values in rows must be distinct.

for ar in sudoku:
    for var1, var2 in itertools.combinations(ar, 2):
        s.add(var1 != var2)

The same applies to columns.

for col_nr in range(9):
    for idx1, idx2 in itertools.combinations(range(9), 2):
        s.add(sudoku[idx1][col_nr] != sudoku[idx2][col_nr])

Also every one of small rectangles must contain every value exactly once.

def distinct_rectangle(idx_x, idx_y):
    indices = []
    for i in range(3):
        for j in range(3):
            indices.append((idx_x + i, idx_y + j))

    for loc1, loc2 in itertools.combinations(indices, 2):
        s.add(
            sudoku[loc1[0]][loc1[1]] != sudoku[loc2[0]][loc2[1]]
        )

distinct_rectangle(0, 0)
distinct_rectangle(3, 0)
distinct_rectangle(6, 0)

distinct_rectangle(0, 3)
distinct_rectangle(3, 3)
distinct_rectangle(6, 3)

distinct_rectangle(0, 6)
distinct_rectangle(3, 6)
distinct_rectangle(6, 6)

Of course we have to set the fixed values.

def idx(x):
    if isinstance(x, str):
        return ord(x) - ord('A')
    else:
        return x - 1

s.add(sudoku[0][8] == 1)
s.add(sudoku[1][1] == 1)
s.add(sudoku[1][2] == 2)
s.add(sudoku[2][6] == 2)

s.add(sudoku[3][8] == 2)
s.add(sudoku[4][1] == 2)

s.add(sudoku[6][6] == 1)
s.add(sudoku[6][7] == 2)
s.add(sudoku[7][0] == 1)
s.add(sudoku[7][5] == 2)
s.add(sudoku[8][3] == 1)

Lastly we apply custom constraints.

# B9 + B8 + C1 + H4 + H4 = 23
s.add(
    sudoku[idx('B')][idx(9)] + 
    sudoku[idx('B')][idx(8)] + 
    sudoku[idx('C')][idx(1)] + 
    sudoku[idx('H')][idx(4)] + 
    sudoku[idx('H')][idx(4)] == 23
)

# A5 + D7 + I5 + G8 + B3 + A5 = 19
s.add(
    sudoku[idx('A')][idx(5)] + 
    sudoku[idx('D')][idx(7)] + 
    sudoku[idx('I')][idx(5)] + 
    sudoku[idx('G')][idx(8)] + 
    sudoku[idx('B')][idx(3)] + 
    sudoku[idx('A')][idx(5)] == 19
)

# I2 + I3 + F2 + E9 = 15
s.add(
    sudoku[idx('I')][idx(2)] + 
    sudoku[idx('I')][idx(3)] + 
    sudoku[idx('F')][idx(2)] + 
    sudoku[idx('E')][idx(9)] == 15
)

# I7 + H8 + C2 + D9 = 26
s.add(
    sudoku[idx('I')][idx(7)] + 
    sudoku[idx('H')][idx(8)] + 
    sudoku[idx('C')][idx(2)] + 
    sudoku[idx('D')][idx(9)] == 26
)

# I6 + A5 + I3 + B8 + C3 = 20
s.add(
    sudoku[idx('I')][idx(6)] + 
    sudoku[idx('A')][idx(5)] + 
    sudoku[idx('I')][idx(3)] + 
    sudoku[idx('B')][idx(8)] + 
    sudoku[idx('C')][idx(3)] == 20
)

# I7 + D9 + B6 + A8 + A3 + C4 = 27
s.add(
    sudoku[idx('I')][idx(7)] + 
    sudoku[idx('D')][idx(9)] + 
    sudoku[idx('B')][idx(6)] + 
    sudoku[idx('A')][idx(8)] + 
    sudoku[idx('A')][idx(3)] + 
    sudoku[idx('C')][idx(4)] == 27
)

# C7 + H9 + I7 + B2 + H8 + G3 = 31
s.add(
    sudoku[idx('C')][idx(7)] + 
    sudoku[idx('H')][idx(9)] + 
    sudoku[idx('I')][idx(7)] + 
    sudoku[idx('B')][idx(2)] + 
    sudoku[idx('H')][idx(8)] + 
    sudoku[idx('G')][idx(3)] == 31
)

# D3 + I8 + A4 + I6 = 27
s.add(
    sudoku[idx('D')][idx(3)] + 
    sudoku[idx('I')][idx(8)] + 
    sudoku[idx('A')][idx(4)] + 
    sudoku[idx('I')][idx(6)] == 27
)

# F5 + B8 + F8 + I7 + F1 = 33
s.add(
    sudoku[idx('F')][idx(5)] + 
    sudoku[idx('B')][idx(8)] + 
    sudoku[idx('F')][idx(8)] + 
    sudoku[idx('I')][idx(7)] + 
    sudoku[idx('F')][idx(1)] == 33
)

# A2 + A8 + D7 + E4 = 21
s.add(
    sudoku[idx('A')][idx(2)] + 
    sudoku[idx('A')][idx(8)] + 
    sudoku[idx('D')][idx(7)] + 
    sudoku[idx('E')][idx(4)] == 21
)

# C1 + I4 + C2 + I1 + A4 = 20
s.add(
    sudoku[idx('C')][idx(1)] + 
    sudoku[idx('I')][idx(4)] + 
    sudoku[idx('C')][idx(2)] + 
    sudoku[idx('I')][idx(1)] + 
    sudoku[idx('A')][idx(4)] == 20
)

# F8 + C1 + F6 + D3 + B6 = 25
s.add(
    sudoku[idx('F')][idx(8)] + 
    sudoku[idx('C')][idx(1)] + 
    sudoku[idx('F')][idx(6)] + 
    sudoku[idx('D')][idx(3)] + 
    sudoku[idx('B')][idx(6)] == 25
)

This is where the magic happens. s keeps track of all of the contraints that we have applied to the set of symbolic variables in the sudoku grid. check() method checks for the satisfiability of the constraints. In our case it prints sat meaning that Z3 was able to simplify our constraints and satisfy them. It means Z3 constructed a model in which the symbolic variables can be mapped to concrete integers. Generally there might be more than one solution to the given constraints, but here the task authors made sure that only one solution exists. So lets get it!

print(s.check())
model = s.model()

Using model.evaluate(var) we get a concrete value for the symbolic variable var within model model.

solution = []
for ar in sudoku:
    row = []
    for var in ar:
        row.append(model.evaluate(var))
    solution.append(row)

Now let’s print the solved sudoku!

for ar in solution:
    for e in ar:
        print(e, end='')
    print()

flag = (solution[0] + 
    [solution[i][8] for i in range(1, 8)] +
    solution[8][::-1] + 
    [solution[i][0] for i in reversed(range(1, 8))])
flag = ''.join(map(str,flag))

print('AOTW{' + flag + '}')

After a little bit of processing we get the flag: AOTW{86472953189247356794813521457639}. Full code can be found here.