### OverTheWire Advent Bonanza 2019: [Day 5] Sudo Sudoku

This post is part of a series in which I’ll post writeups for all challenges of the OverTheWire Advent Bonanza 2019 CTF. To see the intro, click here

## Overview

So, Santa’s helpers are very good at Sudoku puzzles, and made a very hard on we need to solve to get the flag. When downloading the archive file, we get a text file named challenge.txt:

```Santa's little helpers are notoriously good at solving Sudoku puzzles.
Because regular Sudoku puzzles are too trivial, they have invented a 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.```

So we got a Sudoku, and a few additional rules that solved Sudoku must fulfill. And from the solved Sudoku, we can get the flag!

## Extracting stuff

How do we approach this? First of all, we need to extract the Sudoku and the rules into a machine readable format. Let’s beginn with the Sudoku. That’s just manual work, and after a few minutes, we have this representation:

``````0 0 0 0 0 0 0 0 1
0 1 2 0 0 0 0 0 0
0 0 0 0 0 0 2 0 0
0 0 0 0 0 0 0 0 2
0 2 0 0 0 0 0 0 0
0 0 0 0 0 0 0 0 0
0 0 0 0 0 0 1 2 0
1 0 0 0 0 2 0 0 0
0 0 0 1 0 0 0 0 0``````

Where 0 stands for needs to be filled in. Now the rules. We can just copy+paste them:

``````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``````

Our solver should be able to handle that

## The plan of solving it

Now to the (relative to the rest) hard part: Solving the Sudoku. But that also turned out to be easy: we can go the script kiddy way and just use someone else’s tools! I talk about z3, a SAT solver. For those who don’t know: A SAT solver solves for variables, so that one or multiple constraints are fulfilled (Please don’t take my word on that, I’m not a expert). So we could just construct constraints, that only a valid, solved Sudoku fulfills, and then add the custom rules, and we’re done!

## Constructing constraints

Now we need to construct those constraints. The first one is simple: Only the numbers from 1 – 9 can be present. So no 0, no 1337, and no 21 🙁 . The second one is also simple: On each row, all numbers must be different. This also applies for columns and blocks. So we have all the constraints we need!

## Actually solving it

After implementing those constraints and also the additional rules in python, we can let z3 do all the work for us in about 1 minute (on my laptop, I bet it would be faster on my PC):

```\$ python solver.py
Solving...
Solution found in 60 seconds!
8 6 4 7 2 9 5 3 1
9 1 2 4 5 3 7 6 8
3 7 5 6 1 8 2 4 9
6 4 9 8 7 5 3 1 2
7 2 1 9 3 6 8 5 4
5 3 8 2 4 1 6 9 7
4 8 6 5 9 7 1 2 3
1 9 7 3 6 2 4 8 5
2 5 3 1 8 4 9 7 6
```

And applying the procedure from challenge.txt, we get the flag:

`AOTW{86472953189247356794813521457639}`

And here is my (ugly) solver script:

```from z3 import *
from time import time

with open("rules.txt", "r") as rf:

for l in rls.split("\n"):
if len(l) <= 0: continue

#Parse rule
ps = l.split(" + ")
ps[-1], r = ps[-1].split(" = ")

sm = 0

for p in ps:
x = int(p) - 1
y = "ABCDEFGHI".index(p)
sm += si[x][y]

s = [[0 for _ in range(9)] for _ in range(9)]

with open("sudoku.txt", "r") as sf:
for y in range(9):
for x in range(9):
s[x][y] = int(l[x * 2])

si = []

#Create int arry
for x in range(9):
six = []

for y in range(9):
six.append(Int("sX%dY%x" % (x, y)))

si.append(six)

slv = Solver()

#Basic Rules
for x in range(9):
for y in range(9):
#Not smaller than 1, not bigger than 9

#If we have a value, force it
if s[x][y] > 0: slv.add(si[x][y] == s[x][y])

#Rows
for y in range(9):
cs = []

for x in range(9):
cs.append(si[x][y])

#Columns
for x in range(9):
cs = []

for y in range(9):
cs.append(si[x][y])

#Blocks
for blk in range(3 * 3):
cs = []

x = (blk % 3) * 3
y = (blk // 3) * 3

for xo in range(3):
for yo in range(3):
cs.append(si[x + xo][y + yo])

#Solve it!
print("Solving...")

st = time()
if slv.check() == sat:
et = time()

print("Solution found in %d seconds!" % (et - st))

m = slv.model()

#Print the solved sudoku
for y in range(9):
for x in range(9):
print("%d " % m[si[x][y]].as_long(), end="")
print()
else:
#Damnit! :(
print("No solution!")
```
Theme: Overlay by Kaira