Case

Sudoku-variantgenerator

Eigen product

Een Z3-aangedreven generator van variant-sudoku's, met zestien workers die racen naar de eerste geldige puzzel.

Wat & waarom

Een generator voor SudokuPad-variantpuzzels met achtentwintig constraint-types, opgelost en geverifieerd met de Z3-solver. Met een verzorgde CLI en een catalogus via `sp --catalog`.

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 in SudokuPad te spelen. Volgende stap: een web-GUI waarin je zelf constraints kiest en de puzzel direct in SudokuPad opent — zonder de generator te hoeven zien.

Aanpak

Achtentwintig constraint-types gemodelleerd als logische condities voor de Z3-solver.
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-progress-animatie tijdens de race, en een catalogus die alle varianten oplijst.
Output die rechtstreeks oplosbaar is in SudokuPad.

Techniek

Python
Z3-solver
bash
Parallelle workers

Beeld & demo

Zestien parallelle workers racen naar de eerste geldige puzzel — met live Braille-voortgang per worker en de meldingen onderweg, tot er één wint.

Murmur Cipher — XV, German Whispers, palindromen en Kropki, met 0 givens (Very Hard).

Speel zelf →