Constructing strong starters of orders $3p$: triplication with SAT solver

Die Arbeit stellt eine neue Tripplikations-Methode vor, die mithilfe eines SAT-Lösers (z3) starke Starter in zyklischen Gruppen der Ordnung $3p$aus solchen der Ordnung$p$ konstruiert und damit einen wichtigen Schritt zur Überprüfung von Hortons Vermutung unternimmt.

Das Wesentliche

Stellen Sie sich vor, Sie sind ein Architekt, der riesige, perfekte Muster für ein riesiges Parkett entwirft. In der Welt der Mathematik heißen diese Muster „Starke Starter" (Strong Starters). Sie sind spezielle Anordnungen von Zahlenpaaren, die eine sehr strenge Regel erfüllen: Wenn Sie die Zahlen in jedem Paar addieren oder subtrahieren, dürfen keine zwei Ergebnisse gleich sein. Es ist wie ein perfektes Puzzle, bei dem jedes Teil genau an einer Stelle passt und nichts doppelt vorkommt.

Das Problem: Diese perfekten Muster lassen sich leicht für kleine Parkette (z. B. mit 7 oder 13 Kacheln) bauen. Aber was ist, wenn Sie ein Parkett bauen wollen, das genau dreimal so groß ist wie ein kleines? Zum Beispiel 21 Kacheln (3 mal 7) oder 39 Kacheln (3 mal 13)?

Hier kommt die Idee dieses Papers ins Spiel: „Triplication" (Verdreifachung).

Die Grundidee: Vom Kleinen zum Dreifachen

Die Autoren (Oleg, Sergey und Margo) haben eine clevere Methode entwickelt, um aus einem kleinen, perfekten Muster (einem Starter der Ordnung $p$) ein riesiges Muster der Ordnung $3p$ zu bauen.

Stellen Sie sich das so vor:

1. Der Bauplan (Der kleine Starter): Sie haben einen fertigen, kleinen Bauplan für ein Haus mit 7 Räumen.
2. Der Schlüssel (Der Key): Sie brauchen einen geheimen Code (eine Zahl), um das Haus zu erweitern.
3. Die Erweiterung (Die Triplication-Tabelle): Sie nehmen den kleinen Bauplan und kopieren ihn dreimal, aber mit kleinen mathematischen Tricks (Addition und Subtraktion). Das ergibt eine Art „Rohbau" für das große Haus.

Das Rätsel: Das modulare Sudoku

Jetzt haben Sie den Rohbau, aber er ist noch nicht fertig. Es fehlen die genauen Farben oder Nummern für die Wände, damit das große Haus die strengen Regeln erfüllt.

Hier kommt das Sudoku ins Spiel. Aber kein normales Sudoku mit Zahlen 1 bis 9. Es ist ein Sudoku im Modulo-3-System.

• Statt Zahlen von 1 bis 9 gibt es nur drei Farben: Rot, Gelb, Blau (oder mathematisch: 0, 1, 2).
• Sie müssen diese drei Farben so in den Rohbau einfüllen, dass in jeder Zeile und Spalte bestimmte Regeln eingehalten werden (z. B. keine zwei gleichen Farben in einer Reihe, bestimmte Summen dürfen nicht gleich sein).

Wenn Sie dieses Sudoku-Rätsel lösen, haben Sie die genauen Anweisungen, um aus dem kleinen Starter das große, perfekte Muster zu konstruieren.

Der Computer als Detektiv (Der SAT-Solver)

Das Schwierige ist: Dieses Sudoku ist oft extrem komplex. Es gibt Milliarden von Möglichkeiten, die Farben zu verteilen, aber nur wenige funktionieren. Ein Mensch würde ewig brauchen, um das zu lösen.

