sudoku.mlw 23.4 KB
 MARCHE Claude committed Feb 21, 2014 1 `````` `````` Jean-Christophe Filliatre committed Mar 06, 2014 2 3 4 5 ``````(** {1 An Efficient Sudoku Solver } Author: Claude Marché (Inria) Guillaume Melquiond (Inria) *) `````` MARCHE Claude committed Feb 21, 2014 6 7 8 9 `````` (** {2 A theory of 9x9 grids} *) `````` Jean-Christophe Filliatre committed Mar 06, 2014 10 ``````module Grid `````` MARCHE Claude committed Feb 21, 2014 11 `````` `````` Andrei Paskevich committed Jun 15, 2018 12 13 `````` use int.Int use map.Map `````` MARCHE Claude committed Feb 21, 2014 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 `````` (** A grid is a map from integers to integers *) type grid = map int int (** valid indexes are 0..80 *) predicate is_index (i:int) = 0 <= i < 81 (** valid values are 0..9. 0 denotes an empty cell *) predicate valid_values (g:grid) = forall i. is_index i -> 0 <= g[i] <= 9 (** extensional equality of grids and sub-grids *) predicate grid_eq_sub (g1 g2:grid) (a b:int) = forall j. a <= j < b -> g1[j] = g2[j] predicate grid_eq (g1 g2:grid) = grid_eq_sub g1 g2 0 81 lemma grid_eq_sub: forall g1 g2 a b. 0 <= a <= 81 /\ 0 <= b <= 81 /\ grid_eq g1 g2 -> grid_eq_sub g1 g2 a b (** {3 Grid "Chunks"} A chunk is either a column, a row or a square. A chunk is defined by a starting index s and a set of 9 offsets {o0,..,o8}, that thus denotes a set of 9 cells {s+o0,..,s+o8} in a grid. Each cell of the grid belongs to 3 chunks, one of each kind. For each cell index, there is a unique starting index respectively for the column, the row and the square it belongs to. *) `````` Andrei Paskevich committed Jun 15, 2018 49 `````` use array.Array `````` MARCHE Claude committed Mar 04, 2014 50 `````` `````` MARCHE Claude committed Feb 21, 2014 51 `````` type sudoku_chunks = `````` MARCHE Claude committed Mar 04, 2014 52 53 54 55 56 57 `````` { column_start : array int; column_offsets : array int; row_start : array int; row_offsets : array int; square_start : array int; square_offsets : array int; `````` MARCHE Claude committed Feb 21, 2014 58 59 60 `````` } (** Chunks must point to valid indexes of the grid *) `````` MARCHE Claude committed Mar 04, 2014 61 62 63 64 `````` predicate chunk_valid_indexes (start:array int) (offsets:array int) = start.length = 81 /\ offsets.length = 9 /\ forall i o:int. is_index i /\ 0 <= o < 9 -> is_index(start[i] + offsets[o]) `````` MARCHE Claude committed Feb 21, 2014 65 66 67 `````` (** Chunks (of the same kind column, row or square) with distinct starting cells must be disjoint *) `````` MARCHE Claude committed Mar 04, 2014 68 69 `````` predicate disjoint_chunks (start:array int) (offsets:array int) = start.length = 81 /\ offsets.length = 9 /\ `````` MARCHE Claude committed Feb 21, 2014 70 71 `````` forall i1 i2 o:int. is_index i1 /\ is_index i2 /\ 0 <= o < 9 -> `````` MARCHE Claude committed Mar 04, 2014 72 73 74 `````` let s1 = start[i1] in let s2 = start[i2] in s1 <> s2 -> i1 <> s2 + offsets[o] `````` MARCHE Claude committed Feb 21, 2014 75 76 77 78 79 80 81 82 83 84 85 86 `````` (** A sudoku grid is well formed when chunks are valid and disjoint *) predicate well_formed_sudoku (s:sudoku_chunks) = chunk_valid_indexes s.column_start s.column_offsets /\ chunk_valid_indexes s.row_start s.row_offsets /\ chunk_valid_indexes s.square_start s.square_offsets /\ disjoint_chunks s.column_start s.column_offsets /\ disjoint_chunks s.row_start s.row_offsets /\ disjoint_chunks s.square_start s.square_offsets (** {3 Valid Sudoku Solutions} *) `````` Guillaume Melquiond committed Jun 14, 2018 87 88 `````` (** `valid_chunk g i start offsets` is true whenever the chunk denoted by `start,offsets` from cell `i` is "valid" in grid `g`, in `````` MARCHE Claude committed Feb 21, 2014 89 90 91 92 `````` the sense that it contains at most one occurence of each number between 1 and 9 *) predicate valid_chunk (g:grid) (i:int) `````` MARCHE Claude committed Mar 04, 2014 93 `````` (start:array int) (offsets:array int) = `````` MARCHE Claude committed Feb 21, 2014 94 95 96 97 `````` let s = start[i] in forall o1 o2 : int. 0 <= o1 < 9 /\ 0 <= o2 < 9 /\ o1 <> o2 -> let i1 = s + offsets[o1] in let i2 = s + offsets[o2] in `````` MARCHE Claude committed Mar 04, 2014 98 99 `````` 1 <= Map.get g i1 <= 9 /\ 1 <= Map.get g i2 <= 9 -> Map.get g i1 <> Map.get g i2 `````` MARCHE Claude committed Feb 21, 2014 100 101 102 103 104 105 106 107 108 109 `````` predicate valid_column (s:sudoku_chunks) (g:grid) (i:int) = valid_chunk g i s.column_start s.column_offsets predicate valid_row (s:sudoku_chunks) (g:grid) (i:int) = valid_chunk g i s.row_start s.row_offsets predicate valid_square (s:sudoku_chunks) (g:grid) (i:int) = valid_chunk g i s.square_start s.square_offsets `````` Guillaume Melquiond committed Jun 14, 2018 110 `````` (** `valid g` is true when all chunks are valid *) `````` MARCHE Claude committed Feb 21, 2014 111 112 113 114 `````` predicate valid (s:sudoku_chunks) (g : grid) = forall i : int. is_index i -> valid_column s g i /\ valid_row s g i /\ valid_square s g i `````` Guillaume Melquiond committed Jun 14, 2018 115 `````` (** `full g` is true when all cells are filled *) `````` MARCHE Claude committed Feb 21, 2014 116 `````` predicate full (g : grid) = `````` MARCHE Claude committed Mar 04, 2014 117 `````` forall i : int. is_index i -> 1 <= Map.get g i <= 9 `````` MARCHE Claude committed Feb 21, 2014 118 `````` `````` Guillaume Melquiond committed Jun 14, 2018 119 `````` (** `included g1 g2` *) `````` MARCHE Claude committed Feb 21, 2014 120 `````` predicate included (g1 g2 : grid) = `````` Jean-Christophe Filliatre committed Mar 06, 2014 121 `````` forall i : int. is_index i /\ 1 <= Map.get g1 i <= 9 -> `````` MARCHE Claude committed Mar 04, 2014 122 `````` Map.get g2 i = Map.get g1 i `````` MARCHE Claude committed Feb 21, 2014 123 124 125 126 `````` (** validity is monotonic w.r.t. inclusion *) lemma subset_valid_chunk : forall g h : grid. included g h -> `````` MARCHE Claude committed Mar 04, 2014 127 `````` forall i:int, s o:array int. is_index i /\ `````` MARCHE Claude committed Feb 21, 2014 128 129 130 131 `````` chunk_valid_indexes s o /\ valid_chunk h i s o -> valid_chunk g i s o lemma subset_valid : `````` Jean-Christophe Filliatre committed Mar 06, 2014 132 `````` forall s g h. `````` MARCHE Claude committed Feb 21, 2014 133 134 `````` well_formed_sudoku s /\ included g h /\ valid s h -> valid s g `````` Guillaume Melquiond committed Jun 14, 2018 135 136 `````` (** A solution of a grid `data` is a full grid `sol` that is valid and includes `data` *) `````` MARCHE Claude committed Feb 21, 2014 137 138 139 140 141 142 143 144 `````` predicate is_solution_for (s:sudoku_chunks) (sol:grid) (data:grid) = included data sol /\ full sol /\ valid s sol end (** {2 Concrete Values of Chunks for the Classical Sudoku Grid} *) `````` MARCHE Claude committed Mar 04, 2014 145 ``````module TheClassicalSudokuGrid `````` MARCHE Claude committed Feb 21, 2014 146 `````` `````` Andrei Paskevich committed Jun 15, 2018 147 148 149 `````` use Grid use map.Map use int.Int `````` MARCHE Claude committed Feb 21, 2014 150 `````` `````` Andrei Paskevich committed Jun 15, 2018 151 `````` use array.Array `````` MARCHE Claude committed Feb 21, 2014 152 `````` `````` MARCHE Claude committed Mar 04, 2014 153 154 155 `````` let classical_sudoku () : sudoku_chunks ensures { well_formed_sudoku result } = `````` Jean-Christophe Filliatre committed Mar 06, 2014 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 `````` (* column start *) let cs = Array.make 81 0 in cs[ 0]<-0; cs[ 1]<-1; cs[ 2]<-2; cs[ 3]<-3; cs[ 4]<-4; cs[ 5]<-5; cs[ 6]<-6; cs[ 7]<-7; cs[ 8]<-8; cs[ 9]<-0; cs[10]<-1; cs[11]<-2; cs[12]<-3; cs[13]<-4; cs[14]<-5; cs[15]<-6; cs[16]<-7; cs[17]<-8; cs[18]<-0; cs[19]<-1; cs[20]<-2; cs[21]<-3; cs[22]<-4; cs[23]<-5; cs[24]<-6; cs[25]<-7; cs[26]<-8; cs[27]<-0; cs[28]<-1; cs[29]<-2; cs[30]<-3; cs[31]<-4; cs[32]<-5; cs[33]<-6; cs[34]<-7; cs[35]<-8; cs[36]<-0; cs[37]<-1; cs[38]<-2; cs[39]<-3; cs[40]<-4; cs[41]<-5; cs[42]<-6; cs[43]<-7; cs[44]<-8; cs[45]<-0; cs[46]<-1; cs[47]<-2; cs[48]<-3; cs[49]<-4; cs[50]<-5; cs[51]<-6; cs[52]<-7; cs[53]<-8; cs[54]<-0; cs[55]<-1; cs[56]<-2; cs[57]<-3; cs[58]<-4; cs[59]<-5; cs[60]<-6; cs[61]<-7; cs[62]<-8; cs[63]<-0; cs[64]<-1; cs[65]<-2; cs[66]<-3; cs[67]<-4; cs[68]<-5; cs[69]<-6; cs[70]<-7; cs[71]<-8; cs[72]<-0; cs[73]<-1; cs[74]<-2; cs[75]<-3; cs[76]<-4; cs[77]<-5; cs[78]<-6; cs[79]<-7; cs[80]<-8; (* column offset *) let co = Array.make 9 0 in co[ 0]<-0; co[ 1]<-9; co[ 2]<-18; co[ 3]<-27; co[ 4]<-36; co[ 5]<-45; co[ 6]<-54; co[ 7]<-63; co[ 8]<-72; (* row start *) let rs = Array.make 81 0 in rs[ 0]<- 0; rs[ 1]<- 0; rs[ 2]<- 0; rs[ 3]<- 0; rs[ 4]<-0; rs[5]<-0; rs[ 6]<- 0; rs[ 7]<- 0; rs[ 8]<- 0; rs[ 9]<- 9; rs[10]<-9; rs[11]<-9; rs[12]<- 9; rs[13]<- 9; rs[14]<- 9; rs[15]<- 9; rs[16]<-9; rs[17]<-9; rs[18]<-18; rs[19]<-18; rs[20]<-18; rs[21]<-18; rs[22]<-18; rs[23]<-18; rs[24]<-18; rs[25]<-18; rs[26]<-18; rs[27]<-27; rs[28]<-27; rs[29]<-27; rs[30]<-27; rs[31]<-27; rs[32]<-27; rs[33]<-27; rs[34]<-27; rs[35]<-27; rs[36]<-36; rs[37]<-36; rs[38]<-36; rs[39]<-36; rs[40]<-36; rs[41]<-36; rs[42]<-36; rs[43]<-36; rs[44]<-36; rs[45]<-45; rs[46]<-45; rs[47]<-45; rs[48]<-45; rs[49]<-45; rs[50]<-45; rs[51]<-45; rs[52]<-45; rs[53]<-45; rs[54]<-54; rs[55]<-54; rs[56]<-54; rs[57]<-54; rs[58]<-54; rs[59]<-54; rs[60]<-54; rs[61]<-54; rs[62]<-54; rs[63]<-63; rs[64]<-63; rs[65]<-63; rs[66]<-63; rs[67]<-63; rs[68]<-63; rs[69]<-63; rs[70]<-63; rs[71]<-63; rs[72]<-72; rs[73]<-72; rs[74]<-72; rs[75]<-72; rs[76]<-72; rs[77]<-72; rs[78]<-72; rs[79]<-72; rs[80]<-72; (* row offset *) let ro = Array.make 9 0 in ro[ 0]<-0; ro[ 1]<-1; ro[ 2]<-2; ro[ 3]<-3; ro[ 4]<-4; ro[ 5]<-5; ro[ 6]<-6; ro[ 7]<-7; ro[ 8]<-8; (* square start *) let ss = Array.make 81 0 in ss[ 0]<- 0; ss[ 1]<- 0; ss[ 2]<- 0; ss[ 3]<- 3; ss[ 4]<- 3; ss[ 5]<- 3; ss[ 6]<- 6; ss[ 7]<- 6; ss[ 8]<- 6; ss[ 9]<- 0; ss[10]<- 0; ss[11]<- 0; ss[12]<- 3; ss[13]<- 3; ss[14]<- 3; ss[15]<- 6; ss[16]<- 6; ss[17]<- 6; ss[18]<- 0; ss[19]<- 0; ss[20]<- 0; ss[21]<- 3; ss[22]<- 3; ss[23]<- 3; ss[24]<- 6; ss[25]<- 6; ss[26]<- 6; ss[27]<-27; ss[28]<-27; ss[29]<-27; ss[30]<-30; ss[31]<-30; ss[32]<-30; ss[33]<-33; ss[34]<-33; ss[35]<-33; ss[36]<-27; ss[37]<-27; ss[38]<-27; ss[39]<-30; ss[40]<-30; ss[41]<-30; ss[42]<-33; ss[43]<-33; ss[44]<-33; ss[45]<-27; ss[46]<-27; ss[47]<-27; ss[48]<-30; ss[49]<-30; ss[50]<-30; ss[51]<-33; ss[52]<-33; ss[53]<-33; ss[54]<-54; ss[55]<-54; ss[56]<-54; ss[57]<-57; ss[58]<-57; ss[59]<-57; ss[60]<-60; ss[61]<-60; ss[62]<-60; ss[63]<-54; ss[64]<-54; ss[65]<-54; ss[66]<-57; ss[67]<-57; ss[68]<-57; ss[69]<-60; ss[70]<-60; ss[71]<-60; ss[72]<-54; ss[73]<-54; ss[74]<-54; ss[75]<-57; ss[76]<-57; ss[77]<-57; ss[78]<-60; ss[79]<-60; ss[80]<-60; (* square offset *) `````` Guillaume Melquiond committed Mar 16, 2016 217 218 219 `````` let sqo = Array.make 9 0 in sqo[0]<-0; sqo[1]<-1; sqo[2]<-2; sqo[3]<-9; sqo[4]<-10; sqo[5]<-11; sqo[6]<-18; sqo[7]<-19; sqo[8]<-20; `````` Jean-Christophe Filliatre committed Mar 06, 2014 220 221 `````` { column_start = cs; column_offsets = co; row_start = rs; row_offsets = ro; `````` Guillaume Melquiond committed Mar 16, 2016 222 `````` square_start = ss; square_offsets = sqo; } `````` MARCHE Claude committed Feb 21, 2014 223 224 225 226 227 228 229 230 231 `````` end (** {2 A Sudoku Solver} *) module Solver `````` Andrei Paskevich committed Jun 15, 2018 232 233 234 `````` use Grid use array.Array use int.Int `````` MARCHE Claude committed Feb 21, 2014 235 `````` `````` Jean-Christophe Filliatre committed Mar 06, 2014 236 `````` (** predicate for the loop invariant of next function *) `````` MARCHE Claude committed Feb 21, 2014 237 `````` predicate valid_chunk_up_to (g:grid) (i:int) `````` MARCHE Claude committed Mar 04, 2014 238 `````` (start:array int) (offsets:array int) (off:int) = `````` MARCHE Claude committed Feb 21, 2014 239 240 241 242 243 `````` let s = start[i] in forall o1 o2 : int. 0 <= o1 < off /\ 0 <= o2 < off /\ o1 <> o2 -> let i1 = s + offsets[o1] in let i2 = s + offsets[o2] in `````` Jean-Christophe Filliatre committed Mar 06, 2014 244 `````` 1 <= Map.get g i1 <= 9 /\ 1 <= Map.get g i2 <= 9 -> `````` MARCHE Claude committed Mar 04, 2014 245 `````` Map.get g i1 <> Map.get g i2 `````` MARCHE Claude committed Feb 21, 2014 246 247 248 `````` exception Invalid `````` Andrei Paskevich committed Jun 15, 2018 249 `````` use array.Array `````` MARCHE Claude committed Feb 21, 2014 250 `````` `````` Guillaume Melquiond committed Jun 14, 2018 251 252 `````` (** `check_valid_chunk g i start offsets` checks the validity of the chunk that includes `i` *) `````` MARCHE Claude committed Feb 21, 2014 253 `````` let check_valid_chunk (g:array int) (i:int) `````` MARCHE Claude committed Mar 04, 2014 254 `````` (start:array int) (offsets:array int) : unit `````` MARCHE Claude committed Feb 21, 2014 255 256 257 258 259 260 261 `````` requires { g.length = 81 } requires { valid_values g.elts } requires { is_index i } requires { chunk_valid_indexes start offsets } ensures { valid_chunk g.elts i start offsets } raises { Invalid -> not (valid_chunk g.elts i start offsets) } = `````` MARCHE Claude committed Mar 04, 2014 262 `````` let s = start[i] in `````` MARCHE Claude committed Feb 21, 2014 263 264 265 266 `````` let b = Array.make 10 False in for off = 0 to 8 do invariant { valid_chunk_up_to g.elts i start offsets off } invariant { forall o:int. 0 <= o < off -> `````` MARCHE Claude committed Mar 04, 2014 267 `````` let v = g[s + offsets[o]] in `````` MARCHE Claude committed Feb 21, 2014 268 269 270 271 `````` 1 <= v <= 9 -> b[v] = True } invariant { forall j:int. 1 <= j <= 9 -> b[j] = True -> exists o:int. `````` MARCHE Claude committed Mar 04, 2014 272 273 `````` 0 <= o < off /\ Map.get g.elts (s + offsets[o]) = j } let v = g[s + offsets[off]] in `````` MARCHE Claude committed Feb 21, 2014 274 275 `````` if 1 <= v && v <= 9 then begin `````` MARCHE Claude committed Mar 07, 2016 276 `````` if b[v] then raise Invalid; `````` MARCHE Claude committed Feb 21, 2014 277 278 279 280 `````` b[v] <- True end done `````` Jean-Christophe Filliatre committed Mar 06, 2014 281 `````` (** predicate for the loop invariant of next function *) `````` MARCHE Claude committed Feb 21, 2014 282 283 284 285 `````` predicate valid_up_to (s:sudoku_chunks) (g:grid) (i:int) = forall j : int. 0 <= j < i -> valid_column s g j /\ valid_row s g j /\ valid_square s g j `````` Guillaume Melquiond committed Jun 14, 2018 286 287 `````` (** `check_valid s g` checks if the (possibly partially filled) grid `g` is valid. (This function is not needed by the solver) *) `````` MARCHE Claude committed Feb 21, 2014 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 `````` let check_valid (s:sudoku_chunks) (g : array int) : bool requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } ensures { result <-> valid s g.elts } = try for i = 0 to 80 do invariant { valid_up_to s g.elts i } check_valid_chunk g i s.column_start s.column_offsets; check_valid_chunk g i s.row_start s.row_offsets; check_valid_chunk g i s.square_start s.square_offsets done; True with Invalid -> False end `````` Guillaume Melquiond committed Jun 14, 2018 305 `````` (** `full_up_to g i` is true when all cells `0..i-1` in grid `g` are `````` Jean-Christophe Filliatre committed Mar 06, 2014 306 `````` non empty *) `````` MARCHE Claude committed Feb 21, 2014 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 `````` predicate full_up_to (g : grid) (i : int) = forall j : int. 0 <= j < i -> 1 <= Map.get g j <= 9 lemma full_up_to_change : forall g i x. is_index i /\ full_up_to g i -> 1 <= x <= 9 -> full_up_to (Map.set g i x) (i+1) let rec lemma full_up_to_frame (g1 g2:grid) (i:int) requires { 0 <= i <= 81 } requires { grid_eq_sub g1 g2 0 i } requires { full_up_to g1 i } variant { i } ensures { full_up_to g2 i } = if i > 0 then begin assert { full_up_to g1 (i-1) }; full_up_to_frame g1 g2 (i-1) end let lemma full_up_to_frame_all (g1 g2:grid) (i:int) requires { 0 <= i <= 81 } requires { grid_eq g1 g2 } requires { full_up_to g1 i } ensures { full_up_to g2 i } = assert { grid_eq_sub g1 g2 0 i } `````` MARCHE Claude committed May 23, 2017 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 `````` let lemma valid_chunk_frame (start:array int) (offsets:array int) (g1 g2:grid) (i:int) requires { chunk_valid_indexes start offsets } requires { 0 <= i < 81 } requires { grid_eq g1 g2 } requires { valid_chunk g1 i start offsets } ensures { valid_chunk g2 i start offsets } = () let rec lemma valid_up_to_frame (s:sudoku_chunks) (g1 g2:grid) (i:int) requires { well_formed_sudoku s } requires { 0 <= i <= 81 } requires { grid_eq g1 g2 } requires { valid_up_to s g1 i } variant { i } ensures { valid_up_to s g2 i } = if i > 0 then begin assert { valid_up_to s g1 (i-1) }; valid_up_to_frame s g1 g2 (i-1); valid_chunk_frame s.column_start s.column_offsets g1 g2 (i-1); valid_chunk_frame s.row_start s.row_offsets g1 g2 (i-1); valid_chunk_frame s.square_start s.square_offsets g1 g2 (i-1); end `````` MARCHE Claude committed Feb 21, 2014 357 358 359 360 `````` (** how to prove the "hard" property : if `````` Guillaume Melquiond committed Jun 14, 2018 361 `````` `valid_up_to s g i` `````` MARCHE Claude committed Feb 21, 2014 362 363 364 `````` and `````` Guillaume Melquiond committed Jun 14, 2018 365 `````` `h = g[i <- k` (with 1 <= k <= 9)] `````` MARCHE Claude committed Feb 21, 2014 366 367 368 `````` and `````` Guillaume Melquiond committed Jun 14, 2018 369 `````` `valid_column s h i /\ valid_row s h i /\ valid_square s h i` `````` MARCHE Claude committed Feb 21, 2014 370 371 372 `````` then `````` Guillaume Melquiond committed Jun 14, 2018 373 `````` `valid_up_to s h (i+1)` `````` MARCHE Claude committed Feb 21, 2014 374 `````` `````` Guillaume Melquiond committed Jun 14, 2018 375 ``````then the problem is that one should prove that for each `j` in `0..i-1` : `````` MARCHE Claude committed Feb 21, 2014 376 `````` `````` Guillaume Melquiond committed Jun 14, 2018 377 `````` `valid_column s h j /\ valid_row s h j /\ valid_square s h j` `````` MARCHE Claude committed Feb 21, 2014 378 379 380 `````` this is true but with 2 different possible reasons: `````` Guillaume Melquiond committed Jun 14, 2018 381 382 `````` if `column_start j = column_start i` then `valid_column s h j` is true because `valid_column s h i` is true `````` MARCHE Claude committed Feb 21, 2014 383 `````` else `````` Guillaume Melquiond committed Jun 14, 2018 384 385 `````` `valid_column s h j` is true because `valid_column s g j` is true because `valid_column s h j` does not depend on `h[i]` `````` MARCHE Claude committed Feb 21, 2014 386 387 388 389 390 391 `````` *) lemma valid_unchanged_chunks: `````` MARCHE Claude committed Mar 04, 2014 392 `````` forall g : grid, i1 i2 k:int, start offsets:array int. `````` MARCHE Claude committed Feb 21, 2014 393 394 `````` disjoint_chunks start offsets -> is_index i1 /\ is_index i2 /\ 1 <= k <= 9 -> `````` MARCHE Claude committed Mar 04, 2014 395 396 `````` let s1 = start[i1] in let s2 = start[i2] in `````` MARCHE Claude committed Feb 21, 2014 397 398 399 400 401 `````` let h = Map.set g i1 k in s1 <> s2 /\ valid_chunk g i2 start offsets -> valid_chunk h i2 start offsets lemma valid_changed_chunks: `````` MARCHE Claude committed Mar 04, 2014 402 `````` forall g : grid, i1 i2 k:int, start offsets:array int. `````` MARCHE Claude committed Feb 21, 2014 403 `````` is_index i1 /\ is_index i2 /\ 1 <= k <= 9 -> `````` MARCHE Claude committed Mar 04, 2014 404 405 `````` let s1 = start[i1] in let s2 = start[i2] in `````` MARCHE Claude committed Feb 21, 2014 406 407 408 409 410 `````` let h = Map.set g i1 k in s1 = s2 /\ valid_chunk h i1 start offsets -> valid_chunk h i2 start offsets `````` MARCHE Claude committed May 23, 2017 411 412 413 414 415 416 417 418 419 420 `````` let ghost valid_up_to_change (s:sudoku_chunks) (g:grid) (i x : int) requires { well_formed_sudoku s } requires { is_index i } requires { valid_up_to s g i } requires { 1 <= x <= 9 } requires { valid_column s (Map.set g i x) i } requires { valid_row s (Map.set g i x) i } requires { valid_square s (Map.set g i x) i } ensures { valid_up_to s (Map.set g i x) (i+1) } = () `````` MARCHE Claude committed Feb 21, 2014 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 `````` (** {3 The main solver loop} *) exception SolutionFound let rec solve_aux (s:sudoku_chunks) (g : array int) (i : int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } requires { 0 <= i <= 81 } requires { valid_up_to s g.elts i } requires { full_up_to g.elts i } writes { g } variant { 81 - i } ensures { grid_eq (old g).elts g.elts } ensures { forall h : grid. included g.elts h /\ full h -> not (valid s h) } raises { SolutionFound -> is_solution_for s g.elts (old g).elts } = if i = 81 then raise SolutionFound; (* assert { is_index i }; *) if g[i] <> 0 then try (* assert { 1 <= g[i] <= 9 }; *) check_valid_chunk g i s.column_start s.column_offsets; check_valid_chunk g i s.row_start s.row_offsets; check_valid_chunk g i s.square_start s.square_offsets; solve_aux s g (i + 1) with Invalid -> () end else begin `````` MARCHE Claude committed May 23, 2017 451 `````` let ghost old_g = g.elts in `````` MARCHE Claude committed Feb 21, 2014 452 `````` for k = 1 to 9 do `````` MARCHE Claude committed May 23, 2017 453 `````` invariant { grid_eq old_g (Map.set g.elts i 0) } `````` MARCHE Claude committed Feb 21, 2014 454 455 456 `````` invariant { full_up_to g.elts i } invariant { (* for completeness *) forall k'. 1 <= k' < k -> `````` MARCHE Claude committed May 23, 2017 457 `````` let g' = Map.set old_g i k' in `````` MARCHE Claude committed Feb 21, 2014 458 459 `````` forall h : grid. included g' h /\ full h -> not (valid s h) } g[i] <- k; `````` MARCHE Claude committed May 23, 2017 460 `````` valid_up_to_frame s old_g (Map.set g.elts i 0) i; `````` MARCHE Claude committed Feb 21, 2014 461 462 463 464 `````` try check_valid_chunk g i s.column_start s.column_offsets; check_valid_chunk g i s.row_start s.row_offsets; check_valid_chunk g i s.square_start s.square_offsets; `````` MARCHE Claude committed Mar 04, 2014 465 `````` (* the hard part: see lemma valid_up_to_change *) `````` MARCHE Claude committed May 23, 2017 466 `````` assert { let grid' = Map.set old_g i k in `````` MARCHE Claude committed Mar 04, 2014 467 468 `````` grid_eq grid' g.elts && valid_chunk grid' i s.column_start s.column_offsets && `````` Jean-Christophe Filliatre committed Mar 06, 2014 469 `````` valid_chunk grid' i s.row_start s.row_offsets && `````` MARCHE Claude committed Mar 04, 2014 470 `````` valid_chunk grid' i s.square_start s.square_offsets && `````` Jean-Christophe Filliatre committed Mar 06, 2014 471 `````` valid_up_to s grid' (i+1) }; `````` MARCHE Claude committed May 23, 2017 472 `````` valid_up_to_change s old_g i k; `````` MARCHE Claude committed Feb 21, 2014 473 474 475 `````` solve_aux s g (i + 1) with Invalid -> assert { (* for completeness *) `````` MARCHE Claude committed May 23, 2017 476 `````` not (valid s (Map.set old_g i k)) }; `````` MARCHE Claude committed Feb 21, 2014 477 `````` assert { (* for completeness *) `````` MARCHE Claude committed May 23, 2017 478 `````` let g' = Map.set old_g i k in `````` MARCHE Claude committed Feb 21, 2014 479 480 481 482 483 `````` forall h : grid. included g' h /\ full h -> not (valid s h) } end done; g[i] <- 0; assert { (* for completeness *) `````` MARCHE Claude committed May 23, 2017 484 `````` forall h:grid. included old_g h /\ full h -> `````` MARCHE Claude committed Feb 21, 2014 485 `````` let k' = Map.get h i in `````` MARCHE Claude committed May 23, 2017 486 `````` let g' = Map.set old_g i k' in `````` MARCHE Claude committed Feb 21, 2014 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 `````` included g' h } end exception NoSolution let solve (s:sudoku_chunks) (g : array int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ensures { is_solution_for s g.elts (old g).elts } raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = try solve_aux s g 0; raise NoSolution with SolutionFound -> g end `````` MARCHE Claude committed Jan 12, 2015 507 508 509 510 511 512 513 514 515 516 `````` let check_then_solve (s:sudoku_chunks) (g : array int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ensures { is_solution_for s g.elts (old g).elts } raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = `````` MARCHE Claude committed Jan 13, 2015 517 518 519 520 `````` if check_valid s g then solve s g else raise NoSolution end `````` MARCHE Claude committed May 23, 2017 521 ``````(* Proof in progress `````` MARCHE Claude committed Jan 13, 2015 522 523 524 525 ``````module RandomSolver (* a variant: solve using a random order of cells *) `````` Andrei Paskevich committed Jun 15, 2018 526 527 528 `````` use Grid use array.Array use int.Int `````` MARCHE Claude committed Jan 13, 2015 529 530 `````` use random.Random `````` Andrei Paskevich committed Jun 15, 2018 531 `````` use Solver `````` MARCHE Claude committed Jan 13, 2015 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 `````` let rec solve_aux (s:sudoku_chunks) (randoffset:int) (g : array int) (i : int) requires { well_formed_sudoku s } requires { 0 <= randoffset <= 80 } requires { g.length = 81 } requires { valid_values g.elts } requires { 0 <= i <= 81 } requires { valid_up_to s g.elts i } requires { full_up_to g.elts i } writes { g } variant { 81 - i } ensures { grid_eq (old g).elts g.elts } ensures { forall h : grid. included g.elts h /\ full h -> not (valid s h) } raises { SolutionFound -> is_solution_for s g.elts (old g).elts } = if i = 81 then raise SolutionFound; (* assert { is_index i }; *) let j = i + randoffset in let j = if j >= 81 then j - 81 else j in (* assert { is_index j }; *) if g[j] <> 0 then try (* assert { 1 <= g[j] <= 9 }; *) Solver.check_valid_chunk g j s.column_start s.column_offsets; check_valid_chunk g j s.row_start s.row_offsets; check_valid_chunk g j s.square_start s.square_offsets; solve_aux s randoffset g (i + 1) with Invalid -> () end else begin `````` MARCHE Claude committed Mar 07, 2016 562 `````` label L in `````` MARCHE Claude committed Jan 13, 2015 563 `````` for k = 1 to 9 do `````` MARCHE Claude committed Mar 07, 2016 564 `````` invariant { grid_eq (g at L).elts (Map.set g.elts j 0) } `````` MARCHE Claude committed Jan 13, 2015 565 566 567 `````` invariant { full_up_to g.elts i } (* TODO i -> j *) invariant { (* for completeness *) forall k'. 1 <= k' < k -> `````` MARCHE Claude committed Mar 07, 2016 568 `````` let g' = Map.set (g at L).elts i k' in (* TODO i -> j *) `````` MARCHE Claude committed Jan 13, 2015 569 570 571 572 573 574 575 576 `````` forall h : grid. included g' h /\ full h -> not (valid s h) } g[j] <- k; try check_valid_chunk g j s.column_start s.column_offsets; check_valid_chunk g j s.row_start s.row_offsets; check_valid_chunk g j s.square_start s.square_offsets; (* the hard part: see lemma valid_up_to_change *) (* TODO i -> j *) `````` MARCHE Claude committed Mar 07, 2016 577 `````` assert { let grid' = Map.set (g at L).elts i k in `````` MARCHE Claude committed Jan 13, 2015 578 579 580 581 582 583 584 585 586 `````` grid_eq grid' g.elts && valid_chunk grid' i s.column_start s.column_offsets && valid_chunk grid' i s.row_start s.row_offsets && valid_chunk grid' i s.square_start s.square_offsets && valid_up_to s grid' (i+1) }; assert { valid_up_to s g.elts (i+1) }; solve_aux s randoffset g (i + 1) with Invalid -> assert { (* for completeness *) `````` MARCHE Claude committed Mar 07, 2016 587 `````` not (valid s (Map.set (g at L).elts i k)) }; `````` MARCHE Claude committed Jan 13, 2015 588 `````` assert { (* for completeness *) `````` MARCHE Claude committed Mar 07, 2016 589 `````` let g' = Map.set (g at L).elts i k in `````` MARCHE Claude committed Jan 13, 2015 590 591 592 593 594 `````` forall h : grid. included g' h /\ full h -> not (valid s h) } end done; g[j] <- 0; assert { (* for completeness *) `````` MARCHE Claude committed Mar 07, 2016 595 `````` forall h:grid. included (g at L).elts h /\ full h -> `````` MARCHE Claude committed Jan 13, 2015 596 `````` let k' = Map.get h i in `````` MARCHE Claude committed Mar 07, 2016 597 `````` let g' = Map.set (g at L).elts i k' in `````` MARCHE Claude committed Jan 13, 2015 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 `````` included g' h } end exception NoSolution let solve (s:sudoku_chunks) (g : array int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ensures { is_solution_for s g.elts (old g).elts } raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = try let randoffset = 27 in solve_aux s randoffset g 0; raise NoSolution `````` MARCHE Claude committed Jan 12, 2015 617 618 `````` with SolutionFound -> g end `````` MARCHE Claude committed Jan 13, 2015 619 620 621 622 623 624 625 626 627 628 629 630 `````` let check_then_solve (s:sudoku_chunks) (g : array int) requires { well_formed_sudoku s } requires { g.length = 81 } requires { valid_values g.elts } writes { g } ensures { result = g } ensures { is_solution_for s g.elts (old g).elts } raises { NoSolution -> forall h : grid. included g.elts h /\ full h -> not (valid s h) } = if check_valid s g then solve s g else raise NoSolution `````` MARCHE Claude committed Feb 21, 2014 631 632 `````` end `````` MARCHE Claude committed May 23, 2017 633 ``````*) `````` MARCHE Claude committed Feb 21, 2014 634 635 636 `````` (** {2 Some Tests} *) `````` MARCHE Claude committed Mar 04, 2014 637 `````` `````` MARCHE Claude committed Feb 21, 2014 638 639 ``````module Test `````` Andrei Paskevich committed Jun 15, 2018 640 641 `````` use Grid use TheClassicalSudokuGrid `````` MARCHE Claude committed Feb 21, 2014 642 `````` `````` Andrei Paskevich committed Jun 15, 2018 643 644 645 `````` use Solver use map.Map use array.Array `````` MARCHE Claude committed Feb 21, 2014 646 647 648 649 650 `````` (** Solving the empty grid: easy, yet not trivial *) let test0 () raises { NoSolution -> true } = let a = Array.make 81 0 in `````` MARCHE Claude committed Mar 04, 2014 651 `````` solve (classical_sudoku()) a `````` MARCHE Claude committed Feb 21, 2014 652 653 654 655 656 657 658 659 660 661 662 663 664 ``````(* a possible solution: 1, 2, 3, 4, 5, 6, 7, 8, 9, 4, 5, 6, 7, 8, 9, 1, 2, 3, 7, 8, 9, 1, 2, 3, 4, 5, 6, 2, 1, 4, 3, 6, 5, 8, 9, 7, 3, 6, 5, 8, 9, 7, 2, 1, 4, 8, 9, 7, 2, 1, 4, 3, 6, 5, 5, 3, 1, 6, 4, 2, 9, 7, 8, 6, 4, 2, 9, 7, 8, 5, 3, 1, 9, 7, 8, 5, 3, 1, 6, 4, 2 *) (** A grid known to be solvable *) `````` MARCHE Claude committed Mar 04, 2014 665 ``````(* `````` MARCHE Claude committed Feb 21, 2014 666 667 668 669 670 671 672 673 674 675 676 677 678 679 ``````2 0 9 0 0 0 0 1 0 0 0 0 0 6 0 0 0 0 0 5 3 8 0 2 7 0 0 3 0 0 0 0 0 0 0 0 0 0 0 0 7 5 0 0 3 0 4 1 2 0 8 9 0 0 0 0 4 0 9 0 0 2 0 8 0 0 0 0 1 0 0 5 0 0 0 0 0 0 0 7 6 *) let test1 () raises { NoSolution -> true } = let a = Array.make 81 0 in `````` MARCHE Claude committed Mar 07, 2016 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 `````` a[0] <- 2; a[2] <- 9; a[7] <- 1; a[13] <- 6; a[19] <- 5; a[20] <- 3; a[21] <- 8; a[23] <- 2; a[24] <- 7; a[27] <- 3; a[40] <- 7; a[41] <- 5; a[44] <- 3; a[46] <- 4; a[47] <- 1; a[48] <- 2; a[50] <- 8; a[51] <- 9; a[56] <- 4; a[58] <- 9; a[61] <- 2; a[63] <- 8; a[68] <- 1; a[71] <- 5; a[79] <- 7; a[80] <- 6; assert { valid_values a.Array.elts }; `````` MARCHE Claude committed Mar 04, 2014 707 `````` solve (classical_sudoku()) a `````` MARCHE Claude committed Mar 07, 2016 708 `````` `````` MARCHE Claude committed Feb 21, 2014 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 ``````(* the solution: 2, 6, 9, 3, 5, 7, 8, 1, 4, 1, 8, 7, 9, 6, 4, 5, 3, 2, 4, 5, 3, 8, 1, 2, 7, 6, 9, 3, 7, 5, 6, 4, 9, 2, 8, 1, 9, 2, 8, 1, 7, 5, 6, 4, 3, 6, 4, 1, 2, 3, 8, 9, 5, 7, 7, 1, 4, 5, 9, 6, 3, 2, 8, 8, 3, 6, 7, 2, 1, 4, 9, 5, 5, 9, 2, 4, 8, 3, 1, 7, 6 *) (** A trivially unsolvable grid *) let test2 () raises { NoSolution -> true } = let a = Array.make 81 1 in `````` MARCHE Claude committed Mar 04, 2014 727 `````` solve (classical_sudoku()) a `````` MARCHE Claude committed Feb 21, 2014 728 729 730 731 732 `````` end (*** Local Variables: `````` MARCHE Claude committed Mar 18, 2016 733 ``````compile-command: "why3 ide --extra-config ../share/strategies.conf sudoku.mlw" `````` MARCHE Claude committed Feb 21, 2014 734 735 ``````End: *)``````