1 /* A solver for the Japanese number-puzzle Hashiwokakero
2 * (http://en.wikipedia.org/wiki/Hashiwokakero)
4 * Sebastian Nowozin <nowozin@gmail.com>, 13th January 2009
10 param givens{rows, cols}, integer, >= 0, <= 8, default 0;
12 /* Set of vertices as (row,col) coordinates */
13 set V := { (i,j) in { rows, cols }: givens[i,j] != 0 };
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
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
29 /* Indicators: use edge once/twice */
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;
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];
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;
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.
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 };
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);
77 /* Variable-Upper-Bound (VUB) constraints: xe1/xe2 bound the flows.
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]);
84 /* A feasible solution is enough
90 /* Output solution graphically */
91 printf "\nSolution:\n";
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} " ";
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} "=";
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} " ";
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} " ";
137 /* This is a difficult 25x25 Hashiwokakero.
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
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