Sind grosse Sudoku eindeutig lösbar? Wie wir das maschinell beweisen

Ein Sudoku, das mehrere Lösungen zulässt, ist kein Sudoku – es ist Raten. Bei einem 9×9-Rätsel merkt man das schnell. Bei 4'096 Feldern kann das kein Mensch mehr von Hand prüfen. Deshalb übernimmt bei uns eine Maschine den Beweis: Jedes Poster, das wir drucken, hat garantiert genau eine Lösung.

Was «eindeutig lösbar» wirklich bedeutet

Ein Sudoku ist eindeutig lösbar, wenn es aus den vorgegebenen Zahlen heraus auf genau einem Weg zu Ende gefüllt werden kann. Nicht «man findet eine Lösung», sondern: Es gibt keine zweite. Genau das unterscheidet ein sauberes Logikrätsel von einem Gitter, das man nur mit Glück und Ausprobieren zu Ende bringt.

Die Regel bleibt dabei immer dieselbe, egal wie gross das Feld ist: In jeder Zeile, jeder Spalte und jeder Region steht jedes Zeichen genau einmal. Bei einem klassischen 9×9 sind das die Zahlen 1 bis 9. Bei unseren grossen Rätseln wächst der Zeichensatz mit – ein 32×32-Monster füllt 1'024 Felder, ein 64×64-Kolossal 4'096.

Zuerst die Lösung, dann das Rätsel

Viele stellen sich das Erstellen falsch herum vor. Wir setzen nicht ein paar Zahlen und hoffen, dass etwas Lösbares entsteht. Der Ablauf ist umgekehrt:

Zuerst erzeugt der Generator ein komplett gefülltes, regelkonformes Gitter – eine vollständige, gültige Lösung. Bei den grossen Formaten wird das Feld dafür in Regionen aufgeteilt: entweder in rechteckige Blöcke (so beim Titan mit 48×48 und beim Kolossal mit 64×64) oder in frei geformte Gebiete, die wie Puzzleteile ineinandergreifen (beim Einstieg mit 24×24 und beim Monster mit 32×32). In jeder dieser Regionen kommt am Ende jedes Zeichen genau einmal vor.

Erst wenn diese vollständige Lösung steht, wird daraus das Rätsel geschnitten.

Der eigentliche Beweis: Zahlen wegnehmen, bis es kippt

Jetzt beginnt der Teil, der die Eindeutigkeit sichert. Der Generator entfernt Feld für Feld eine Zahl – und prüft nach jedem einzelnen Schritt mit einem deterministischen Löser, ob das Rätsel noch genau eine Lösung hat.

Dieser Löser arbeitet nicht mit Raten. Er sucht in jedem Schritt das Feld mit den wenigsten verbleibenden Möglichkeiten (das ist die sogenannte MRV-Strategie) und zieht logisch zwingende Schlüsse, solange es sie gibt. Findet er an irgendeiner Stelle einen zweiten gültigen Weg, ist bewiesen: Dieses Feld durfte nicht leer sein. Die Zahl kommt zurück, und der Generator versucht es an anderer Stelle.

So entsteht ein Rätsel, das so weit wie möglich ausgedünnt ist – aber keine Zahl zu viel verloren hat. Am Ende steht die maschinelle Garantie: genau eine Lösung, mathematisch geprüft, nicht geschätzt.

Warum das gerade bei XXL-Sudoku zählt

Bei einem kleinen Rätsel kann ein geübter Mensch die Eindeutigkeit im Kopf abschätzen. Bei 2'304 oder 4'096 Feldern ist das ausgeschlossen – die Zahl der möglichen Füllungen ist astronomisch. Ohne maschinellen Beweis müsste man dem Rätsel einfach vertrauen. Wir müssen nicht vertrauen: Jedes Poster, das das Haus verlässt, hat den Test bestanden, bevor es überhaupt gedruckt wird.

Das ist der Grund, warum wir unsere Rätsel guten Gewissens als «eine Lösung» verkaufen. Es ist kein Werbeversprechen, sondern das Ergebnis eines Prüfschritts, den jedes einzelne Gitter durchläuft.