Dafür nutzen die Autoren einen SAT-Solver (hier das Tool „z3").

• Was ist das? Stellen Sie sich den SAT-Solver als einen super-schnellen, unermüdlichen Detektiv vor. Ihm geben Sie die Regeln des Rätsels (die mathematischen Bedingungen) und er schreit: „Ich habe die Lösung!" oder „Es gibt keine Lösung!".
• Der Computer prüft blitzschnell alle Kombinationen, bis er die perfekte Anordnung der Farben findet.

Warum ist das wichtig?

Es gibt eine berühmte Vermutung (die Horton-Vermutung), die besagt, dass solche perfekten Muster für fast alle ungeraden Zahlen existieren, außer für ein paar sehr kleine Ausnahmen. Aber niemand konnte beweisen, dass sie für Zahlen wie 21, 33, 39 usw. wirklich existieren, wenn diese durch 3 teilbar sind.

Die Autoren sagen: „Wir beweisen es nicht theoretisch (noch nicht), aber wir zeigen, wie man sie praktisch baut."

• Sie haben gezeigt, dass man fast immer ein Sudoku-Rätsel lösen kann, um das große Muster zu erhalten.
• Sie haben getestet, wie schnell Computer das machen. Bei kleinen Zahlen geht es in Sekunden, bei größeren Zahlen dauert es Minuten oder Stunden, aber es funktioniert.

Zusammenfassung in einer Metapher

Stellen Sie sich vor, Sie wollen ein riesiges, perfektes Mosaik legen.

1. Sie haben ein kleines, perfektes Muster (den Starter).
2. Sie wollen es vergrößern, indem Sie es verdreifachen.
3. Sie bauen eine Gerüststruktur (die Triplication-Tabelle), die auf dem kleinen Muster basiert.
4. Das Gerüst ist aber noch leer. Sie müssen die Kacheln (die Zahlen) einsetzen.
5. Die Regeln, wie die Kacheln gesetzt werden müssen, sind wie ein Sudoku-Rätsel, bei dem es nur drei Farben gibt.
6. Ein Computer-Detektiv (SAT-Solver) löst dieses Sudoku in Sekunden.
7. Sobald das Sudoku gelöst ist, können Sie das riesige, perfekte Mosaik zusammenbauen.

Das Fazit: Die Autoren haben einen neuen, praktischen Weg gefunden, um diese komplexen mathematischen Strukturen zu erschaffen, indem sie ein kleines Puzzle in ein riesiges verwandeln und einen Computer helfen lassen, die fehlenden Teile zu finden. Es ist ein Brückenschlag zwischen reiner Mathematik und moderner Computertechnologie.

Technische Zusammenfassung

1. Problemstellung und Hintergrund

Das Paper adressiert das Problem der Konstruktion von starken Startern (strong starters) in zyklischen Gruppen $\mathbb{Z}_n$ für ungerade Ordnungen $n$, die durch 3 teilbar sind ($n = 3p$).

• Definition eines starken Starters: Ein Starter $S$ in einer additiven abelschen Gruppe $G$ der Ordnung $n$ ist eine Partition der Menge $G^* = G \setminus \{0\}$ in $k = (n-1)/2$ Paare $\{a_i, b_i\}$. Ein Starter heißt stark, wenn:
  1. Alle Paarsummen $a_i + b_i$ modulo $n$ verschieden und ungleich 0 sind.
  2. Alle Differenzen $\pm(a_i - b_i)$ modulo $n$ verschieden und ungleich 0 sind (d.h. sie bilden $G^*$).
• Existenzlücke: Es ist bekannt, dass starke Starter für alle ungeraden Ordnungen $n \ge 7$ existieren, bei denen $3 \nmid n$. Für den Fall, dass$3 \mid n$(insbesondere$n=3p$), ist die Existenz jedoch nur teilweise bewiesen. Die **Horton-Vermutung** (1989) besagt, dass starke Starter für alle ungeraden Ordnungen existieren, außer für$n=3, 5, 9$. Bisherige theoretische Ergebnisse decken nur Fälle mit$n < 1000$oder spezifische Bedingungen für$n=3^r p$ab. Für große$n=3p$(wobei$p$ teilerfremd zu 3 ist) fehlt ein allgemeiner Existenzbeweis oder eine konstruktive Methode.

Das Ziel des Papers ist es, eine neue konstruktive Methode vorzustellen, um starke Starter der Ordnung $3p$aus starken Startern der Ordnung$p$ zu generieren.

2. Methodik: Triplication und das modulare Sudoku-Problem

Die Autoren stellen eine Methode namens „Triplication" vor. Diese reduziert das Konstruktionsproblem für Ordnung $3p$ auf ein Constraint-Satisfaction-Problem (CSP) modulo 3.

A. Der Triplication-Prozess

Gegeben sei ein starker Starter $T$ der Ordnung $p$ (wobei $\gcd(p,3)=1$) und ein Schlüssel $t \in \{0, \dots, p-1\}$.

1. Erweiterung ($\Sigma_p$): Aus $T$ und $t$ wird eine Tabelle $\Sigma_p$ (die „Triplication-Tabelle") konstruiert. Diese besteht aus:
   • Einer Top-Zeile mit dem Paar $(t, t)$.
   • $q = (p-1)/2$ regulären Zeilen. Jede Zeile $i$ enthält drei Paare, die aus dem $i$-ten Paar $(x_i, y_i)$ von $T$ durch Addition und Subtraktion von $t$ modulo $p$ abgeleitet werden:
     • Spalte 1: $(x_i, y_i)$
     • Spalte 2: $(x_i+t, y_i+t)$
     • Spalte 3: $(t-y_i, t-x_i)$
2. Struktur von $\Sigma_p$: Die Tabelle erfüllt spezifische arithmetische Eigenschaften bezüglich der Differenzen und Summen modulo $p$.

B. Das modulare Sudoku-Problem ($\Sigma_3$)

Das eigentliche Konstruktionsproblem besteht darin, eine Tabelle $\Sigma_3$ mit Werten in $\{0, 1, 2\}$ zu finden, die bestimmte Constraints erfüllt. Diese Tabelle wird dann mit $\Sigma_p$ mittels des Chinesischen Restsatzes (CRT) kombiniert, um den finalen Starter $S$ der Ordnung $3p$ zu erhalten.

Die Constraints für $\Sigma_3$ sind:

1. Reihen-Constraints: In jeder regulären Zeile müssen die Differenzen $U_i - V_i$ modulo 3 alle verschieden sein (d.h. $\{0, 1, 2\}$).
2. Schwache Mengen-Constraints (Weak Sets): Basierend auf den Summen der Paare in $\Sigma_p$ (modulo $p$).
   • Wenn Paare in $\Sigma_p$ die gleiche Summe $s \neq 0$ haben, müssen ihre Summen in $\Sigma_3$ (modulo 3) verschieden sein.
   • Wenn Paare in $\Sigma_p$ die Summe $0$haben, müssen ihre Summen in$\Sigma_3$ verschieden und ungleich 0 sein.
3. Farb-Dreifach-Constraints (Monochrome Sets): Für jeden Wert $c \in \{0, \dots, p-1\}$, der in $\Sigma_p$ an bestimmten Positionen auftritt, müssen die entsprechenden Werte in $\Sigma_3$ (modulo 3) alle verschieden sein. Für den Wert 0 wird eine Dummy-Variable hinzugefügt, um eine Dreiergruppe zu bilden.

C. Lösung durch SAT-Solver

Da das Finden einer gültigen Belegung für $\Sigma_3$ ein komplexes CSP ist, verwenden die Autoren den allgemeinen SAT-Solver z3 (von Microsoft), um die Constraints zu lösen. Die Eingabe für den Solver sind die aus $T$ und $t$ abgeleiteten Constraints.

3. Wichtige theoretische Beiträge

• Theorem 1 (Existenz): Wenn eine Lösung für das modulare Sudoku-Problem existiert, dann definiert die Kombination aus $\Sigma_p$ und der Lösung $\Sigma_3$ (via CRT) einen starken Starter der Ordnung $3p$.
• Theorem 2 (Notwendige Bedingung): Das Sudoku-Problem hat keine Lösung, wenn der Schlüssel $t$ gleich 0 ist oder wenn $t$ einer der Paarsummen des Basis-Starters $T$ entspricht ($t \in \hat{T} \cup \{0\}$). Dies ist eine notwendige Bedingung für die Lösbarkeit.
• Theorem 3 (Symmetrie): Die Lösungen des Sudoku-Problems treten in Paaren auf. Eine Permutation, die die Werte 1 und 2 vertauscht, transformiert eine gültige Lösung in eine andere gültige Lösung.
• Inverse Problematik: Die Autoren stellen einen Algorithmus vor, um zu prüfen, ob ein gegebener Starter der Ordnung $3p$durch Triplication entstanden ist. Dies basiert auf der Analyse der Zeilenstruktur modulo$p$.

4. Ergebnisse und experimentelle Evaluation

Die Autoren haben die Methode in Python unter Verwendung der Bibliothek z3-solver implementiert und umfangreiche numerische Experimente durchgeführt.

• Datensätze:
  • Serie 1: Basis-Starter für Ordnungen $m < 100$ (alle zulässigen Schlüssel $t$).
  • Serie 2: Größere Ordnungen ($100 < m < 500$) mit zufälligen Schlüsselwerten.
  • Serie 3: Feste Ordnung $m=101$, alle zulässigen Schlüssel, 10 Wiederholungen pro Schlüssel zur Analyse der Varianz.
• Leistung (Laufzeit):
  • Die Lösungszeit $\tau$ steigt mit der Ordnung $m$. Für $m < 100$ folgt die Zeit grob einer heuristischen Funktion $\tau \approx 0.023 \cdot m^2 \ln m$.
  • Für $m > 200$ wird die Komplexität höher, und die Laufzeit variiert stark (nicht monoton), wobei Sprünge bei bestimmten Ordnungen (z.B. zwischen 335 und 395) beobachtet wurden.
  • Trotz der Komplexität konnte das Problem für $m$ bis zu 500 erfolgreich gelöst werden.
• Vergleich:
  • Die Triplication-Methode ist deutlich effizienter als die direkte Suche nach einem starken Starter der Ordnung $3p$mit einem SAT-Solver. (Beispiel:$n=39$direkt vs. Triplication von$p=13$: < 1 Sekunde vs. ~200 Sekunden).
  • Sie ist jedoch langsamer als der Hill-Climbing-Algorithmus von Dinitz und Stinson zur Generierung von Startern.
• Statistische Beobachtungen:
  • Nur ein sehr kleiner Prozentsatz der zufällig generierten starken Starter der Ordnung $3p$(z.B. ~1,8$n=21$) konnte durch Triplication erzeugt werden. Dies deutet darauf hin, dass Triplication eine spezifische Teilmenge aller starken Starter abdeckt, aber nicht alle.

5. Bedeutung und Fazit

• Neuer konstruktiver Ansatz: Das Paper bietet den ersten allgemeinen algorithmischen Ansatz, um starke Starter für Ordnungen $3p$(mit$p$ teilerfremd zu 3) zu konstruieren, basierend auf Startern kleinerer Ordnung.
• Unterstützung der Horton-Vermutung: Da die Methode für viele getestete Fälle erfolgreich war, liefert sie starke empirische Evidenz für die Existenz starker Starter in diesen Ordnungen, auch wenn der allgemeine Beweis noch aussteht.
• Verbindung von Kombinatorik und SAT: Das Paper demonstriert erfolgreich, wie moderne SAT-Solver verwendet werden können, um komplexe kombinatorische Design-Probleme zu lösen, die durch eine geschickte Reduktion (Triplication) auf ein modulares Sudoku-Problem zurückgeführt werden.
• Zukunftsaussichten: Die Autoren planen, einen spezialisierten Algorithmus zu entwickeln, der das modulare Sudoku-Problem effizienter löst als der allgemeine SAT-Solver, um die Methode für noch größere Ordnungen skalierbar zu machen.

Zusammenfassend stellt die „Triplication" einen eleganten Brückenschlag zwischen der Theorie der Startern und der praktischen Anwendung von Constraint-Solving-Techniken dar, der die theoretische Lücke bei der Existenz starker Starter für durch 3 teilbare Ordnungen signifikant schließt.