Case
Sudoku variant generator
Our own productA Z3-powered generator of variant sudokus — build a puzzle in the web app or from the command line, with sixteen workers racing to the first valid one.
What & why
A web app to build, save and play variant sudokus: pick from dozens of constraint types, have the Z3 solver prove a guaranteed-unique puzzle and determine the difficulty, and open it straight in SudokuPad. A library keeps every puzzle made with its constraints, difficulty and rating. The same generator also runs from the command line.
Making good variant sudokus by hand is slow and error-prone. We wanted a tool that produces a guaranteed-solvable puzzle in seconds, ready to play — and that works just as pleasantly in a polished web app as from the command line.
Approach
- Dozens of constraint types modelled as logical conditions for the Z3 solver.
- A web app to pick constraints, generate and play, with a library that keeps every puzzle made — the same generator also runs from the command line.
- Sixteen parallel workers (on a dedicated 16-core build host) racing to the first valid puzzle — the first wins, the rest are killed; a Braille animation shows the progress.
- Output that is directly solvable in SudokuPad.
Technology
Images & demo
In the web app
-
The swarm searches live: sixteen workers like a field coming into bloom, until one finds a unique puzzle.
-
-
-
On the command line
-
The same swarm on the command line: sixteen workers race with live Braille progress, until one wins.