3coSoKu

3coSoKu

MiniZinc und Answer Set Programmierlöser für IcoSoKu und seine stark NP-vollständige Verallgemeinerung 3coSoKu (siehe die Artikel dazu hier und hier), ergänzt durch ein 3D-Visualisierungs-/Lösertool für IcoSoKu, das mit Three.js und clingo-wasm erstellt wurde, das können Sie Probieren Sie es jetzt online aus. Dieses Repository enthält auch einige Skripte, die die Solver vergleichen und überprüfen, ob jede Instanz von IcoSoKu tatsächlich gelöst werden kann (siehe Experimentelle Ergebnisse ).

Das Problem

IcoSoKu ist ein mechanisches Puzzle, das 2009 von Andrea Mainini entwickelt wurde und wie folgt funktioniert:

1. Das Spiel wird aufgebaut, indem die 12 gelben Stifte (die Zahlen von 1 bis 12) willkürlich auf den Eckpunkten platziert werden.
2. Das Spiel wird gespielt, indem die 20 dreieckigen Spielsteine, die dem Spiel beiliegen, auf den Flächen des Ikosaeders so angeordnet werden, dass die Anzahl der schwarzen Punkte, die jeden Scheitelpunkt umgeben, der Anzahl auf dem gelben Stift entspricht.

Die 20 Kacheln werden unten angezeigt.

3coSoKu ist die Verallgemeinerung von IcoSoKu, wobei jede Instanz definiert ist durch:

• das Spielfeld , ein Polyeder mit dreieckigen Flächen (das Ikosaeder, für IcoSoKu);
• die Kapazität jedes Scheitelpunkts, eine nicht negative ganze Zahl (die Anordnung der gelben Stifte);
• die Kacheln , bestehend aus drei nicht negativen ganzzahligen Gewichten (die Kacheln mit ihren Punkten).

Um IcoSoKu treu zu bleiben, legen wir fest, dass die Anzahl der Kacheln der Anzahl der Flächen entspricht. 3coSoKu ist stark NP-vollständig, Sie können alle Details in den Aufsätzen nachlesen, die Agostino Dovier, mein Professor an der Universität Udine, und ich geschrieben haben.

Erste Schritte

Um IcoSoKu-Instanzen anzuzeigen und sie mit dem ASP-Solver zu lösen, können Sie mit der Webanwendung herumspielen: Dank Three.js und dem zu WebAssembly kompilierten Clingo ist keine Installation erforderlich.

Andernfalls, wenn Sie die Solver testen möchten, installieren Sie MiniZinc und/oder Clingo und laden Sie dann dieses Repository herunter.

$ git clone https://github.com/nrizzo/3coSoKu.git
$ cd 3coSoKu

Die Solver in solvers/MiniZinc und solvers/ASP sind bereits für die Lösung von IcoSoKu-Instanzen konfiguriert. Auf Linux/Unix-Systemen können Sie das Skript icosolve.sh verwenden, das sich in beiden Ordnern befindet: Das Skript akzeptiert als Eingabe die zwölf Kapazitäten, die die gelben Stifte angeben, und folgt dabei der Konvention der Abbildung rechts (alphabetische Reihenfolge).

$ cd solvers/MiniZinc
$ ./icosolve.sh 1 2 3 4 5 6 7 8 9 10 11 12

Alternativ können Sie das Array cap in der Datei input-ico.dzn bzw. Facts cap(V,C) in input-ico.lp ändern, ebenfalls der Konvention der Abbildung rechts folgen, und die Löser manuell ausführen:

$ minizinc --solver chuffed 3coSoKu.mzn input-ico.dzn

für MiniZinc (Sie können auch die IDE verwenden) und

$ clingo 3coSoKu.lp variants/ico.lp input-ico.lp

für ASP.

Experimentelle Ergebnisse

Der Ordner tests enthält die Bash-Skripte zur Durchführung einiger interessanter Tests, die ebenfalls in den Artikeln beschrieben werden. Details und Ergebnisse werden hier beschrieben. Insbesondere: Die Solver ermöglichen es dank der Symmetrien des Spiels, jede IcoSoKu-Instanz zu lösen; Für jede IcoSoKu-Instanz gibt es Milliarden verschiedener Lösungen. Daher besteht eine gute Strategie für das Spiel im wirklichen Leben darin, häufige Neustarts durchzuführen und zu versuchen, „Glück zu haben“.

Das 3D-Visualisierungstool

Wir haben eine 3D-Anwendung entwickelt, die IcoSoKu-Instanzen und ihre Lösungen mithilfe von three.js , Tweakpane und stats.js visualisiert. Darüber hinaus verwendet die Anwendung clingo-wasm um die vom Benutzer angegebene IcoSoKu-Instanz tatsächlich (im Browser!) zu lösen, dank Clingo, das zu WebAssembly kompiliert wurde, und unserer ASP-Kodierung.

Sie können die Webanwendung hier mit einem beliebigen modernen Browser ausprobieren oder sie auf zwei Arten lokal starten:

• Sie können den Ordner webapp/http in Ihrem lokalen Netzwerk mit jedem HTTP-Server hosten;

    $ cd webapp/http
    $ python3 -m http.server &
    $ firefox localhost:8000
  

• Sie können die Offline-Version der Anwendung in webapp/offline ausführen, ohne ein Hosting durchführen zu müssen, indem Sie die Haupt-HTML-Datei öffnen.

    $ firefox webapp/offline/index.html
  

Die Offline-Version in webapp/offline löst nicht die CORS-Regeln des Browsers aus und wurde mit einigen Tricks erhalten, darunter das Kompilieren von Clingo zu JavaScript anstelle von WebAssembly mithilfe der empscripten -Optionen -s WASM=0 --memory-init-file 0 ( was zu einer schlechteren Clingo-Leistung führt).

Lizenz

Mein gesamter Code (der Solver, die Skripte und die Webapp) ist unter den Bedingungen der GNU GPL v3-Lizenz lizenziert, während die Software und Assets, die ich verwende (befindet sich in webapp/{http,offline}/vendor und in webapp/{http,offline}/assets ), also Clingo WebAssembly, three.js, Tweakpane und stats.js, behalten ihre ursprüngliche Lizenz. Meine Bilder (im images ) sind stattdessen unter CC BY lizenziert.

Danksagungen

Vielen Dank an meinen Professor Agostino Dovier für den Vorschlag dieser Aufgabe und dafür, dass er die Arbeit mit mir geschrieben hat, an Marzio De Biasi für seine freundlichen Worte, an die Organisatoren von CILC 2020, an ihre Gutachter und an seine Teilnehmer.