this repo has no description
dekker.one
1% RUNS ON mzn_mer_fd
2% RUNS ON mzn_mer_lazyfd
3% RUNS ON mzn_mer_lp
4% RUNS ON zinc_fdic_mznlib
5% RUNS ON zinc_mip_hl
6% RUNS ON minizinc_cpx
7% RUNS ON minizinc_fd
8%
9%-----------------------------------------------------------------------------%
10% Sudoku for squares of arbitrary size N = (S x S)
11%-----------------------------------------------------------------------------%
12
13%int: S=3;
14%int: N = S * S;
15%array[1..N,1..N] of int: puzzle_input=[|
16%0, 0, 0, 0, 0, 0, 0, 0, 0|
17%0, 6, 8, 4, 0, 1, 0, 7, 0|
18%0, 0, 0, 0, 8, 5, 0, 3, 0|
19%0, 2, 6, 8, 0, 9, 0, 4, 0|
20%0, 0, 7, 0, 0, 0, 9, 0, 0|
21%0, 5, 0, 1, 0, 6, 3, 2, 0|
22%0, 4, 0, 6, 1, 0, 0, 0, 0|
23%0, 3, 0, 2, 0, 7, 6, 9, 0|
24%0, 0, 0, 0, 0, 0, 0, 0, 0|
25%|];
26
27int: S;
28int: N=S*S;
29array[1..N,1..N] of int: puzzle_input;
30
31%int: S=4;
32%int: N=S*S;
33%array[1..N,1..N] of int: puzzle_input=[|
34%13, 4, 0, 16, 0, 2, 0, 0, 0, 0, 0, 0, 11, 0, 14, 10|
35%9, 12, 14, 5, 7, 0, 0, 15, 0, 0, 0, 0, 0, 2, 1, 0|
36%2, 15, 0, 6, 16, 0, 10, 9, 0, 0, 0, 0, 0, 5, 3, 0|
37%0, 0, 1, 0, 5, 0, 14, 0, 0, 0, 0, 0, 9, 6, 0, 0|
38%0, 0, 0, 0, 10, 12, 0, 5, 0, 0, 13, 0, 0, 0, 6, 8|
39%0, 0, 0, 0, 8, 0, 9, 0, 2, 0, 0, 14, 16, 0, 0, 11|
40%0, 0, 0, 0, 0, 0, 6, 7, 9, 0, 0, 0, 5, 15, 13, 12|
41%0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 12, 2, 0, 0, 3|
42%16, 9, 15, 10, 0, 0, 0, 4, 0, 6, 0, 2, 0, 0, 0, 0|
43%0, 13, 0, 3, 0, 11, 0, 0, 0, 4, 1, 16, 0, 0, 0, 0|
44%0, 0, 8, 12, 6, 7, 16, 0, 0, 5, 0, 0, 0, 0, 0, 0|
45%0, 2, 11, 0, 1, 0, 0, 0, 10, 13, 12, 0, 0, 0, 0, 0|
46%4, 0, 12, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 13, 0, 9|
47%3, 6, 0, 0, 0, 0, 0, 0, 12, 1, 11, 8, 14, 0, 0, 5|
48%0, 14, 0, 0, 0, 0, 0, 0, 0, 0, 7, 10, 15, 11, 0, 4|
49%0, 11, 10, 1, 0, 0, 0, 0, 0, 0, 15, 9, 6, 0, 7, 0|];
50
51%int: S=5;
52%int: N=S*S;
53%array[1..N,1..N] of int: puzzle_input=[|
54%0, 12, 0, 25, 10, 0, 0, 0, 11, 24, 2, 0, 0, 0, 14, 23, 0, 9, 0, 0, 19, 0, 4, 0, 3|
55%0, 14, 0, 4, 1, 0, 15, 21, 2, 0, 0, 0, 13, 12, 0, 0, 0, 20, 24, 0, 0, 0, 8, 18, 5|
56%0, 18, 0, 9, 17, 0, 0, 6, 0, 5, 0, 0, 21, 24, 0, 19, 0, 0, 10, 16, 0, 0, 23, 0, 0|
57%16, 23, 0, 0, 0, 0, 25, 10, 14, 0, 22, 0, 0, 1, 6, 0, 7, 0, 0, 0, 0, 0, 20, 24, 0|
58%0, 0, 0, 0, 0, 7, 0, 0, 0, 12, 19, 0, 0, 15, 0, 0, 5, 6, 0, 0, 22, 0, 0, 16, 0|
59%0, 17, 10, 0, 0, 0, 0, 0, 0, 11, 0, 12, 24, 0, 0, 6, 21, 0, 18, 0, 0, 19, 0, 0, 0|
60%0, 13, 0, 19, 0, 0, 0, 0, 21, 1, 10, 15, 22, 11, 0, 0, 16, 0, 25, 0, 23, 0, 5, 0, 0|
61%9, 22, 0, 11, 15, 12, 18, 5, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 8, 23, 10, 17, 0, 0, 0|
62%0, 0, 0, 2, 0, 0, 0, 24, 0, 25, 0, 13, 0, 23, 0, 0, 0, 0, 4, 0, 15, 9, 22, 0, 21|
63%0, 24, 21, 3, 23, 6, 0, 15, 0, 0, 0, 25, 18, 0, 17, 0, 0, 0, 9, 0, 14, 12, 0, 8, 0|
64%4, 15, 0, 0, 5, 0, 11, 0, 1, 0, 9, 16, 14, 10, 0, 0, 6, 17, 0, 0, 0, 13, 0, 3, 19|
65%0, 0, 0, 10, 0, 0, 0, 8, 19, 0, 0, 6, 0, 17, 0, 0, 0, 16, 0, 25, 4, 1, 0, 5, 0|
66%0, 1, 19, 13, 0, 0, 0, 25, 0, 0, 3, 2, 11, 0, 0, 12, 0, 23, 0, 0, 0, 21, 0, 0, 0|
67%0, 21, 11, 0, 0, 17, 7, 0, 5, 3, 0, 23, 8, 0, 0, 0, 1, 0, 2, 13, 0, 25, 0, 10, 14|
68%0, 0, 23, 0, 0, 4, 0, 0, 0, 14, 7, 0, 0, 25, 0, 0, 0, 24, 0, 9, 2, 0, 0, 0, 0|
69%0, 0, 0, 7, 18, 11, 5, 0, 0, 22, 0, 14, 0, 0, 0, 1, 0, 2, 20, 0, 3, 0, 19, 13, 0|
70%6, 10, 2, 14, 0, 0, 0, 20, 0, 0, 0, 0, 23, 7, 4, 0, 12, 25, 3, 0, 0, 16, 21, 17, 0|
71%15, 0, 0, 0, 11, 0, 21, 0, 0, 0, 0, 0, 17, 8, 22, 5, 18, 0, 0, 0, 7, 24, 0, 0, 0|
72%0, 0, 13, 0, 21, 1, 0, 23, 24, 0, 0, 0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 0, 0, 8|
73%0, 9, 0, 12, 0, 0, 0, 14, 7, 0, 0, 24, 0, 19, 20, 16, 0, 0, 0, 10, 0, 0, 0, 25, 18|
74%21, 25, 1, 5, 0, 0, 0, 0, 0, 2, 0, 17, 0, 14, 18, 0, 4, 0, 7, 0, 0, 0, 0, 0, 16|
75%8, 19, 0, 15, 0, 0, 9, 0, 20, 21, 25, 0, 3, 0, 11, 0, 0, 0, 16, 0, 0, 0, 0, 0, 0|
76%0, 0, 0, 0, 2, 0, 0, 7, 0, 0, 0, 22, 0, 0, 9, 17, 14, 0, 23, 0, 8, 4, 0, 0, 6|
77%0, 4, 0, 0, 6, 18, 0, 3, 10, 17, 8, 0, 0, 0, 0, 0, 0, 0, 0, 12, 21, 22, 0, 0, 7|
78%0, 0, 17, 0, 0, 5, 0, 4, 25, 0, 12, 19, 20, 13, 0, 0, 0, 0, 0, 1, 0, 14, 9, 0, 11|];
79
80array[1..N*N] of var 1..N: puzzle;
81
82constraint forall (i in 1..N, j in 1..N) (
83 if (puzzle_input[i,j]==0) then true
84 else puzzle[(i-1)*N+j]==puzzle_input[i,j]
85 endif
86 );
87
88ann: total;
89
90function var int: eq_const(var int: x, int: d) ::total =
91 if d in dom(x) then let {
92 array[int] of var int: i2ax = int2a(x)
93 } in i2ax[d] else 0 endif;
94
95function array[int] of var int: int2a(var int: x) ::total =
96 let {
97 array[dom(x)] of var 0..1: a;
98 constraint int_lin_eq([1|i in index_set(a)],a,1);
99 constraint int_lin_eq([i|i in index_set(a)]++[-1],a++[x],0);
100 } in a;
101
102predicate alldiff(array[int] of var int: x) =
103 forall (d in dom_array(x)) (
104 int_lin_le([1|i in index_set(x)],[eq_const(x[i],d) | i in index_set(x)],1)
105 );
106
107predicate alldiff_builtin(array[int] of var int: x);
108
109 % All cells in a row, in a column, and in a subsquare are different.
110constraint
111 forall(i in 1..N)( alldiff(j in 1..N)( puzzle[(i-1)*N+j] ))
112 /\
113 forall(j in 1..N)( alldiff(i in 1..N)( puzzle[(i-1)*N+j] ))
114 /\
115 forall(i,j in 1..S)
116 ( alldiff(p,q in 1..S)( puzzle[(S*(i-1)+p-1)*N+(S*(j-1)+q)] ))
117 ;
118
119
120solve satisfy;
121
122%-----------------------------------------------------------------------------%
123%
124% The data for the puzzle that causes satz to make 1 backtrack (normally none
125% are made).
126%
127