|
1 /* A solver for the Japanese number-puzzle Hashiwokakero |
|
2 * (http://en.wikipedia.org/wiki/Hashiwokakero) |
|
3 * |
|
4 * Sebastian Nowozin <nowozin@gmail.com>, 13th January 2009 |
|
5 */ |
|
6 |
|
7 param n := 25; |
|
8 set rows := 1..n; |
|
9 set cols := 1..n; |
|
10 param givens{rows, cols}, integer, >= 0, <= 8, default 0; |
|
11 |
|
12 /* Set of vertices as (row,col) coordinates */ |
|
13 set V := { (i,j) in { rows, cols }: givens[i,j] != 0 }; |
|
14 |
|
15 /* Set of feasible horizontal edges from (i,j) to (k,l) rightwards */ |
|
16 set Eh := { (i,j,k,l) in { V, V }: |
|
17 i = k and j < l and # Same row and left to right |
|
18 card({ (s,t) in V: s = i and t > j and t < l }) = 0 # No vertex inbetween |
|
19 }; |
|
20 |
|
21 /* Set of feasible vertical edges from (i,j) to (k,l) downwards */ |
|
22 set Ev := { (i,j,k,l) in { V, V }: |
|
23 j = l and i < k and # Same column and top to bottom |
|
24 card({ (s,t) in V: t = j and s > i and s < k }) = 0 # No vertex inbetween |
|
25 }; |
|
26 |
|
27 set E := Eh union Ev; |
|
28 |
|
29 /* Indicators: use edge once/twice */ |
|
30 var xe1{E}, binary; |
|
31 var xe2{E}, binary; |
|
32 |
|
33 /* Constraint: Do not use edge or do use once or do use twice */ |
|
34 s.t. edge_sel{(i,j,k,l) in E}: |
|
35 xe1[i,j,k,l] + xe2[i,j,k,l] <= 1; |
|
36 |
|
37 /* Constraint: There must be as many edges used as the node value */ |
|
38 s.t. satisfy_vertex_demand{(s,t) in V}: |
|
39 sum{(i,j,k,l) in E: (i = s and j = t) or (k = s and l = t)} |
|
40 (xe1[i,j,k,l] + 2.0*xe2[i,j,k,l]) = givens[s,t]; |
|
41 |
|
42 /* Constraint: No crossings */ |
|
43 s.t. no_crossing1{(i,j,k,l) in Eh, (s,t,u,v) in Ev: |
|
44 s < i and u > i and j < t and l > t}: |
|
45 xe1[i,j,k,l] + xe1[s,t,u,v] <= 1; |
|
46 s.t. no_crossing2{(i,j,k,l) in Eh, (s,t,u,v) in Ev: |
|
47 s < i and u > i and j < t and l > t}: |
|
48 xe1[i,j,k,l] + xe2[s,t,u,v] <= 1; |
|
49 s.t. no_crossing3{(i,j,k,l) in Eh, (s,t,u,v) in Ev: |
|
50 s < i and u > i and j < t and l > t}: |
|
51 xe2[i,j,k,l] + xe1[s,t,u,v] <= 1; |
|
52 s.t. no_crossing4{(i,j,k,l) in Eh, (s,t,u,v) in Ev: |
|
53 s < i and u > i and j < t and l > t}: |
|
54 xe2[i,j,k,l] + xe2[s,t,u,v] <= 1; |
|
55 |
|
56 |
|
57 /* Model connectivity by auxiliary network flow problem: |
|
58 * One vertex becomes a target node and all other vertices send a unit flow |
|
59 * to it. The edge selection variables xe1/xe2 are VUB constraints and |
|
60 * therefore xe1/xe2 select the feasible graph for the max-flow problems. |
|
61 */ |
|
62 set node_target := { (s,t) in V: |
|
63 card({ (i,j) in V: i < s or (i = s and j < t) }) = 0}; |
|
64 set node_sources := { (s,t) in V: (s,t) not in node_target }; |
|
65 |
|
66 var flow_forward{ E }, >= 0; |
|
67 var flow_backward{ E }, >= 0; |
|
68 s.t. flow_conservation{ (s,t) in node_target, (p,q) in V }: |
|
69 /* All incoming flows */ |
|
70 - sum{(i,j,k,l) in E: k = p and l = q} flow_forward[i,j,k,l] |
|
71 - sum{(i,j,k,l) in E: i = p and j = q} flow_backward[i,j,k,l] |
|
72 /* All outgoing flows */ |
|
73 + sum{(i,j,k,l) in E: k = p and l = q} flow_backward[i,j,k,l] |
|
74 + sum{(i,j,k,l) in E: i = p and j = q} flow_forward[i,j,k,l] |
|
75 = 0 + (if (p = s and q = t) then card(node_sources) else -1); |
|
76 |
|
77 /* Variable-Upper-Bound (VUB) constraints: xe1/xe2 bound the flows. |
|
78 */ |
|
79 s.t. connectivity_vub1{(i,j,k,l) in E}: |
|
80 flow_forward[i,j,k,l] <= card(node_sources)*(xe1[i,j,k,l] + xe2[i,j,k,l]); |
|
81 s.t. connectivity_vub2{(i,j,k,l) in E}: |
|
82 flow_backward[i,j,k,l] <= card(node_sources)*(xe1[i,j,k,l] + xe2[i,j,k,l]); |
|
83 |
|
84 /* A feasible solution is enough |
|
85 */ |
|
86 minimize cost: 0; |
|
87 |
|
88 solve; |
|
89 |
|
90 /* Output solution graphically */ |
|
91 printf "\nSolution:\n"; |
|
92 for { row in rows } { |
|
93 for { col in cols } { |
|
94 /* First print this cell information: givens or space */ |
|
95 printf{0..0: givens[row,col] != 0} "%d", givens[row,col]; |
|
96 printf{0..0: givens[row,col] = 0 and |
|
97 card({(i,j,k,l) in Eh: i = row and col >= j and col < l and |
|
98 xe1[i,j,k,l] = 1}) = 1} "-"; |
|
99 printf{0..0: givens[row,col] = 0 and |
|
100 card({(i,j,k,l) in Eh: i = row and col >= j and col < l and |
|
101 xe2[i,j,k,l] = 1}) = 1} "="; |
|
102 printf{0..0: givens[row,col] = 0 |
|
103 and card({(i,j,k,l) in Ev: j = col and row >= i and row < k and |
|
104 xe1[i,j,k,l] = 1}) = 1} "|"; |
|
105 printf{0..0: givens[row,col] = 0 |
|
106 and card({(i,j,k,l) in Ev: j = col and row >= i and row < k and |
|
107 xe2[i,j,k,l] = 1}) = 1} '"'; |
|
108 printf{0..0: givens[row,col] = 0 |
|
109 and card({(i,j,k,l) in Eh: i = row and col >= j and col < l and |
|
110 (xe1[i,j,k,l] = 1 or xe2[i,j,k,l] = 1)}) = 0 |
|
111 and card({(i,j,k,l) in Ev: j = col and row >= i and row < k and |
|
112 (xe1[i,j,k,l] = 1 or xe2[i,j,k,l] = 1)}) = 0} " "; |
|
113 |
|
114 /* Now print any edges */ |
|
115 printf{(i,j,k,l) in Eh: i = row and col >= j and col < l and xe1[i,j,k,l] = 1} "-"; |
|
116 printf{(i,j,k,l) in Eh: i = row and col >= j and col < l and xe2[i,j,k,l] = 1} "="; |
|
117 |
|
118 printf{(i,j,k,l) in Eh: i = row and col >= j and col < l and |
|
119 xe1[i,j,k,l] = 0 and xe2[i,j,k,l] = 0} " "; |
|
120 printf{0..0: card({(i,j,k,l) in Eh: i = row and col >= j and col < l}) = 0} " "; |
|
121 } |
|
122 printf "\n"; |
|
123 for { col in cols } { |
|
124 printf{(i,j,k,l) in Ev: j = col and row >= i and row < k and xe1[i,j,k,l] = 1} "|"; |
|
125 printf{(i,j,k,l) in Ev: j = col and row >= i and row < k and xe2[i,j,k,l] = 1} '"'; |
|
126 printf{(i,j,k,l) in Ev: j = col and row >= i and row < k and |
|
127 xe1[i,j,k,l] = 0 and xe2[i,j,k,l] = 0} " "; |
|
128 /* No vertical edges: skip also a field */ |
|
129 printf{0..0: card({(i,j,k,l) in Ev: j = col and row >= i and row < k}) = 0} " "; |
|
130 printf " "; |
|
131 } |
|
132 printf "\n"; |
|
133 } |
|
134 |
|
135 data; |
|
136 |
|
137 /* This is a difficult 25x25 Hashiwokakero. |
|
138 */ |
|
139 param givens : 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 |
|
140 25 := |
|
141 1 2 . 2 . 2 . . 2 . 2 . . 2 . . . . 2 . 2 . 2 . 2 . |
|
142 2 . 1 . . . . 2 . . . 4 . . 5 . 2 . . 1 . 2 . 2 . 1 |
|
143 3 2 . . 5 . 4 . . 3 . . . . . 1 . . 4 . 5 . 1 . 1 . |
|
144 4 . . . . . . . . . . . 1 . 3 . . 1 . . . . . . . . |
|
145 5 2 . . 6 . 6 . . 8 . 5 . 2 . . 3 . 5 . 7 . . 2 . . |
|
146 6 . 1 . . . . . . . . . 1 . . 2 . . . . . 1 . . . 3 |
|
147 7 2 . . . . 5 . . 6 . 4 . . 2 . . . 2 . 5 . 4 . 2 . |
|
148 8 . 2 . 2 . . . . . . . . . . . 3 . . 3 . . . 1 . 2 |
|
149 9 . . . . . . . . . . 4 . 2 . 2 . . 1 . . . 3 . 1 . |
|
150 10 2 . 3 . . 6 . . 2 . . . . . . . . . . 3 . . . . . |
|
151 11 . . . . 1 . . 2 . . 5 . . 1 . 4 . 3 . . . . 2 . 4 |
|
152 12 . . 2 . . 1 . . . . . . 5 . 4 . . . . 4 . 3 . . . |
|
153 13 2 . . . 3 . 1 . . . . . . . . 3 . . 5 . 5 . . 2 . |
|
154 14 . . . . . 2 . 5 . . 7 . 5 . 3 . 1 . . 1 . . 1 . 4 |
|
155 15 2 . 5 . 3 . . . . 1 . 2 . 1 . . . . 2 . 4 . . 2 . |
|
156 16 . . . . . 1 . . . . . . . . . . 2 . . 2 . 1 . . 3 |
|
157 17 2 . 6 . 6 . . 2 . . 2 . 2 . 5 . . . . . 2 . . . . |
|
158 18 . . . . . 1 . . . 3 . . . . . 1 . . 1 . . 4 . 3 . |
|
159 19 . . 4 . 5 . . 2 . . . 2 . . 6 . 6 . . 3 . . . . 3 |
|
160 20 2 . . . . . . . . . 2 . . 1 . . . . . . 1 . . 1 . |
|
161 21 . . 3 . . 3 . 5 . 5 . . 4 . 6 . 7 . . 4 . 6 . . 4 |
|
162 22 2 . . . 3 . 5 . 2 . 1 . . . . . . . . . . . . . . |
|
163 23 . . . . . . . . . 1 . . . . . . 3 . 2 . . 5 . . 5 |
|
164 24 2 . 3 . 3 . 5 . 4 . 3 . 3 . 4 . . 2 . 2 . . . 1 . |
|
165 25 . 1 . 2 . 2 . . . 2 . 2 . . . 2 . . . . 2 . 2 . 2 |
|
166 ; |
|
167 |
|
168 end; |