3coSoKu

3coSoKu

Solveurs MiniZinc et Answer Set Programming pour IcoSoKu et sa généralisation fortement NP-complète 3coSoKu (voir les articles à ce sujet ici et ici), complétés par un outil de visualisation/solveur 3D pour IcoSoKu construit avec Three.js et clingo-wasm, que vous pouvez essayez en ligne maintenant. Ce référentiel contient également des scripts évaluant les solveurs et vérifiant que chaque instance d'IcoSoKu peut effectivement être résolue (voir Résultats expérimentaux ).

Le problème

IcoSoKu est un puzzle mécanique créé en 2009 par Andrea Mainini et il fonctionne comme suit :

1. le jeu se déroule en plaçant les 12 piquets jaunes (les nombres de 1 à 12) arbitrairement sur les sommets ;
2. le jeu se joue en trouvant un arrangement des 20 tuiles triangulaires livrées avec le jeu sur les faces de l'icosaèdre, de telle sorte que le nombre de points noirs entourant chaque sommet soit égal à son numéro de piquet jaune.

Les 20 tuiles sont présentées ci-dessous.

3coSoKu est la généralisation d'IcoSoKu où chaque instance est définie par :

• le terrain de jeu , un polyèdre à faces triangulaires (l'icosaèdre, pour IcoSoKu) ;
• la capacité de chaque sommet, un entier non négatif (la disposition des piquets jaunes) ;
• les tuiles , constituées de trois poids entiers non négatifs (les tuiles avec leurs points).

Pour rester fidèle à IcoSoKu, nous imposons que le nombre de tuiles soit égal au nombre de faces. 3coSoKu est fortement NP-complet, vous pouvez lire tous les détails dans les articles qu'Agostino Dovier, mon professeur à l'Université d'Udine, et moi avons écrit.

Commencer

Pour voir les instances IcoSoKu et les résoudre à l'aide du solveur ASP, vous pouvez essayer de jouer avec l'application web : aucune installation n'est requise, grâce à Three.js et au clingo compilé en WebAssembly.

Sinon, si vous souhaitez tester les solveurs, installez MiniZinc et/ou clingo, puis téléchargez ce référentiel.

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

Les solveurs, trouvés dans solvers/MiniZinc et solvers/ASP , sont déjà configurés pour résoudre les instances d'IcoSoKu. Sur les systèmes Linux/Unix vous pouvez utiliser le script icosolve.sh , trouvé dans les deux dossiers : le script accepte en entrée les douze capacités spécifiant les piquets jaunes, en suivant la convention de la figure de droite (ordre alphabétique).

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

Alternativement, vous pouvez modifier respectivement le cap du tableau dans le fichier input-ico.dzn et cap(V,C) dans input-ico.lp , en suivant également la convention de la figure de droite, et exécuter manuellement les solveurs :

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

pour MiniZinc (vous pouvez également utiliser l'IDE), et

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

pour ASP.

Résultats expérimentaux

tests de dossiers contiennent les scripts Bash pour effectuer des tests intéressants, également décrits dans les articles. Les détails et les résultats sont décrits ici. En particulier : les solveurs permettent de résoudre chaque instance d'IcoSoKu, grâce aux symétries du jeu ; il existe des milliards de solutions différentes pour chaque instance d'IcoSoKu, donc une bonne stratégie réelle pour le jeu consiste à effectuer des redémarrages fréquents et à essayer de « avoir de la chance ».

L'outil de visualisation 3D

Nous avons développé une application 3D visualisant les instances IcoSoKu et ses solutions à l'aide de three.js , Tweakpane et stats.js . De plus, l'application utilise clingo-wasm pour résoudre réellement (dans le navigateur !) l'instance IcoSoKu spécifiée par l'utilisateur, grâce à clingo compilé sur WebAssembly et à notre encodage ASP.

Vous pouvez essayer ici l'application Web en utilisant n'importe quel navigateur moderne, ou vous pouvez la lancer localement de deux manières :

• vous pouvez héberger le dossier webapp/http sur votre réseau local avec n'importe quel serveur HTTP ;

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

• vous pouvez exécuter la version hors ligne de l'application trouvée dans webapp/offline sans effectuer d'hébergement en ouvrant le fichier html principal.

    $ firefox webapp/offline/index.html
  

La version hors ligne dans webapp/offline ne déclenche pas les règles CORS du navigateur et a été obtenue grâce à quelques astuces, parmi lesquelles la compilation de clingo en JavaScript au lieu de WebAssembly en utilisant les options de empscripten -s WASM=0 --memory-init-file 0 ( ce qui entraîne une moins bonne performance du clingo).

Licence

Tout mon code (le solveur, les scripts et la webapp) est sous licence selon les termes de la licence GNU GPL v3, tandis que les logiciels et les actifs que j'utilise (situés dans webapp/{http,offline}/vendor et dans webapp/{http,offline}/assets ), c'est-à-dire Clingo WebAssembly, three.js, Tweakpane et stats.js, conservent leur licence d'origine. Mes images (dans le dossier images ) sont sous licence CC BY.

Remerciements

Un grand merci à mon professeur Agostino Dovier pour la proposition de ce problème et pour avoir rédigé l'article avec moi, à Marzio De Biasi pour ses aimables paroles, aux organisateurs du CILC 2020, à leurs relecteurs et à ses participants.