OverTheWire Advent Bonanza 2019: [Day 5] Sudo Sudoku

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

#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!")

Leave a Reply

Your email address will not be published. Required fields are marked *