-
Notifications
You must be signed in to change notification settings - Fork 0
/
feedback_sudoku.idp
84 lines (69 loc) · 1.7 KB
/
feedback_sudoku.idp
1
2
3
4
5
6
7
8
9
10
11
12
13
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
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
//TODO/ OK
/*
* permentier_sudoku.idp
* Romeo Permentier
* 17/05/2021
*/
vocabulary V {
/* ----- TYPE ----- */
type R isa nat //RIJ
type K isa nat //KOLOM
type G isa nat //GETAL
/* ----- CONSTANTE ----- */
/* ----- RELATIE ----- */
Gegeven(R, K, G)
Vierkant(R, K, R, K)
/* ----- FUNCTIE ----- */
Oplossing(R, K): G
}
structure S : V {
R = {1..9}
K = {1..9}
G = {1..9}
Gegeven = {
1,2,2; 1,4,3;
2,1,7; 2,2,1; 2,6,9; 2,7,3 ;
3,2,3; 3,3,4; 3,4,5; 3,8,7 ;
4,1,9; 4,4,6;
5,2,4; 5,8,6;
6,6,4; 6,9,9;
7,2,8; 7,6,6; 7,7,7; 7,8,4;
8,3,3; 8,4,4; 8,8,5; 8,9,8;
9,6,1; 9,8,9
}
}
theory T : V {
// GEGEVEN GETAL IS OOK EEN OPLOSSING
!r[R], k[K], g[G]: Gegeven(r, k, g) => Oplossing(r, k) = g.
// DEFINITIE VAN 2 VAKJES IN ZELFDE VIERKANT
{
!r1[R],r2[R], k1[K], k2[K]: Vierkant(r1, k1, r2, k2) <-
// RELATIE GELDT NIET VOOR EEN VAKJE MET ZICHZELF
~(r1 = r2 & k1 = k2)
&
/*
FORMULA y(x) "x - (x-1)%3 = y"
y(1)=y(2)=y(3)=1
y(4)=y(5)=y(6)=4
y(7)=y(8)=y(9)=7
*/
r1 - (r1-1)%3 = r2 - (r2-1)%3
&
k1 - (k1-1)%3 = k2 - (k2-1)%3.
}
// GEEN DUBBELE WAARDEN IN ...
!r1[R],r2[R], k1[K], k2[K]:
// ... EEN VIERKANT
Vierkant(r1, k1, r2, k2)
|
// ... EEN RIJ
(r1=r2 & k1~=k2)
|
// ... EEN KOLOM
(r1~=r2 & k1=k2)
=> Oplossing(r1, k1) ~= Oplossing(r2, k2).
}
procedure main() {
stdoptions.nbmodels = 0
printmodels(modelexpand(T,S))
}