/* Hidato puzzle in Picat. http://www.shockwave.com/gamelanding/hidato.jsp http://www.hidato.com/ """ Puzzles start semi-filled with numbered tiles. The first and last numbers are circled. Connect the numbers together to win. Consecutive number must touch horizontally, vertically, or diagonally. """ Problem CP SAT SMT/z3 SMT/cvc4 (forward/ (system time) (system time) up) -------------------------------------------------- 1 0.001s 0.008s 0.095s 0.268s 2 0.014s 0.085s 4.94s >12000s (>3h) 3 0.008s 0.039s 0.495s 124.46s 4 0.002s 0.033s 0.419s 43.90s 5 0.015s 0.113s 2.27s 219.69s 6 0.037s 0.175s 25.05s - 7 280.145s 1.461s 751.89s - 8 97.114s 1.835s 5636.67s - As usual, CP tends to be faster on the smaller instances (1-6) and SAT is (much) faster on the larger instances (7 and 8). Also it's interesting that CP is much slower on problem 7 than problem 8 while SAT has the opposite behavior. SMT/z3 is slow. SMT/cvc4 is very slow on the simple examples so I skipped the rest of the problems. Note that the time for the SMT solvers is via the system time command since the Picat's time/1 don't report the correct solve time (it's way too small). Model created by Hakan Kjellerstrand, hakank@gmail.com See also my Picat page: http://www.hakank.org/picat/ */ import util. import sat. main => go. main(Args) => statistics(runtime,_), N = Args[1].to_int, solveit(N), statistics(runtime, [_,Time]), println(time=Time), nl. go => time2($solveit(6)). % % Test all problems % go2 => foreach(P in 1..8) time2($solveit(P)) end. % % Solve the problem instance % solveit(Problem) => printf("\nProblem %d\n", Problem), problem(Problem,X), hidato(X). % % Solve the Hidato puzzle % hidato(X) => N = X.length, XList = array_matrix_to_list(X), XList :: 1..N*N, % Valid connections, used by the table constraint below Connections = [{I1,J1,I2,J2} : I1 in 1..N, J1 in 1..N, I2 in 1..N, J2 in 1..N, abs(I1-I2) =< 1, abs(J1-J2) =< 1, (I1 !=I2; J1 != J2)], % place all integers from 1..r*c all_distinct(XList), NN1 = (N*N)-1, Extras = [], Connect = [], % table constraint table_in(Connect,Connections), foreach(K in 1..NN1) % define temporary variables for finding % the index of this and the next number (K) I :: 1..N, % index I J :: 1..N, % index J A :: -1..1, % offset from K's position B :: -1..1, % ibid % needed for element IA :: 1..N, JB :: 1..N, IA #= I+A, JB #= J+B, % some extra constraints abs(A)+abs(B) #>= 1, % both A and B cannot be 0, i.e. it must be a move % 1. First: fix this k, i.e. % K #= X[I,J], % don't work (instantiation fault) IJ #= (I-1)*N + J, element(IJ, XList, K), % 2. Then, find the position of the next value, i.e. % K+1 #= X[I+A,J+B], % this don't work IA_JB #= (I-1+A)*N + JB, K1 = K+1, element(IA_JB, XList, K1), Extras := Extras ++ [IJ,IA_JB,A,B], Connect := Connect ++ [(I,J,IA,JB)] end, % search if membchk(sat,loaded_modules()) then % This seems to be the best for the SAT solver Vars = XList ++ Extras ++ Connect else % Vars = Extras ++ Connect ++ XList, % This seems to be the best for CP Vars = Connect ++ XList ++ Extras end, % solve([inout,down],Vars), solve($[cvc4,forward,up],Vars), pretty_print(X). pretty_print(X) => N = X.length, foreach(I in 1..N) foreach(J in 1..N) printf("%3d ", X[I,J]) end, nl end, nl. % % Problems % % Simple problem % % solution: % 6 7 9 % 5 2 8 % 1 4 3 % problem(1, P) => P = {{6,_,9}, {_,2,8}, {1,_,_}}. problem(2, P) => P = {{ _,44,41, _, _, _, _}, { _,43, _,28,29, _, _}, { _, 1, _, _, _,33, _}, { _, 2,25, 4,34, _,36}, {49,16, _,23, _, _, _}, { _,19, _, _,12, 7, _}, { _, _, _,14, _, _, _}}. % Problems from the book: % Gyora Bededek: "Hidato: 2000 Pure Logic Puzzles" % problem 1 (Practice} problem(3, P) => P = {{_, _,20, _, _}, {_, _, _,16,18}, {22, _,15, _, _}, {23, _, 1,14,11}, {_,25, _, _,12}}. % problem 2 (Practice} problem(4, P) => P = {{_, _, _, _,14}, {_,18,12, _, _}, {_, _,17, 4, 5}, {_, _, 7, _, _}, {9, 8,25, 1, _}}. % problem 3 (Beginner} problem(5, P) => P = {{ _,26, _, _, _,18}, { _, _,27, _, _,19}, {31,23, _, _,14, _}, { _,33, 8, _,15, 1}, { _, _, _, 5, _, _}, {35,36, _,10, _, _}}. % Problem 15 (Intermediate} problem(6,P) => P = {{64, _, _, _, _, _, _, _}, { 1,63, _,59,15,57,53, _}, { _, 4, _,14, _, _, _, _}, { 3, _,11, _,20,19, _,50}, { _, _, _, _,22, _,48,40}, { 9, _, _,32,23, _, _,41}, {27, _, _, _,36, _,46, _}, {28,30, _,35, _, _, _, _}}. % Problem 156 (Master} % (This is harder to solve for CP than the 12x12 prolem 188 below.) % problem(7, P) => P = {{88, _, _,100, _, _,37,_, _,34}, { _,86, _,96,41, _, _,36, _, _}, { _,93,95,83, _, _, _,31,47, _}, { _,91, _, _, _, _, _,29, _, _}, {11, _, _, _, _, _, _,45,51, _}, { _, 9, 5, 3, 1, _, _, _, _, _}, { _,13, 4, _, _, _, _, _, _, _}, {15, _, _,25, _, _,54,67, _, _}, { _,17, _,23, _,60,59, _,69, _}, {19, _,21,62,63, _, _, _, _, _}}. % Problem 188 (Genius} problem(8, P) => P = {{ _, _,134, 2, 4, _, _, _, _, _, _, _}, {136, _, _, 1, _, 5, 6, 10,115,106, _, _}, {139, _, _,124, _,122,117, _, _,107, _, _}, { _,131,126, _,123, _, _, 12, _, _, _,103}, { _, _,144, _, _, _, _, _, 14, _, 99,101}, { _, _,129, _, 23, 21, _, 16, 65, 97, 96, _}, { 30, 29, 25, _, _, 19, _, _, _, 66, 94, _}, { 32, _, _, 27, 57, 59, 60, _, _, _, _, 92}, { _, 40, 42, _, 56, 58, _, _, 72, _, _, _}, { _, 39, _, _, _, _, 78, 73, 71, 85, 69, _}, { 35, _, _, 46, 53, _, _, _, 80, 84, _, _}, { 36, _, 45, _, _, 52, 51, _, _, _, _, 88}}. % Variable selection selection(Selection) => Selection = [backward,constr,degree,ff,ffc,forward,inout,leftmost,max,min]. % Value selection choice(Choice) => Choice = [down,updown,split,reverse_split].