## About

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 = 25If 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 #Read in the rules with open("rules.txt", "r") as rf: rls = rf.read() def add_rules(slv, si): 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]) - 1 y = "ABCDEFGHI".index(p[0]) sm += si[x][y] #Add new constraint slv.add(sm == r) s = [[0 for _ in range(9)] for _ in range(9)] #Read in sudoku with open("sudoku.txt", "r") as sf: for y in range(9): l = sf.readline() 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 slv.add(si[x][y] >= 1) slv.add(si[x][y] <= 9) #If we have a value, force it if s[x][y] > 0: slv.add(si[x][y] == s[x][y]) #Additional rules add_rules(slv, si) #Rows for y in range(9): cs = [] for x in range(9): cs.append(si[x][y]) slv.add(Distinct(cs)) #Columns for x in range(9): cs = [] for y in range(9): cs.append(si[x][y]) slv.add(Distinct(cs)) #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]) slv.add(Distinct(cs)) #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!")