3coSoKu and its Logic Programming Modeling ? Nicola Rizzo and Agostino Dovier DMIF, University of Udine, Italy Abstract. In this paper we analyze the physical puzzle IcoSoKu and we propose its generalization called 3coSoKu. We prove the NP-completeness of the latter. Then we encode it both in the constraint programming language MiniZinc and in the logic programming paradigm of Answer Set Programming. We use our encodings to experimentally prove the conjecture that every initial state for IcoSoKu admits a solution. Keywords: IcoSoKu · 3coSoKu · NP-completeness · MiniZinc · ASP. 1 Introduction IcoSoKu, shown in Figure 1, is a mechanical puzzle created by Andrea Mainini in 2009. The IcoSoku problem is presented in detail in Section 2. Since it admits A B C D E F H G I K J L Fig. 1. IcoSoKu: a plastic blue icosahedron, 12 yellow numbered pegs, and 20 triangular tiles (left), and a possible naming of icosahedron vertices (right). only a finite number of different initial states, from the point of view of decidabil- ity/complexity it is a finite game (and, hence, trivial). In this paper we present a ? Copyright c 2020 for this paper by its authors. Use permitted under Creative Com- mons License Attribution 4.0 International (CC BY 4.0). generalization of the problem that admits an infinite number of different initial states, called 3coSoKu, and we prove its NP-completeness in Section 3. We then model the 3coSoKu problem (and, as a side effect, IcoSoKu) using the constraint modeling language MiniZinc [13] (Section 4) and Answer Set Pro- gramming [3] (Section 5). The two chosen paradigms are the standard de facto for constraint programming (thanks to the MiniZinc challenge organized since 2008 [12]) and for solving combinatorial problems in logic programming (thanks to the ASP competition organized since 2007 [4]). In Section 6 we compare ex- perimentally the two declarative approaches, along the lines of the empirical study conducted in [1]. Moreover, we use them in solving all possible instances of IcoSoKu, proving the conjecture that claims it to be possible. Some conclu- sions are drawn in Section 7. All the code and scripts used and described in the paper are available from http://clp.dimi.uniud.it/sw/. 2 The Problem The IcoSoKu puzzle consists of (i) a plastic blue icosahedron, (ii) 12 yellow pegs with the numbers from 1 to 12 written on their tips, and (iii) 20 equilateral triangular tiles with from 0 up to 3 black dots near each vertex. The game is set up by placing all the pegs on the vertices of the icosahedron in an arbitrary way; the goal is to place all the tiles on the faces of the solid in a way such that the number of black dots surrounding each vertex is equal to the number P12 of its peg. All the pieces of the puzzle must be used. Globally, there are i=1 i = 78 black dots (see Figure 2). Each triangle can be rotated (for the sake of completeness we add that it cannot be flipped: the other face is not colored by dots). In [6,10] it is claimed that every setup of the pegs can be solved, but a proof of this conjecture is not given. ×1 ×1 ×1 ×1 ×1 ×3 ×3 ×1 ×1 ×1 ×2 ×2 ×1 ×1 Fig. 2. The set of twenty tiles for IcoSoKu. We can represent each triangle of Figure 2 with a triple of numbers, read in clockwise order written in non-decreasing lexicographical ordering: (0, 0, 0), (0, 0, 1), (0, 0, 2), (0, 0, 3), (0, 1, 1), . . . , (1, 2, 3), (1, 3, 2), (2, 2, 2), (3, 3, 3). In the process of modeling this problem, each tile is assigned to an integer number in {1, . . . , 20}. The possible rotations are encoded as 0 (0◦ ), 1 (120◦ ), and 2 (240◦ ). Let us observe that the set does not include all the triples in {0, . . . , 3}3 (e.g., (1, 3, 3), (2, 3, 3), . . . ). Moreover, we assign the letters from A to L to the vertices of the icosahedron, as seen in Figure 1 (right), and we refer to the faces using the three vertices that they involve in clockwise order. Thus the 20 faces are ABC, ACD, ADE, AEF, . . . , HLI, ILJ, JLK. Given a face f = v0 v1 v2 , we use πi (f ) to indicate its (i + 1)-th element, with i = 0, 1, 2, that is πi (f ) = vi . This is sufficient to describe the placement of a tile. For instance, assigning tile (0, 1, 2) to face ABC with rotation 1 means to rotate the tile by 120◦ , obtaining tile (2, 0, 1), and to place 2 black dots on the corner corresponding to vertex A, 0 dots on vertex B and 1 dot on vertex C. 2.1 Related work An interesting benchmark for estimating the performance in solving instances of IcoSoKu is De Biasi’s JavaScript online solver [5], implementing a backtrack- ing algorithm that fills the faces of the icosahedron with the tiles, following a heuristic and deterministic search of the solution that prioritizes the most filled vertices. An experimental analysis of running times is given in Section 6. IcoSoKu as a constraint programming problem has been recently studied by Liu et al. [9]: they observe that there are 24 different triangular tiles obtain- able using i ∈ {0, 1, 2, 3} black dots, after accounting for rotations, whereas the tile distribution of IcoSoKu uses only 14 types of tiles (this leaves room for a generalization). The authors then proceed to pose some questions inspired by IcoSoKu but characterized by the use of pairwise distinct tiles (again, accounting for rotations), instead of the distribution the game ships with: using constraint programming, and in particular using the alldifferent and table constraints, they verify that each instance of IcoSoKu can be solved using the 24 possible tiles, having each time 4 unused tiles. In the process, they avoid checking all possible instances using symmetry breaking constraints that we also use in Section 6.2. 3 Generalizing IcoSoKu to 3coSoKu A variant of IcoSoKu can be stated for every polyhedron with regular faces, or faces of the same size and shape. All five Platonic solids (Figure 3) fit into this category, but infinite more polyhedra can be the gaming field, defining the vertices and their connections. We focus on all polyhedra with triangular faces. In this way, we generalize IcoSoKu by posing the constraint satisfaction problem we call 3coSoKu and that we prove to be NP-complete. We try to stay close to the original problem by imposing that each tile must be used only once and that there must be as many tiles as there are faces. Temporarily, we overlook the practical constraint of having the faces and the tiles of the same size and shape: this is addressed at the end of the Section. A B C D Fig. 3. The other Platonic solids can be the playing field of the game. If P is a polyhedron with triangular faces, we refer to VP as the set of the vertices of P and FP as the set of the triples of vertices describing the faces of P (FP ⊆ VP3 ). Given v ∈ VP , we also denote by FPv ⊆ FP the set of faces containing the vertex v. For example, the tetrahedron T in Figure 3 (left) is described by VT = {A, B, C, D} and FT = {ABC, ACD, ADB, BDC}, with FTA = {ABC, ACD, ADB}. The setup for a game of 3coSoKu consists of the polyhedron, the capacities assigned to the vertices (the numbers on the yellow pegs of IcoSoKu) and the tiles containing triples of weights (number of black dots). Definition 1 (3coSoKu instance). Let P be a polyhedron with triangular faces. An instance of 3coSoKu is a tuple P, c, T where – c : VP → N is a (capacity) map that assigns each vertex to an integer and – T = {|t1 , . . . , tn |} is a multiset of tiles, where each element ti ∈ N3 is a triple of weights and n = |FP |.  With T in Figure 3 (left), an instance of 3coSoKu is T , c, T where: c(A) = 1, c(B) = 2, c(C) = 3, c(D) = 4 and T = {|(0, 0, 1), (0, 0, 2), (0, 0, 3), (1, 1, 2)|} .  Definition 2 (3coSoKu problem). Given an instance P, c, T of 3coSoKu, an arrangement of the tiles in T to the faces of P is a pair (ρ, σ) such that: – ρ : T → {0, 1, 2} defines the rotation of each tile and – σ : T → FP is a bijection assigning tiles to faces.  An arrangement (ρ, σ) is a solution of P, c, T if X πi (t) = c(v) ∀v ∈ VP . (1) t∈T, i∈{0,1,2}: π(i+ρ(t)) mod 3 (σ(t))=v  The 3coSoKu problem is the problem of finding a solution of P, c, T . For each vertex v, equation (1) takes all the weights that end up near v after the rotation and placement of the tiles, using the modulo operation, and constraints their sum to be equal to the capacity of v. We can reformulate (1) into a handier equation that directly involves FPv instead of the tiles that are placed there (the latter is defined by the input while the former depends on the arrangement considered): let τ = σ −1 ; then the constraints for the 3coSoKu problem are equivalent to X  π(i−ρ(τ (f ))) mod 3 τ (f ) = c(v) ∀v ∈ VP . (2) f ∈FP , i∈{0,1,2}: πi (f )=v Note how the rotation must be applied backwards in order to get the weight placed on the i-th vertex of face f , whereas in (1) the rotation is applied forward in order to find where the weights are placed. For example, if the polyhedron P is the tetrahedron T in Figure 3 (left), then the constraints defined by (2) become   π(−ρ(τ (ABC))) mod 3 τ (ABC) + π(−ρ(τ (ACD))) mod 3 τ (ACD) +  π(−ρ(τ (ADB))) mod 3 τ (ADB) = c(A) π(1−ρ(τ (ABC))) mod 3 τ (ABC) + π(2−ρ(τ (ADB))) mod 3 τ (ADB) +  π(−ρ(τ (BDC))) mod 3 τ (BDC) = c(B) π(2−ρ(τ (ABC))) mod 3 τ (ABC) + π(1−ρ(τ (ACD))) mod 3 τ (ACD) +  π(2−ρ(τ (BDC))) mod 3 τ (BDC) = c(C) π(2−ρ(τ (ACD))) mod 3 τ (ACD) + π(1−ρ(τ (ADB))) mod 3 τ (ADB) + π(1−ρ(τ (BDC))) mod 3 τ (BDC) = c(D) since the couples f ∈ FT , i ∈ {0, 1, 2} such that πi (f ) = A are (ABC, 0), (ACD, 0) and (ADB, 0), the couples such that πi (f ) = B are (ABC, 1), (ADB, 2) and (BDC, 0), the couples such that πi (f ) = C are (ABC, 2), (ACD, 1) and (BDC, 2), and the couples such that πi (f ) = D are (ACD, 2), (ADB, 1) and (BDC, 1). 3.1 NP-completeness We study the complexity of 3coSoKu, proving that it is NP-complete. NP mem- bership is immediate: given an instance of 3coSoKu and an arrangement of its tiles to its faces, checking if the arrangement satisfies constraint (2) requires O(n) arithmetic operations. To prove NP-hardness we will reduce one of Karp’s original 21 NP-complete problems, the partition problem, (see [8, p. 97] and [2, pp. 60-61, 223]): Input: A finite set A and an assignment s(a) ∈ Z+ for each a ∈ A. Problem: Establish whether there is a subset B ⊆ A such that X X s(a) = s(a). a∈B a∈A\B Theorem 1. 3coSoKu is NP-complete. Proof. We already established that 3coSoKu is in NP. To prove its NP-hardness we reduce Partition to 3coSoKu showing how to transform its generic instance A = {a1, . . . , an } with s(ai ) = si for i ∈ {1, . . . , n} into an instance of 3coSoKu P, c, T , that we now describe, such that the latter admits a solution if and only if the former has a solution: 1. P is a bipyramid with 2n faces composed by merging two n-gonal pyramids base to base, such that the two apices correspond to sets B and A \ B of a possible solution and the other 2n − 2 vertices are dummy vertices, as seen in Figure 4 (left); P n 2. c assigns capacity i=1 si /2 to apices B and A \ B and capacity 0 to all other vertices; 3. T is a multiset of 2n tiles made of n empty tiles (0, 0, 0) and tiles (si , 0, 0) for i ∈ {1, . . . , n}, as seen in Figure 4 (right). B s1 ×1 .. ×n Z3 Z2 Z1 Z2n−3 . Z2n−2 sn ×1 A\B Fig. 4. The corresponding instance (P, c, T ) of 3coSoKu is such that P a bipyramid with 2n faces (left) and T has n empty tiles and tiles (si , 0, 0) for i ∈ {1, . . . n} (right). It is easy to see that the Partition instance admits a solution B corresponding to sizes q1 , . . . , qk , with k ∈ {1, . . . , n − 1} if and only if there is an arrangement (ρ, σ) that satisfies Equations (2), placing all the weights corresponding to sizes q1 , . . . , qk near vertex B, placing the rest of the positive weights near A \ B and arbitrarily placing all remaining (0, 0, 0) tiles. The n tiles of cost zero are needed to compensate the difference of cardinality Pn between  B and A \ B. The reduction can clearly be carried on in O log( i=1 log si ) space. t u We can now discuss more deeply the definition of 3coSoKu, because it does not specify polyhedron P to be well-founded and constructible in three-dimensional space, especially so with equilateral triangles as faces. Some considerations: – each instance defines linear constraints that are well defined even if P is not; – in the reduction, the rotation of the tiles is not exploited; – the constructed bypiramid is always a well defined polyhedron with faces of the same size and shape; – Theorem 1 implicitly proves that the subset of instances characterized by strictly-convex triangular polyhedra (the bipyramid constructed has this fea- tures) is sufficient to make it NP-complete. For these reasons, imposing constraints over the points above does not change the complexity of the problem. This reasoning leaves out general deltahedra, i.e. polyhedra with equal regular triangles as faces, to suffice for NP-completeness, since the only ones that are bipyramids are the triangular bipyramid, the octa- hedron and the pentagonal bipyramid [7]. So the NP-completeness of 3coSoKu restricted to deltahedra remains an open problem. 4 The MiniZinc Encoding In this section we present the MiniZinc encoding of 3coSoKu. First, we need to define its instance (P, c, T ). The model of P (see Listing 1.1) consists of: – the integers m and n, the number of vertices and faces of P; – two sets VERTEX and FACE that contain the vertices and faces of P; – a matrix vrtx with n rows, one for each face of P, and 3 columns such that vrtx[f,j], j ∈ {0, 1, 2} are the vertices of face f in clockwise order. The capacities c and the tiles T are modeled by array cap and matrix weight (see for instance Listing 1.2). The solution (ρ, σ) is modeled by array tile, that int : m = 12; int : n = 20; enum VERTEX = {A , B , C , D , E , F , G , H , I , J , K , L }; enum FACE = { ABC , ACD , ADE , AEF , AFB , BFK , BKG , BGC ,CGH , CHD , DIE , DHI , EIJ , EJF , FJK ,GKL , GLH , HLI , ILJ , JLK }; array [ FACE , 0..2] of VERTEX : vrtx = array2d ( FACE , 0..2 , [A , B , C , A, C, D, A, D, E, ... H, L, I, I, L, J, J , L , K ]) ; array [ FACE ] of var 1.. n : tile ; array [ FACE ] of var 0..2: rot ; Listing 1.1. Setting the icosahedron as playing field of the MiniZinc model. assigns each face to a tile, and rot, that assigns each face to the rotation (0, 1, or 2) of the tile placed on it, as shown at the end of Listing 1.1. tile models array [ VERTEX ] of int : cap = [1 ,11 ,5 ,10 ,6 ,7 ,9 ,2 ,3 ,8 ,4 ,12]; array [1.. n , 0..2] of int : weight = array2d (1.. n , 0..2 , [0 ,0 ,0 , 0 ,0 ,1 , 0 ,0 ,2 , 0 ,0 ,3 , 0 ,1 ,1 , 0 ,1 ,2 , 0 ,1 ,2 , 0 ,1 ,2 , 0 ,2 ,1 , 0 ,2 ,1 , 0 ,2 ,1 , 0 ,2 ,2 , 0 ,3 ,3 , 1 ,1 ,1 , 1 ,2 ,3 , 1 ,2 ,3 , 3 ,2 ,1 , 3 ,2 ,1 , 2 ,2 ,2 , 3 ,3 ,3]) ; Listing 1.2. Instance of IcoSoKu for the MiniZinc model. function var int : vertex_sum ( VERTEX : v ) = sum ( f in FACE , r in 0..2 where vrtx [f , r ] == v ) ( weight [ tile [ f ] , [1 ,2 ,0 ,1 ,2][3 + r - rot [ f ]]]) ; % equivalent to (3 + r - rot [ f ]) mod 3 constraint alldifferent ( tile ) ; constraint forall ( v in VERTEX ) ( vertex_sum ( v ) == cap [ v ]) ; Listing 1.3. Constraints of the MiniZinc model. Put tile (0 , 2 , 1) on face corresponding to pegs 1 , 11 , 5 ( face ABC ) . Put tile (0 , 0 , 2) on face corresponding to pegs 1 , 5 , 10 ( face ACD ) . Put tile (1 , 2 , 0) on face corresponding to pegs 1 , 10 , 6 ( face ADE ) . ... Put tile (0 , 2 , 1) on face corresponding to pegs 2 , 12 , 3 ( face HLI ) . Put tile (1 , 3 , 2) on face corresponding to pegs 3 , 12 , 8 ( face ILJ ) . Put tile (1 , 3 , 2) on face corresponding to pegs 8 , 12 , 4 ( face JLK ) . ---------- Listing 1.4. Example output of the MiniZinc encoding for IcoSoKu. τ = σ −1 instead of σ, since during the development of the encoding we have heuristically observed that this implicitly defines a faster search strategy. For the solution to be correct, all the tiles must be assigned to different faces, which is guaranteed using the predicate alldifferent, and the weights assigned to each vertex must add up to its capacity. The constraints corresponding to Equation (2) are easily enforced using the matrix vrtx and the modulo operation, as in Listing 1.3.1 Symmetry breaking constraints that impose tiles of the form (x, x, x), with x ∈ {0, 1, 2, 3}, are not rotated and that impose a fixed order between duplicated tiles are also added (and are not shown in this paper). Finally, Listing 1.4 shows the output of the encoding for an instance of IcoSoKu, obtained using the post-processing functions we have written to give instructions to the solution. We will explore in the future other ways to visualize the solutions. 5 The ASP Encoding The input is similar to the input of the MiniZinc solver: the variant played consists of constants m and n, the vertices and faces of P given as input facts of predicates vertex/1 and face/1 and the projection of the vertices in their component is given in input extensionally with predicate vrtx/3 (see Listing 1.5); capacities and tiles are given by the predicate cap/2 and weight/3, such that c(v) = i corresponds to fact cap(v, i) and the i-th tile being (x, y, z) corresponds to facts weight(i, 0, x), weight(i, 1, y) and weight(i, 2, z). The encoding of an instance of IcoSoKu is shown in Listing 1.6. # const m = 12. # const n = 20. vertex ( a ; b ; c ; d ; e ; f ; g; h; i; j; k; l). face ( abc ; acd ; ade ; aef ; afb ; ... ; hli ; ilj ; jlk ) . vrtx (a , abc , 0; b , abc , 1; c , abc , 2; a , acd , 0; c , acd , 1; d , acd , 2; .... h , hli , 0; l , hli , 1; i , hli , 2; i , ilj , 0; l , ilj , 1; j , ilj , 2; j , jlk , 0; l , jlk , 1; k , jlk , 2) . Listing 1.5. Setting the icosahedron as playing field of the ASP model. The solution is modeled by functions assign/2 and rotate/2, that indicate respectively which tile to put on each face and the rotation of each tile. To constraint the solution to be correct (see Listing 1.7): 1 A reformulation without using the mod operator as suggested by a reviewer—that we would like to thank—proved to be an improvement on harder instances of IcoSoKu using Gecode’s standard search strategy. cap (a ,1; b ,11; c ,5; d ,10; ... ; j ,8; k ,4; l ,12) . weight (1 , 0 , 0; 1 , 1 , 0; 1 , 2 , 0; 2 , 0 , 0; 2 , 1 , 0; 2 , 2 , 1; 3 , 0 , 0; 3 , 1 , 0; 3 , 2 , 2; ... 18 , 0 , 3; 18 , 1 , 2; 18 , 2 , 1; 19 , 0 , 2; 19 , 1 , 2; 19 , 2 , 2; 20 , 0 , 3; 20 , 1 , 3; 20 , 2 , 3) . Listing 1.6. Instance of IcoSoKu for the ASP model. – we impose assign to be a bijection of the tiles to the faces; – we impose each tile to have one and only one rotation; – we use aggregate function #sum to discard all models in which the capacities of the vertices are not fulfilled exactly. tile (1.. n ) . rotation (0..2) . 1 { assign (T , F ) : face ( F ) } 1 : - tile ( T ) . 1 { assign (T , F ) : tile ( T ) } 1 : - face ( F ) . 1 { rotate (T , R ) : rotation ( R ) } 1 : - tile ( T ) . : - # sum { P , F : vrtx (V , F , A ) , assign (T , F ) , rotate (T , R ) , weight (T , ( A - R + 3) \ 3 , P ) } != C , cap (V , C ) . Listing 1.7. Rules to constraint the solution of the ASP model. Also in this case we add symmetry breaking constraints as in the MiniZinc encoding (not shown in this paper). For the output to be readable, an auxiliary predicate put/9 has been written: its values, to be read in groups of three, indicate the tile, the face where to put the tile and the corresponding capacities.2 An example of the output for IcoSoKu is shown in Listing 1.8. 6 Tests and Experiments We report on some tests on 3coSoKu, available in the code repository http: //clp.dimi.uniud.it/sw/, we have written in Bash. The comparative tests have been executed on a single-thread of an Intel Core i5-7400 @ 3.50 GHz running Arch Linux. The versions of the main tools we used are shown in Figure 5. 2 Predicate put/9 affects the grouding size, adding O(n2 ) statements: its removal must be considered when solving 3coSoKu instances with a high number of tiles and faces. clingo version 5.4.0 Reading from stdin Solving ... Answer : 1 cap (a ,1) cap (b ,11) cap (c ,5) cap (d ,10) cap (e ,6) cap (f ,7) cap (g ,9) cap (h ,2) cap (i ,3) cap (j ,8) cap (k ,4) cap (l ,12) put (0 ,3 ,0 , a ,b ,c ,1 ,11 ,5) put (0 ,1 ,2 , a ,c ,d ,1 ,5 ,10) put (0 ,1 ,2 , a ,d ,e ,1 ,10 ,6) ... put (0 ,2 ,0 , h ,l ,i ,2 ,12 ,3) put (0 ,2 ,2 , i ,l ,j ,3 ,12 ,8) put (3 ,2 ,1 , j ,l ,k ,8 ,12 ,4) SATISFIABLE Models : 1+ Calls : 1 Time : 0.102 s ( Solving : 0.04 s 1 st Model : 0.04 s Unsat : 0.00 s ) CPU Time : 0.100 s Listing 1.8. Example output of the ASP model for IcoSoKu. Software Description Version MiniZinc Distribution MiniZinc compiler and FlatZinc solvers 2.4.3 clingo Answer Set System 5.4.0 Node.js JavaScript run-time environment (v8 engine) 14.5.0 OpenSSL Algorithms for test generation 1.1.1g GNU parallel Shell tool to execute jobs in parallel 20200322 Fig. 5. Software used in testing. 6.1 Comparative performance tests for IcoSoKu To measure the performance of the solvers we have written a script that, starting from a seed, generates a batch of 100 instances of IcoSoKu and measures the performance of each solver on the whole batch. The generator uses openssl as shuf’s pseudo-random source. The solvers we compare are: for the MiniZinc encoding3 , Gecode and Chuffed; for the ASP encoding, the clingo ASP system; De Biasi’s JavaScript solver. We have not explored any optimization parameters of the models, but after some preliminary experiments we observed that the most successful search strategy of the Gecode solver for MiniZinc is a randomized search plus a restart after a low and constant number of nodes visited, implemented in Listing 1.9. The times reported have been gathered, respectively, from minizinc’s own “Overall time” in its statistics (option -s), from clingo’s “CPU Time” already available, and by parametrizing function icosolve of the JavaScript solver to accept the capacities in input (taking care of the difference in the naming con- vention for the vertices) and with two invocations of new Date(). 3 In the MiniZinc tests, for each instance of the batch the model is compiled to FlatZinc and is then fed into a solver. Looking at the different outputs of the first step, we have noted that the difference from instance to instance is only in the 12 FlatZinc instructions specifying the capacities (they involve constraint int_lin_eq). This means that the compilation to FlatZinc can be skipped by modifying the FlatZinc output of one instance. We have not exploited this trick to be fair to the other solvers. The results are shown in Figures 6 and 7, with the relative mean value drawn horizontally. The worst times are: – 15.14 seconds for the plain MiniZinc model using Gecode; – 0.45 seconds for the MiniZinc model using Gecode with the randomized search of Listing 1.9; – 0.23 seconds for the MiniZinc model using Chuffed; – 0.09 seconds for the ASP model; – 47.61 seconds for the JavaScript solver. The best model for IcoSoKu is the ASP one, but Chuffed and Gecode’s ran- domized search are valid alternatives. Gecode’s standard search is similar to the preexisting JavaScript solver, in the sense that in average it is faster but solving some instances takes a lot of time because the solvers explore a large subtree of the search space that has no solution. 6.2 Verifying IcoSoKu’s solvability We have challenged our encodings (and the constraint/ASP solvers used) to verify the conjecture that every possible instance of the commercial version of IcoSoKu admits a solution (i.e. fixing the icosahedron as playing field and using the set of tiles of Figure 2). The naive search space consisting of all the permu- tations of {1, . . . , 20} has been first pruned removing symmetric solutions: 1. W.l.o.g., we impose the capacity of vertex A to be equal to 1. 2. Once the capacity of vertex A is fixed, the icosahedron can still be rotated on its A–L vertical axis by any multiple of 72◦ . Thus, w.l.o.g. we can impose the capacity of vertex B to be less than those of vertices C, D, E, and F. This leaves for B any value in {2, . . . , 8}. 3. We can exploit one last symmetry, involving both the icosahedron and the tile configuration of IcoSoKu. By flipping the icosahedron horizontally with the plane of reflection that goes through A, L and B, as shown in Figure 8, we can obtain a mirrored icosahedron imposable over the original. For each instance defined by points 1. and 2. we can flip their capacities instead of the vertices, obtaining a different instance that still fits the two constraints, so we can split these instances into mutually symmetric pairs. Thus for each instance there is a symmetrical one and also for each solution there is a symmetrical one: in fact, by flipping the whole tile configuration of IcoSoKu we get the same tile configuration, because the tiles with three different numbers of black dots all have their symmetric counterpart (see Figure 2). This allows us to divide by two the number of possible inputs. Thus, with 7 possible capacities for vertex B and the whole set divided by two we have roughly 4M instances to check:   1 9! · 6! 8! · 6! 7! · 6! 6! · 6! 10! + + + + + 5! · 6! + 4! · 6! = 3 991 680 2 5! 4! 3! 2! solve :: int_search ( tile , first_fail , indomain_random ) :: restart_constant (100) satisfy ; Listing 1.9. Randomized search for the MiniZinc model. MiniZinc model (Gecode) 20 15 Time (s) 10 5 Mean: 0.85s 0 0 10 20 30 40 50 60 70 80 90 100 Index of the instance MiniZinc model (Gecode, randomized search + constant restart) 1 0.8 Time (s) 0.6 0.4 0.2 Mean: 0.16s 0 0 10 20 30 40 50 60 70 80 90 100 Index of the instance MiniZinc model (Chuffed) 1 0.8 Time (s) 0.6 0.4 0.2 Mean: 0.14s 0 0 10 20 30 40 50 60 70 80 90 100 Index of the instance Fig. 6. MiniZinc performance tests on instances of IcoSoKu. ASP model 1 0.8 Time (s) 0.6 0.4 0.2 Mean: 0.03s 0 0 10 20 30 40 50 60 70 80 90 100 Index of the instance JavaScript solver 40 Time (s) 20 Mean: 0.83s 0 0 10 20 30 40 50 60 70 80 90 100 Index of the instance Fig. 7. ASP (top) and JavaScript (bottom) performance test on instances of IcoSoKu. A A D E C E F D B F B C H I G K G J H J K I L L Fig. 8. The icosahedron (left) intersected with the plane through A, B and L (in red) and its mirrored version (right): this symmetry can be exploited with the symmetries of the tile configuration. We have written a small program to generate the corresponding instances and using GNU parallel [14] we have parallelized our ASP model4 : using four threads, in 15 hours, 57 minutes and 50 seconds all instances were checked, em- pirically verifying the claim of the author of the game. We also repeated the benchmark using parallel’s option --joblog to log the solving time of each in- stance. The process took five extra minutes, with 0.23 seconds the worst solving time and 0.05 seconds the average solving time. 98% of instances took less than 0.1 seconds and 61% of instances took less time than the average. During devel- opment, this test has also been executed successfully with our MiniZinc models, using Chuffed and using Gecode’s randomized search. 7 Conclusions We have defined 3coSoKu, a generalized version of IcoSoKu and show its NP- completeness, even when imposing that the playing field is well formed and that the faces are of the same size and shape. Some questions remain unanswered: is 3coSoKu still NP-complete if we impose the playing field to be a deltahedron, i.e. a polyhedron with equilater triangles as faces? Partition admits a pseudo- polynomial time algorithm (see [2, p. 223]); is it the case for 3coSoKu as well? From experimental testing on instances of IcoSoKu, the best approaches we have found to solve instances of IcoSoKu use our ASP model and our MiniZinc model with solver Chuffed: our interpretation is that the nogood learning of the former and the lazy clause generation of the latter is an effective tool to prune the search tree of 3coSoKu. Gecode’s randomized search plus constant restart is also valid, probably because there is a high number of solutions for each instance of IcoSoKu, and could inspire a practical strategy for the game. Counting the number of solutions with our solvers proved to be a difficult task because of the size of the search tree. Exploring approximately 2% of the search tree for the first instance of the batch of tests, we found more than 200 million different solutions (with symmetry breaking constraints). A profound combinatorial reason for the existance of a solution to every instance of IcoSoKu has not been found (not looked for, actually), but using our models and some symmetry breaking considerations, we managed to solve every possible instance in 16 hours with common hardware, proving the conjecture. References 1. Dovier A., Formisano A., Pontelli E.: An empirical study of constraint logic pro- gramming and answer set programming solutions of combinatorial problems. J. Exp. Theor. Artif. Intell. 21(2): 79-121 (2009) 2. Garey M. R., Johnson D. S.: Computers and Intractability, a Guide to the Theory of NP-Completeness. W. H. Freeman and Company (1979) 4 In order to shave off as much time as possible, we removed print predicate put/9 and suppressed the output of the solution entirely, relying on clingo’s output to know if there exists a solution or not. 3. Gebser M., Kaminski R., Kaufmann B., Lindauer M., Ostrowski M., Romero J., Schaub T., Thiele S., Wanko P.: Potassco User Guide. 2nd edn, version 2.2.0. University of Potsdam (2019) 4. Gebser M, et al.: The First Answer Set Programming System Competition. Proc of LPNMR, LNCS 4483, pp 3–17 (2007) 5. IcoSoKu online solver page, http://www.nearly42.org/games/icosoku-solver/. Last accessed 30 March 2020 6. IcoSoKu puzzle product page, https://www.recenttoys.com/ recent-toys-icosoku-puzzle/. Last accessed 30 March 2020 7. Johnson N.: Convex Polyhedra with Regular Faces. Canadian Journal of Mathe- matics, 18, 169–200 (1966). https://doi.org/10.4153/CJM-1966-021-8 8. Karp R. M.: Reducibility among Combinatorial Problems. In: Complexity of com- puter computations, pp. 85–103. Springer, Boston, MA (1972) 9. Liu K., Löffler S., and Hofstedt, P.: Exploring Properties of Icosoku by Constraint Satisfaction Approach, in post proc of Declarative Programming and Knowledge Management - Conference on Declarative Programming, DECLARE 2019, LNCS 12057, pp 99–105, 2020 10. Mainini A.: Profile page in Spiele-Autoren-Zunft e.V. Game Designers Associa- tion’s website, https://www.spieleautorenzunft.de/authors-details.html?member= 241. Last accessed 30 March 2020 11. Papadimitriou C. H.: Computational Complexity. Addison-Wesley (1994) 12. Stuckey P. J., Becket R. , Fischer J.: Philosophy of the MiniZinc challenge. Con- straints 15 (3), 307-316 (2010) 13. Stuckey P. J., Marriot K., Tack G.: The MiniZinc Handbook 2.3.1. https://www. minizinc.org 14. Tange O.: GNU Parallel 2018. https://doi.org/https://doi.org/10.5281/zenodo.1146014 (2018)