From 780a143898a5fb25a8eebaec3976bd70e3084e93 Mon Sep 17 00:00:00 2001
From: Michael Leuschel <leuschel@uni-duesseldorf.de>
Date: Thu, 1 Jul 2021 11:10:06 +0200
Subject: [PATCH] add two more puzzles
---
Sudoku/SudokuEvent.mch | 33 ++++++++++++++++++++++++++++++++-
1 file changed, 32 insertions(+), 1 deletion(-)
diff --git a/Sudoku/SudokuEvent.mch b/Sudoku/SudokuEvent.mch
index 27283a9..cefcf11 100644
--- a/Sudoku/SudokuEvent.mch
+++ b/Sudoku/SudokuEvent.mch
@@ -44,6 +44,36 @@ DEFINITIONS
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
+ );
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)})
@@ -53,7 +83,8 @@ CONSTANTS
conflict_pos_sym /*@desc "symmetry-reduced version of conflict_pos" */,
PuzzleBoard /*@desc "Stored Puzzle" */
PROPERTIES
- PuzzleBoard : DOM --> (DOM +-> RAN) & PUZZLE(PuzzleBoard) &
+ PuzzleBoard : DOM --> (DOM +-> RAN) &
+ PUZZLE(PuzzleBoard) &
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) &
--
GitLab