Slitherlink

Slitherlink oder Suriza (japanisch スリザーリンク - surizā rinku) ist ein japanisches Puzzle. Es wurde erstmals 1989 vom Sudoku-Herausgeber Nikoli veröffentlicht. Es ist ein nachgewiesen NP-vollständiges Problem^[1].

Spielregeln

Das Spielfeld ist ein m x n Gittergraph. In den Zellen können Zahlen von 0 bis 3 stehen. Das Ziel ist es, benachbarte Knoten so zu verbinden, dass ein Zyklus entsteht. Dabei gilt es, die folgenden drei Regeln zu beachten:^[2]

1. Verbinde benachbarte Knoten mit horizontalen oder vertikalen Kanten, sodass genau ein Zyklus entsteht.
2. Die Zahlen geben an, wie viele Linien eine Zelle umgeben müssen. Leere Zellen können durch beliebig viele Linien umgeben werden.
3. Der Zyklus kreuzt sich nicht selbst nicht und es gibt keine Verzweigungen.

Gute Slitherlink-Puzzles haben eine eindeutige Lösung. In Abbildung 1^[3] ist ein kleines Slitherlink-Puzzle dargestellt.

Spielvarianten

Hexagonal Slitherlink^[4]

Es wird nach den selben Regeln gespielt, aber das Spielfeld besteht aus Hexagonen. Die Zahlen in den Zellen können entsprechend größer sein. In dem Beispiel aus Abbildung 2^[4:1] gibt es auch Zellen mit der Nummer 4 oder 5.

No-Square Slitherlink^[5]

Es gilt neben den Standardregeln noch die Zusatzregeln, dass es keinen 2x2 Bereich an Zellen innerhalb des Zyklus geben darf. Lösungen die zuvor bei Slitherlink möglich waren, können dadurch wie in Abbildung 3^[5:1] verboten werden.

Colorlink^[6]

Die Slitherlink-Regeln werden um die Folgenden ergänzt:

• Die Zahlen haben unterschiedliche Farben, z.B. rot und blau wie in Abbildung 4^[6:1]. Es soll für jede Farbe außer schwarz ein Zyklus nach Slitherlink-Regeln gefunden werden.
• Zahlen anderer Farben haben keinen Einfluss auf Zyklen anderer Farben.
• Zyklen unterschiedlicher Farben dürfen sich kreuzen.
• Linien dürfen jeweils von nur einer Farbe belegt werden.
• Schwarze Zahlen geben die Anzahl der umgebenden Linien unabhängig von der Farbe an.

Lösungsstrategien

Für gewöhnlich geht man so vor, dass man damit beginnt kleinere eindeutige Teillösungen zu bestimmen, um diese dann zu einem geschlossenen Kreis zu verbinden^[7]. Zudem ist es sinnvoll, Linien auszustreichen, die nicht Teil der Lösung sein können. In Abbildung 5^[2:1] ist die Progression beim Lösen von Slitherlink exemplarisch dargestellt.

Ausgewählte Linien stimmen mit Zellennummer überein

Für den Fall, dass die Anzahl ausgewählter Linien mit der Nummer einer Zelle übereinstimmt, können alle anliegenden und noch nicht gewählten Kanten ausgeschlossen werden. Dies ist bei Zellen mit der Nummer 0 wie in Abbildung 6^[8] leicht zu erkennen.

0 oder 2 angrenzende Linien an jedem Knotenpunkt

Die Erkenntnis, dass jeder Knoten nur 0 oder 2 angrenzende Linien hat, führt zu vielen verschiedenen Deduktionsstrategien, wie z.B. die Folgenden.

Zellen mit 3:

• 3 mit benachbarter 0: In diesem Fall können alle Linien um die 3 gewählt werden außer die an der 0 angrenzende. Außerdem kann die Teillösung um die 2 orthogonale Linien in beide Richtungen verlängert werden, denn an der 0 darf keine weitere Linie angrenzen und die beiden Enden dürfen nicht offen sein. In der Abbildung 7^[8:1] können drei Linien links, rechts und unten von der 3 gezogen werden und die Lösung kann um je eine Linie nach rechts und links erweitert werden. Zudem können für Knotenpunkte, die bereits 2 anliegende Linien haben, die anderen möglichen Linien ausgeschlossen werden.

• 3 mit diagonaler 0: Bei dieser Anordnung, müssen beide Linien, die an der Ecke zur 0 angrenzen, gewählt werden. Andernfalls wäre eines der beiden Enden der Teillösung an dem zu 0 angrenzenden Knotenpunkt und der Weg könnte nicht weitergeführt werden. Die grauen Linien in Abbildung 8^[8:2] zeigen die einzigen beiden Möglichkeiten, die Linien um die 3 zu ziehen.

