Case

Sudoku-variantgenerator

Eigen product

Een Z3-aangedreven generator van variant-sudoku's — bouw een puzzel in de web-app of via de command line, met zestien workers die racen naar de eerste geldige.

Wat & waarom

Een web-app om variant-sudoku's te bouwen, te bewaren en te spelen: kies uit tientallen constraint-types, laat de Z3-solver een gegarandeerd unieke puzzel bewijzen en de moeilijkheid bepalen, en open 'm direct in SudokuPad. Een bibliotheek bewaart elke gemaakte puzzel met z'n constraints, moeilijkheid en rating. Dezelfde generator draait ook vanaf de command line.

Goede variant-sudoku's met de hand maken is traag en foutgevoelig. Wij wilden een gereedschap dat in seconden een gegarandeerd oplosbare puzzel oplevert, klaar om te spelen — en dat even prettig werkt in een verzorgde web-app als vanaf de command line.

Aanpak

Tientallen constraint-types gemodelleerd als logische condities voor de Z3-solver.
Een web-app om constraints te kiezen, te genereren en te spelen, met een bibliotheek die elke gemaakte puzzel bewaart — dezelfde generator draait ook vanaf de command line.
Zestien parallelle workers (op een eigen 16-core build-host) laten racen naar de eerste geldige puzzel — de eerste wint, de rest wordt gekild; een Braille-animatie toont de voortgang.
Output die rechtstreeks oplosbaar is in SudokuPad.

Techniek

Python
Z3-solver
Flask (web-app)
bash
Parallelle workers

Beeld & demo

De zwerm zoekt live: zestien workers als een veld dat opbloeit, tot er één een unieke puzzel vindt.

Een gevonden puzzel met givens, klaar om te spelen of te openen in SudokuPad.

Dezelfde zwerm op de command line: zestien workers racen met live Braille-voortgang, tot er één wint.

Open de generator →

Speel zelf →