Click on the squares below to configure a tic-tac-toe board. Paste the generated code into the Z3 theorem prover to see if blue can win on the next move.
The tic-tac-toe problem is obviously so simple that no reasonable person would use a SAT solver for it. Sudoku has become a canonical SAT problem, but Sudoku-SAT clauses are difficult enough that a student might benefit from something easier first. Thus, tic-tac-toe.
A interesting design flaw of this program is that it cannot consider if red has already won. The constraints allow only a single white to turn blue (literal true). Implicitly, this means that all other white squares turn red (literal false). If we want to further constrain solutions and check that red has not already won, we need to change the type from Bool to something with more than two possible states.