this repo has no description
dekker.one
1/***
2--- !Test
3extra_files: [sudoku_1_16x16.dzn]
4solvers: [cbc, chuffed]
5check_against: [cbc, chuffed]
6expected: !Result
7 solution: !Solution {}
8--- !Test
9extra_files: [sudoku_2_16x16.dzn]
10solvers: [cbc, chuffed]
11check_against: [cbc, chuffed]
12expected: !Result
13 solution: !Solution {}
14--- !Test
15extra_files: [sudoku_3_16x16.dzn]
16solvers: [cbc, chuffed]
17check_against: [cbc, chuffed]
18expected: !Result
19 solution: !Solution {}
20--- !Test
21extra_files: [sudoku_4_16x16.dzn]
22solvers: [cbc, chuffed]
23check_against: [cbc, chuffed]
24expected: !Result
25 solution: !Solution {}
26--- !Test
27extra_files: [sudoku_5_16x16.dzn]
28solvers: [cbc, chuffed]
29check_against: [cbc, chuffed]
30expected: !Result
31 solution: !Solution {}
32***/
33
34
35%-----------------------------------------------------------------------------%
36% Sudoku for squares of arbitrary size N = (S x S)
37%-----------------------------------------------------------------------------%
38
39%int: S=3;
40%int: N = S * S;
41%array[1..N,1..N] of int: puzzle_input=[|
42%0, 0, 0, 0, 0, 0, 0, 0, 0|
43%0, 6, 8, 4, 0, 1, 0, 7, 0|
44%0, 0, 0, 0, 8, 5, 0, 3, 0|
45%0, 2, 6, 8, 0, 9, 0, 4, 0|
46%0, 0, 7, 0, 0, 0, 9, 0, 0|
47%0, 5, 0, 1, 0, 6, 3, 2, 0|
48%0, 4, 0, 6, 1, 0, 0, 0, 0|
49%0, 3, 0, 2, 0, 7, 6, 9, 0|
50%0, 0, 0, 0, 0, 0, 0, 0, 0|
51%|];
52
53int: S;
54int: N=S*S;
55array[1..N,1..N] of int: puzzle_input;
56
57%int: S=4;
58%int: N=S*S;
59%array[1..N,1..N] of int: puzzle_input=[|
60%13, 4, 0, 16, 0, 2, 0, 0, 0, 0, 0, 0, 11, 0, 14, 10|
61%9, 12, 14, 5, 7, 0, 0, 15, 0, 0, 0, 0, 0, 2, 1, 0|
62%2, 15, 0, 6, 16, 0, 10, 9, 0, 0, 0, 0, 0, 5, 3, 0|
63%0, 0, 1, 0, 5, 0, 14, 0, 0, 0, 0, 0, 9, 6, 0, 0|
64%0, 0, 0, 0, 10, 12, 0, 5, 0, 0, 13, 0, 0, 0, 6, 8|
65%0, 0, 0, 0, 8, 0, 9, 0, 2, 0, 0, 14, 16, 0, 0, 11|
66%0, 0, 0, 0, 0, 0, 6, 7, 9, 0, 0, 0, 5, 15, 13, 12|
67%0, 0, 0, 0, 0, 0, 4, 0, 0, 0, 0, 12, 2, 0, 0, 3|
68%16, 9, 15, 10, 0, 0, 0, 4, 0, 6, 0, 2, 0, 0, 0, 0|
69%0, 13, 0, 3, 0, 11, 0, 0, 0, 4, 1, 16, 0, 0, 0, 0|
70%0, 0, 8, 12, 6, 7, 16, 0, 0, 5, 0, 0, 0, 0, 0, 0|
71%0, 2, 11, 0, 1, 0, 0, 0, 10, 13, 12, 0, 0, 0, 0, 0|
72%4, 0, 12, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 13, 0, 9|
73%3, 6, 0, 0, 0, 0, 0, 0, 12, 1, 11, 8, 14, 0, 0, 5|
74%0, 14, 0, 0, 0, 0, 0, 0, 0, 0, 7, 10, 15, 11, 0, 4|
75%0, 11, 10, 1, 0, 0, 0, 0, 0, 0, 15, 9, 6, 0, 7, 0|];
76
77%int: S=5;
78%int: N=S*S;
79%array[1..N,1..N] of int: puzzle_input=[|
80%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|
81%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|
82%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|
83%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|
84%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|
85%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|
86%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|
87%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|
88%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|
89%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|
90%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|
91%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|
92%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|
93%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|
94%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|
95%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|
96%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|
97%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|
98%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|
99%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|
100%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|
101%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|
102%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|
103%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|
104%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|];
105
106array[1..N*N] of var 1..N: puzzle;
107
108constraint forall (i in 1..N, j in 1..N) (
109 if (puzzle_input[i,j]==0) then true
110 else puzzle[(i-1)*N+j]==puzzle_input[i,j]
111 endif
112 );
113
114ann: total;
115
116function var int: eq_const(var int: x, int: d) ::total =
117 if d in dom(x) then let {
118 array[int] of var int: i2ax = int2a(x)
119 } in i2ax[d] else 0 endif;
120
121function array[int] of var int: int2a(var int: x) ::total =
122 let {
123 array[dom(x)] of var 0..1: a;
124 constraint int_lin_eq([1|i in index_set(a)],a,1);
125 constraint int_lin_eq([i|i in index_set(a)]++[-1],a++[x],0);
126 } in a;
127
128predicate alldiff(array[int] of var int: x) =
129 forall (d in dom_array(x)) (
130 int_lin_le([1|i in index_set(x)],[eq_const(x[i],d) | i in index_set(x)],1)
131 );
132
133predicate alldiff_builtin(array[int] of var int: x);
134
135 % All cells in a row, in a column, and in a subsquare are different.
136constraint
137 forall(i in 1..N)( alldiff(j in 1..N)( puzzle[(i-1)*N+j] ))
138 /\
139 forall(j in 1..N)( alldiff(i in 1..N)( puzzle[(i-1)*N+j] ))
140 /\
141 forall(i,j in 1..S)
142 ( alldiff(p,q in 1..S)( puzzle[(S*(i-1)+p-1)*N+(S*(j-1)+q)] ))
143 ;
144
145
146solve satisfy;
147
148%-----------------------------------------------------------------------------%
149%
150% The data for the puzzle that causes satz to make 1 backtrack (normally none
151% are made).
152%
153