• Zwei benachbarte 3en: Die Linie zwischen beiden Zellen muss ausgewählt werden. Andernfalls würde ein geschlossener Zyklus entstehen, der nicht mit weiteren Teilstücken verbunden werden kann. Außerdem können die dazu parellelen Linien ausgewählt werden. In Abbildung 9^[8:3] werden mit den grauen Linien die beiden Möglichkeiten, die Linien um diese Zellen herumzuziehen, dargestellt. Zudem wissen wir, dass die mittlere rot markierte Linie nicht gerade weitergeführt werden kann, da drei Seiten der Zelle abgedeckt werden müssen.

Diese Regel gilt nicht für triviale Slitherlink-Puzzles, welche durch einen einfachen Zyklus um zwei benachbarte 3-Zellen gelöst werden können, weil es keine anderen Zahlen gibt.^[9]

Zellen mit 1:

• Teillösung führt zur 1: Wenn die Linie an einer Zelle mit der Nummer 1 endet, muss man möglicherweise die Lösung um die 1 herum weiterführen. Dies könnte zum Beispiel aufgrund des Spielfeldrands in Abbildung 10 erforderlich sein. In solchen Fällen können wir die Linien, die nicht direkt am bestehenden Pfad liegen, ausschließen.

Spielfeldecken:

• 1 in einer Ecke: Die Linien zu den äußersten Eckpunkten können ausgeschlossen werden. Würde eine dieser Linien ausgewählt werden , könnte der Weg vom Eckpunkt aus nicht mehr weitergeführt werden, da bereits eine Linie an der Zelle anliegt.
• 2 in einer Ecke: Es müssen zwei Linien von der Ecke weg führen an der Spielfeldgrenze. Es gibt zwei mögliche Wege, die jeweils die in der Abbildung 11^[8:4] rot umkreisten Knoten verbinden. Um den Weg sinnvoll weiterzuführen sind diese beiden Linien an der Grenze notwendig.
• 3 in einer Ecke: In diesem Fall können die beiden äußeren Linien an der Spielfeldgrenze ausgewählt werden. Eine Auswahl von 3 Linien für diese Eckzelle ohne beide dieser Linien führt zu mindestens einem offenen Endpunkt, an dem nur eine Linie anliegt und keine weitere gewählt werden kann.

Lösungsansatz mithilfe von ZDDs

Basierend auf dem SIMPATH-Algorithmus zur Repräsentation von s-t Pfaden als ZDD haben Yoshinaka et. al.^[10] einen Solver für Instanzen von Slitherlink entworfen. Es soll ein ZDD generiert werden, welches alle Lösungen für eine gegebene Slitherlinkinstanz darstellt. Mit anderen Worten sollen alle Zellen entsprechend ihrer Zahl abgedeckt sein.

Definition Slitherlinkinstanz

Eine Instanz für Slitherlink ist ein Tupel aus einem Eingabegraphen G=(V,E) und einer partiellen Funktion h(E'): 2^E \rightharpoonup \mathbb{N}, wobei h(E')\leq |E'|. Für ein E' \subseteq E bedeutet h(E')=c dabei, dass genau c Kanten aus E' in der Lösung enthalten sein müssen. Eine Lösung für eine gegebene Instanz (G, h) ist ein Kreis C unter der Bedingung, dass für alle E' aus der Definitionsmenge von h h(E')= | C \cap E'| gilt.

Pseudocode (angepasst)

initialize mate;
initialize count;
create root labeled with first edge;
create 0-terminal, 1-terminal;
Q = new Queue;
Q.enqueue(root);
while Q not empty
		node = Q.enqueue;
    e = edge node is labeled with;
    if node has fixed end or is incompatible with h
    		create 0-arc from node to 0-terminal;
    else 
    		childnode = create new node;
        create 0-arc from node to childnode;
    if taking e forms a cycle matching h
    		create 1-arc from node to 1-terminal;
		else if taking e declines state of n or is incompatible with h
    		create 1-arc from node to 0-terminal;
		else 
    		childnode = create new node;
        create 0-arc from node to childnode    		

Arbeitsweise

Der Algorithmus iteriert ähnlich wie SIMPATH in einer Art Breitensuche über die Kanten. Auch hier müssen die Kanten zunächst in einer totalen Ordnung sein.

Es wird eine Funktion mate : V^{\geq e_i} \rightarrow V \cup \{0\} anstelle der mate-Tabelle verwendet, um den Zustand eines Knoten im ZDD zu speichern. V^{\geq e_i} bedeutet, dass die Funktion nur für Knoten aus Kanten definiert ist, die entsprechend der Kantenordnung größer oder gleich der aktuell betrachteten Kante e_i sind. Informationen über bereits untersuchte Kanten müssen also nicht gemerkt werden. Dabei gilt:

