Another writeup for a fairly simple challenge as a part of OverTheWire’s Advent Bonanza 2019. Day 5 of the Advent Bonanza challenges was a straightforward Sudoku challenge with constraints.
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.
Looks like all I have to do is solve the Sudoku puzzle with the constraints. What I could do is sit down and actually do the puzzle by hand, but I wanted to take this opportunity to show off an awesome tool known as The Z3 Theorem Prover from Microsoft Research. Z3 uses a variety of solvers to solve equations under constraints. This is perfect here as there are already open source sudoku solvers online that use Z3. A quick online search for sudoku solver z3 and the first link come up with this Github project by Github user ppmx. Credits to this user for a very easy to use and easy to understand sudoku solver using Z3! Here’s what their sudoku solver script looks like:
if any(c notin"123456789."for c in puzzle) or len(puzzle) != 81: raise Exception("got invalid puzzle format")
elements = cross("ABCDEFGHI", "123456789") s.values = {e: v for e,v in zip(elements, puzzle)} return s
def__init__(self, values=dict()): # mapping cells -> "123456789." where the dot represents an empty cell # cells = cross product of "ABCDEFGHI" and "123456789" self.values = values
# we define some additional informations that may be used by a solving function: rows, cols = "ABCDEFGHI", "123456789" self.elements = cross(rows, cols)
self.unitlist = [] self.unitlist += [cross(rows, c) for c in cols] self.unitlist += [cross(r, cols) for r in rows] self.unitlist += [cross(rs, cs) for rs in ["ABC", "DEF", "GHI"] for cs in ["123", "456", "789"]]
self.units = {e: [u for u in self.unitlist if e in u] for e in self.elements}
defis_solved(self): # assure that every cell holds a single value between 1 and 9: ifnot all(k in"123456789"for k in self.values.values()): returnFalse
# assure that every cell of every unit is unique in the proper unit: unitsolved = lambda u: set([self.values[e] for e in u]) == set("123456789") return all(unitsolved(u) for u in self.unitlist)
def__str__(self): lines, elements = [], cross("ABCDEFGHI", "123456789")
print("[+] Puzzle:", ''.join(self.values[e] for e in elements))
for index_row, row in enumerate("ABCDEFGHI"): if index_row % 3 == 0: lines.append("+–––––––––+–––––––––+–––––––––+")
line = '' for index_col, col in enumerate("123456789"): line += "{1} {0} ".format(self.values[row + col], '|'if index_col % 3 == 0else'') lines.append(line + '|')
defZ3Solving(sudoku): from z3 import Solver, Int, Or, Distinct, sat
elements = cross("ABCDEFGHI", "123456789") symbols = {e: Int(e) for e in elements}
# first we build a solver with the general constraints for sudoku puzzles: s = Solver()
# assure that every cell holds a value of [1,9] for symbol in symbols.values(): s.add(Or([symbol == i for i in range(1, 10)]))
# assure that every row covers every value: for row in"ABCDEFGHI": s.add(Distinct([symbols[row + col] for col in"123456789"]))
# assure that every column covers every value: for col in"123456789": s.add(Distinct([symbols[row + col] for row in"ABCDEFGHI"]))
# assure that every block covers every value: for i in range(3): for j in range(3): s.add(Distinct([symbols["ABCDEFGHI"[m + i * 3] + "123456789"[n + j * 3]] for m in range(3) for n in range(3)]))
# now we put the assumptions of the given puzzle into the solver: for elem, value in sudoku.values.items(): if value in"123456789": s.add(symbols[elem] == value)
print("[+] trying to solve it with z3") s_solved = Z3Solving(s) print("[+] it is solved:", s_solved.is_solved()) print(s_solved)
if __name__ == "__main__": from sys import argv
if len(argv) != 2: print("[!] we are using some test puzzle due to missing argument") main("4.....8.5.3..........7......2.....6.....8.4......1.......6.3.7.5..2.....1.4......") else: main(argv[1])
I am far from an advanced user of Z3 but the above script is straightforward enough to understand. This guide by Github user ericpony is also a great place to start to understand how to use Z3 in Python.
Z3 needs to know what kind of values it needs to solve for. We also give symbols for those values, basically like variables.
This happens on line 79-80 where values A1-A9, B1-B9, etc. are added as symbols.
Line 83 initializes the Z3 solver.
Line 77 shows imports from Z3 that can be used to define some of the relationships between variables, like Or and Distinct.
Constraints are added to the solver object and then Solver.check() is called to tell Z3 to try to solve for all the constraints given.
To input my own constraints into the script, I had to understand what the script was doing first. The function Z3Solving is where all the magic happens.
Lines 86-87 ensure that all values in the solution are between 1 and 9 inclusive.
Lines 90-100 ensure that every row, column, and 3x3 block include all values 1 to 9 inclusive and are distinct.
Lines 103-105 ensure that the starting board that is given to the program is satisfied.
For solving this problem, it seems like it would be adequate to place my custom constraints right after line 100.
To make it easier for myself, I replaced the string on line 130 with the starting sudoku problem given to me in the challenge. I saved the script as solve.py and ran it just to make sure I was able to get a solution:
Looks like it works! Now all that is left to do is add all of the constraints from the challenge. What was also nice is that the script from ppmx and the challenge refer to each individual cell of the sudoku board in the same manner. For example, I5 on the sudoku board in the challenge is referenced by symbols['I5'] in the script. Solving this challenge was as easy as adding my own constraints after line 100. I actually wrote a script to take in the constraints and output the following Python code cause I got too lazy to type it all out myself.