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.

Sudo Sudoku

Points: 86

Solves: 229

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

Download: 2a3fad4ea8987eb63b5abdea1c8bdc75d4f2e6b087388c5e33cec99136b4257a-sudosudoku.tar.xz

Downloading and extracting the file gave the following:

**challenge.txt**

1 | Santa's little helpers are notoriously good at solving Sudoku puzzles. |

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:

**sudoku-z3.py** from Github user ppmx

1 | #!/usr/bin/env python3 |

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:

1 | $ python3 solve.py |

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.

1 | # assure that special constraints are met |

Now running `solve.py`

gave the result:

1 | [+] trying to solve it with z3 |

The challenge noted that the flag was the values starting from the top left and going clockwise around the sudoku board. Thus, the final flag was:

1 | AOTW{86472953189247356794813521457639} |

A very simple and ideal use-case for the Z3 solver!