• mate(v) = v, falls v noch nicht betrachtet wurde.
• mate(v) = 0, falls v bereits zweimal besucht wurde.
• mate(v) = u, falls die Kante u-v gewählt wurde.

Neben der mate-Funktion gibt es eine Funktion count: \text{Dom}(h) \rightarrow \mathbb{N} für jeden Knoten des ZDDs. Diese Funktion zählt für alle E' \subseteq E in der Definitionsmenge von h, die Anzahl bereits abgedeckter Kanten. Am Anfang, wenn noch keine Kanten ausgewählt wurden, ist für alle E' count(E') = 0.

Intitial ist mate für alle v \in V definiert als mate(v)=v. Wie bei SIMPATH werden zu Beginn der Wurzelknoten und die Endknoten (0-terminal und 1-terminal) generiert und dann alle Kanten über die Queue iteriert. Für jeden Knoten, der neu generiert wird und in die Queue hinzugefügt wird, wird zusätzlich der Zustand mit mate und count gespeichert. Nachdem alle Kanten untersucht wurden, werden die Lösungen durch den 1-terminal Knoten repräsentiert, d.h. alle gültigen Pfade zu 1-terminal repräsentieren eine Lösung für die Slitherlinkinstanz.

mate updaten:
Nach Wahl einer Kante j-m (1-arc) wird mate wie folgt angepasst:

1. j^* = mate(j)
2. m^* = mate(m)
3. mate(j)=0
4. mate(m)=0
5. mate(j^*) = m^*
6. mate(m^*)= j^*

Außerdem wird der Definitionsbereich von mate so angepasst, dass nur noch Knoten aus V^{\geq e_{i+1}} betrachtet werden. Also nur noch Knoten größer oder gleich der nächsten zu untersuchenden Kante e_{i+1}. Dies gilt unabhängig davon, ob die Kante gewählt wird oder nicht (0-arc und 1-arc).

count updaten:
Nach Wahl einer Kante j-m (1-arc), wird der Zähler für jedes E' \in \text{Dom}(h) um 1 erhöht, wenn j-m \in E'.

Definitionen:
Es gibt einen festen Endpunkt für eine Kante j-m, wenn mate(v) \neq 0 und mate(v) \neq v für ein v \in \{ j, m\} \setminus V^{\geq e_{i+1}}.

Der Zustand eines Knoten ist inkompatibel mit h, falls es ein E' \in \text{Dom}(h) gibt, sodass count(E')>h(E') oder count(E') + |E' \cap E^{\geq e_{i+1}}| < h(E'), wobei E^{\geq e_{i+1}} alle Kanten meint, die gemäß Ordnung größer als die aktuelle Kante e_i sind. Der Zustand ist also inkompatibel, wenn entweder eine Zelle "überabgedeckt" ist oder mit den noch zu untersuchenden Kanten nicht mehr alle Zellen abgedeckt werden können.

Das Auswählen einer Kante e_i erzeugt einen Kreis, wenn für alle v \in \text{Dom}(mate) mate(v)=u falls e_i=\{u,v\} und mate(v)=v oder mate(v)=0 falls v \notin e_i.

Das Auswählen einer Kante erfüllt h, wenn alle Zellen genau abgedeckt sind (count = h).

Das Auswählen einer Kante j-m wird abgelehnt, wenn mate(j)=0, mate(m)=0, mate(m)=j oder mate(j)=m.

Folgezustände erkennen:
Innerhalb der while-Schleife (Z. 8-21 im Pseudocode) werden verschiedene Bedingungen geprüft, um den passenden Folgeknoten im ZDD für den 0-arc bzw. 1-arc zu finden.

Fall 1: Die aktuelle Kante soll nicht ausgewählt werden (0-arc).

• Falls es einen festen Endpunkt oder einen inkompatiblen Zustand mit h gibt, kann die Kante nicht ausgewählt werden, d.h. es gibt ein 0-arc zu 0-terminal.
• Sonst wird ein neuer Knoten im ZDD generiert, der über ein 0-arc verbunden wird.

Fall 2: Die aktuelle Kante soll ausgewählt werden (1-arc).

• Falls das Auswählen der Kante einen Kreis, der h erfüllt, erzeugt, wurde eine Lösung gefunden, d.h. 1-arc zu 1-terminal.
• Falls das Auswählen zu einem festen Endpunkt führt, es abgelehnt wird oder es zu einem mit h inkompatiblen Zustand führt, kann die Kante nicht ausgewählt werden, d.h. 1-arc zu 0-terminal.
• Sonst wird ein neuer Knoten im ZDD generiert, der über ein 1-arc verbunden wird.

