MiniZinc and Answer Set Programming solvers for IcoSoKu and its strongly NP-complete generalization 3coSoKu (see the papers about it here and here), completed by a 3D visualisation/solver tool for IcoSoKu built with Three.js and clingo-wasm, that you can try online now. This repository also contains some scripts benchmarking the solvers and verifying that every instance of IcoSoKu can indeed be solved (see Experimental results).
IcoSoKu is a mechanical puzzle created in 2009 by Andrea Mainini and it works as follows:
The 20 tiles are shown below.
3coSoKu is the generalization of IcoSoKu where each instance is defined by:
To stay true to IcoSoKu, we impose the number of tiles to be equal to the number of faces. 3coSoKu is strongly NP-complete, you can read all the details in the papers that Agostino Dovier, my professor at the University of Udine, and I wrote.
To see IcoSoKu instances and to solve them using the ASP solver you can try and play around with the web application: no installation is required, thanks to Three.js and to clingo compiled to WebAssembly.
Otherwise, if you want to test the solvers, install MiniZinc and/or clingo, then download this repository.
$ git clone https://github.com/nrizzo/3coSoKu.git
$ cd 3coSoKu
The solvers, found in solvers/MiniZinc
and solvers/ASP
, are already configured to solve instances of IcoSoKu. On Linux/Unix systems you can use the script icosolve.sh
, found in both folders: the script accepts as input the twelve capacities specifying the yellow pegs, following the convention of the figure on the right (alphabetical order).
$ cd solvers/MiniZinc
$ ./icosolve.sh 1 2 3 4 5 6 7 8 9 10 11 12
Alternatively, you can modify the array cap
in file input-ico.dzn
and facts cap(V,C)
in input-ico.lp
, respectively, also following the convention of the figure on the right, and manually execute the solvers:
$ minizinc --solver chuffed 3coSoKu.mzn input-ico.dzn
for MiniZinc (you can also use the IDE), and
$ clingo 3coSoKu.lp variants/ico.lp input-ico.lp
for ASP.
Folder tests
contains the Bash scripts to perform some interesting tests, also described in the papers. Details and results are described in here. In particular: the solvers make it possible to solve every IcoSoKu instance, thanks to the symmetries of the game; there are billions of different solutions for each IcoSoKu instance, so a good real-life strategy for the game is to do frequent restarts and try to "get lucky".
We developed a 3D application visualising IcoSoKu instances and its solutions using three.js
, Tweakpane
, and stats.js
. Moreover, the application uses clingo-wasm
to actually solve (in-browser!) the IcoSoKu instance specified by the user, thanks to clingo compiled to WebAssembly and our ASP encoding.
You can try here the web application using any modern browser, or you can launch it locally in two ways:
you can host the folder webapp/http
on your local network with any HTTP server;
$ cd webapp/http
$ python3 -m http.server &
$ firefox localhost:8000
you can run the offline version of the application found in webapp/offline
without doing any hosting by opening the main html file.
$ firefox webapp/offline/index.html
The offline version in webapp/offline
does not trigger the browser's CORS rules and it was obtained with some tricks, among which compiling clingo to JavaScript instead of WebAssembly using empscripten
's options -s WASM=0 --memory-init-file 0
(resulting in poorer clingo performance).
All of my code (the solver, the scripts and the webapp) is licensed under the terms of the GNU GPL v3 license, whereas the software and assets I am using (located in webapp/{http,offline}/vendor
and in webapp/{http,offline}/assets
), that is Clingo WebAssembly, three.js, Tweakpane, and stats.js, keep their original license. My images (in the images
folder) are instead licensed under CC BY.
Many thanks to my professor Agostino Dovier for the proposal of this problem and for writing the paper with me, to Marzio De Biasi for his kind words, to the organizers of CILC 2020, to their reviewers and to its attendees.