encode puzzles more constructively

to avoid additional solutions in setup constants

Sudoku/SudokuEvent.mch

@@ -29,51 +29,35 @@ DEFINITIONS
  MAX_OPERATIONS_SetBoard == 10;
 
     /* PUZZLE CONSTRAINTS : */
- PUZZLE(BOARD) == (
+ PUZZLE1 == 
+ {(1↦{(1↦7),(2↦8),(3↦1),(4↦6),(6↦2),(7↦9),(9↦5)}),
+  (2↦{(1↦9),(3↦2),(4↦7),(5↦1)}),
+  (3↦{(3↦6),(4↦8),(8↦1),(9↦2)}),
+  (4↦{(1↦2),(4↦3),(7↦8),(8↦5),(9↦1)}),
+  (5↦{(2↦7),(3↦3),(4↦5),(9↦4)}),(6↦{(3↦8),(6↦9),(7↦3),(8↦6)}),
+  (7↦{(1↦1),(2↦9),(6↦7),(8↦8)}),
+  (8↦{(1↦8),(2↦6),(3↦7),(6↦3),(7↦4),(9↦9)}),
+  (9↦{(3↦5),(7↦1)})}
+  ;
+  PUZZLE2 == 
+ {(1↦{(1↦1),(2↦3),(4↦8),(5↦6),(6↦5),(9↦9)}),
+  (2↦{(3↦8),(6↦4),(7↦1),(9↦2)}),
+  (3↦{(4↦1),(5↦2)}),
+  (4↦{(3↦7),(4↦6),(7↦9),(9↦3)}),
+  (5↦{(1↦9),(2↦1),(3↦5),(4↦4),(8↦8),(9↦7)}),
+  (6↦{(1↦6),(3↦3),(5↦1),(6↦7),(8↦5)}),
+  (7↦{(7↦3),(8↦4),(9↦5)}),
+  (8↦{(3↦6),(4↦7),(6↦3),(7↦8),(8↦9)}),
+  (9↦{(3↦9),(5↦8),(9↦6)})};
 
-   BOARD(1)(1)=7 & BOARD(1)(2)=8 & BOARD(1)(3)=1 & BOARD(1)(4)=6 & BOARD(1)(6)=2
-                 & BOARD(1)(7)=9 & BOARD(1)(9)=5 &
-   BOARD(2)(1)=9 & BOARD(2)(3)=2 & BOARD(2)(4)=7 & BOARD(2)(5)=1 &
-   BOARD(3)(3)=6 & BOARD(3)(4)=8 & BOARD(3)(8)=1 & BOARD(3)(9)=2 &
-
-   BOARD(4)(1)=2 & BOARD(4)(4)=3 & BOARD(4)(7)=8 & BOARD(4)(8)=5 & BOARD(4)(9)=1 &
-   BOARD(5)(2)=7 & BOARD(5)(3)=3 & BOARD(5)(4)=5 & BOARD(5)(9)=4 &
-   BOARD(6)(3)=8 & BOARD(6)(6)=9 & BOARD(6)(7)=3 & BOARD(6)(8)=6 &
-
-   BOARD(7)(1)=1 & BOARD(7)(2)=9 & BOARD(7)(6)=7 & BOARD(7)(8)=8 &
-   BOARD(8)(1)=8 & BOARD(8)(2)=6 & BOARD(8)(3)=7 & BOARD(8)(6)=3 & BOARD(8)(7)=4 & BOARD(8)(9)=9 &
-   BOARD(9)(3)=5 & BOARD(9)(7)=1
-  );
-  PUZZLE2(BOARD) == (
-
-   BOARD(1)(1)=1 & BOARD(1)(2)=3 & BOARD(1)(4)=8 & BOARD(1)(5)=6 & BOARD(1)(6)=5
-                 & BOARD(1)(9)=9 &
-   BOARD(2)(3)=8 & BOARD(2)(6)=4 & BOARD(2)(7)=1 & BOARD(2)(9)=2 &
-   BOARD(3)(4)=1 & BOARD(3)(5)=2 &
-
-   BOARD(4)(3)=7 & BOARD(4)(4)=6 & BOARD(4)(7)=9 & BOARD(4)(9)=3 &
-   BOARD(5)(1)=9 & BOARD(5)(2)=1 & BOARD(5)(3)=5 & BOARD(5)(4)=4 
-                 & BOARD(5)(8)=8 & BOARD(5)(9)=7 &           
-   BOARD(6)(1)=6 & BOARD(6)(3)=3 & BOARD(6)(5)=1 & BOARD(6)(6)=7 & BOARD(6)(8)=5 &
-
-   BOARD(7)(7)=3 & BOARD(7)(8)=4 & BOARD(7)(9)=5 &
-   BOARD(8)(3)=6 & BOARD(8)(4)=7 & BOARD(8)(6)=3 & BOARD(8)(7)=8 & BOARD(8)(8)=9 &
-   BOARD(9)(3)=9 & BOARD(9)(5)=8 & BOARD(9)(9)=6
-  );
-
- PUZZLE3(BOARD) == (
-   BOARD(1)(2)=4 & BOARD(1)(3)=3 & BOARD(1)(6)=5 & BOARD(1)(8)=8 & BOARD(1)(9)=7 &
-   BOARD(2)(2)=9 & BOARD(2)(6)=3 & 
-   BOARD(3)(5)=2 & BOARD(3)(8)=1 &
-
-   BOARD(4)(3)=9 & BOARD(4)(4)=8 & BOARD(4)(9)=5 & 
-   BOARD(5)(2)=5 & BOARD(5)(3)=8 & BOARD(5)(8)=2 & BOARD(5)(9)=6 &            
-   BOARD(6)(2)=7 & BOARD(6)(4)=2 & 
-
-   BOARD(7)(1)=5 & BOARD(7)(2)=8 & BOARD(7)(4)=1 & BOARD(7)(6)=2 & BOARD(7)(7)=4 & BOARD (7)(8)=7 &
-   BOARD(8)(9)=3 &
-   BOARD(9)(1)=9 & BOARD(9)(2)=1 & BOARD(9)(4)=7 & BOARD(9)(5)=6 & BOARD(9)(7)=5
-  );
+ PUZZLE3 == 
+ {(1↦{(2↦4),(3↦3),(6↦5),(8↦8),(9↦7)}),
+  (2↦{(2↦9),(6↦3)}),(3↦{(5↦2),(8↦1)}),(4↦{(3↦9),(4↦8),(9↦5)}),
+  (5↦{(2↦5),(3↦8),(8↦2),(9↦6)}),
+  (6↦{(2↦7),(4↦2)}),
+  (7↦{(1↦5),(2↦8),(4↦1),(6↦2),(7↦4),(8↦7)}),
+  (8↦{(9↦3)}),(9↦{(1↦9),(2↦1),(4↦7),(5↦6),(7↦5)})}
+  ;
 
   UnassignedPosition(x,y) == x:DOM & y:DOM & not(y:dom(Board(x)));
   PossibleVals(cx,cy) == DOM \ ran({x,y,r| x|->y : conflict_pos(cx,cy) & y:dom(Board(x)) & r=Board(x)(y)})
@@ -84,7 +68,7 @@ CONSTANTS
   PuzzleBoard /*@desc "Stored Puzzle" */
 PROPERTIES
   PuzzleBoard : DOM --> (DOM +-> RAN) & 
-  PUZZLE(PuzzleBoard) &
+  PuzzleBoard : {PUZZLE1,PUZZLE2,PUZZLE3} &
   get_square = %x.(x:DOM | 1 + (x-1)/3) /*@desc "Get square (1,2,3) for a coordinate 1..9" */
   &
   conflict_pos = %(x,y).(x:DOM & y:DOM | {x2,y2 | x2:DOM & y2:DOM &  (x,y) /= (x2,y2) &