Beispiele:
Das einfache Beispiel in Abbildung 12 wird betrachtet und verschiedene Zustände, die bei der Anwendung des Algorithmus auftreten werden, werden untersucht. Die Kantenordnung wird entsprechend der angegebenen Knotennummerierung betrachtet, z.B. 1-2 \leq 1-3. Seien mate' und count' die Belegung der Funktionen nach der Auswahl einer Kante (1-arc). Für dieses Beispiel gibt es 4 verschiedene Beschränkungen für die umliegenden Linien der Zellen. Sei h wie folgt definiert:

• h(E_1=\{1-2,1-3,2-5,3-5\}) = 2
• h(E_2=\{2-4,2-5,4-7,5-7\}) = 2
• h(E_3=\{3-5,3-6,5-8,6-8\}) = 2
• h(E_4=\{5-7,5-8,7-9,8-9\}) = 2

1. Aktuelle Kante 2-5, nachdem 1-2, 1-3 und 2-4 nicht gewählt wurden (Abbildung 13).

Der Zustand des Knoten ist inkompatibel mit h. Für E_1 \subseteq E ist count(E_1)=0. Die nächste zu untersuchende Kante wäre 3-5, d.h. count(E_1) + |E_1 \cap E^{\geq 3-5}|= 0 + 1 = 1 < h(E_1). Falls auch die Kante 2-5 nicht genommen wird, gibt es nur noch eine Kante, um count(E_1)=2 zu erreichen, aber zwei wären notwendig. Nicht-Wahl der Kante führt also zur Unlösbarkeit, der 0-arc führt zu 0-terminal.

Allerdings führt das Auswählen von 2-5 auch zur Unlösbarkeit. 2-5 ist die letzte Kante über den Knoten 2 des Eingabegraphen. Um einen Kreis zu erzeugen, wird jedoch eine weitere Kante mit 2 als Endpunkt benötigt. Die nächste Kante gemäß Kantenordnung wäre 3-5, d.h. für 2 \in \{2,5\} \setminus V^{\geq 3-5} ist mate'(2) = 5. Es gibt einen festen Endpunkt, also führt auch der 1-arc zu 0-terminal.

2. Aktuelle Kante 2-5, nachdem 1-2, 1-3 und 2-4 gewählt wurden (Abbildung 14).

Das Auswählen von 2-5 wird abgelehnt, denn mate(2)=0. Der Knoten 2 des Eingabegraphen wurde bereits zweimal besucht, ein drittes Mal ist verboten. Der 1-arc führt also zu 0-terminal. Die Nicht-Wahl (0-arc) von 2-5 ist hingegen in diesem Fall möglich und ein neuer Knoten im ZDD wird generiert.

3. Aktuelle Kante 8-9, nachdem 1-2, 1-3, 2-4, 3-6, 4-7, 6-8 und 7-9 gewählt wurden (Abbildung 15).

Die Wahl von 8-9 erzeugt einen Kreis, denn mate(8)=9, mate(9)=8, mate(5)=5 und mate(v)=0 sonst. Außerdem ist count'=h für E_1, E_2, E_3 und E_4, h wird also erfüllt. Es wurde eine Lösung für die Slitherlinkinstanz gefunden, es führt ein 1-arc zu 1-terminal.

Bei einen guten Slitherlink-Puzzle mit nur einer Lösung, kann der Algorithmus bei dem ersten h-erfüllenden gefundenen Kreis abgebrochen werden.

Vergleich mit anderen Solvern

Die Autoren haben ihren Algorithmus für verschiedene Instanzen mit dem SAT-Solver Sugar und dem Integer Programming Solver CPLEX verglichen. Im Ergebnis schlägt der ZDD-Algorithmus für viele Instanzen Sugar. Es gibt auch Beispiele, bei denen Sugar zeiteffizienter war. CPLEX ist in manchen Fällen schneller. Die Instanzen wurden auch mit einem heuristische Solver slink getestet. Dieser war für alle Instanzen deutlich schneller. Laut den Autoren seien diese Ergebnisse damit zu erklären, dass Sugar und CPLEX eher für allgemeinere Zwecke entwickelt wurden, während slink speziell für Slitherlink designt wurde und die ZDD-Lösung eher dazwischen liegt.

Laufzeit angegeben in Sekunden für das Lösen von Slitherlink. Für C95 konnte der ZDD-Solver keine Lösung finden aufgrund nicht ausreichenden Speichers.

Lösungsansatz mit SMT-Solver

Eine Lösungsmöglichkeit ist der Constrained-Based Ansatz dabei generiert man aus einem gegebenen Spielfeld eine aussagenlogische Formel und sucht eine Lösung mithilfe von bekannten SAT oder SMT Solvern. Miyauchi und Tanaka^[11] haben eine SMT-Lösung entwickelt, die für einige Fälle bessere Ergebnisse als vorherige Slitherlink-Solver erreichen konnte.

Referenzen