-
Notifications
You must be signed in to change notification settings - Fork 0
/
6queens.smt
84 lines (79 loc) · 6.49 KB
/
6queens.smt
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
;constantes
(declare-const q0_0 Bool)
(declare-const q0_1 Bool)
(declare-const q0_2 Bool)
(declare-const q0_3 Bool)
(declare-const q0_4 Bool)
(declare-const q0_5 Bool)
(declare-const q1_0 Bool)
(declare-const q1_1 Bool)
(declare-const q1_2 Bool)
(declare-const q1_3 Bool)
(declare-const q1_4 Bool)
(declare-const q1_5 Bool)
(declare-const q2_0 Bool)
(declare-const q2_1 Bool)
(declare-const q2_2 Bool)
(declare-const q2_3 Bool)
(declare-const q2_4 Bool)
(declare-const q2_5 Bool)
(declare-const q3_0 Bool)
(declare-const q3_1 Bool)
(declare-const q3_2 Bool)
(declare-const q3_3 Bool)
(declare-const q3_4 Bool)
(declare-const q3_5 Bool)
(declare-const q4_0 Bool)
(declare-const q4_1 Bool)
(declare-const q4_2 Bool)
(declare-const q4_3 Bool)
(declare-const q4_4 Bool)
(declare-const q4_5 Bool)
(declare-const q5_0 Bool)
(declare-const q5_1 Bool)
(declare-const q5_2 Bool)
(declare-const q5_3 Bool)
(declare-const q5_4 Bool)
(declare-const q5_5 Bool)
;cada linha possui ao menos uma rainha
(assert (or q0_0 q0_1 q0_2 q0_3 q0_4 q0_5))
(assert (or q1_0 q1_1 q1_2 q1_3 q1_4 q1_5))
(assert (or q2_0 q2_1 q2_2 q2_3 q2_4 q2_5))
(assert (or q3_0 q3_1 q3_2 q3_3 q3_4 q3_5))
(assert (or q4_0 q4_1 q4_2 q4_3 q4_4 q4_5))
(assert (or q5_0 q5_1 q5_2 q5_3 q5_4 q5_5))
;cada linha possui no máximo uma rainha
(assert (not (or (and q0_0 q0_1) (and q0_0 q0_2) (and q0_0 q0_3) (and q0_0 q0_4) (and q0_0 q0_5) (and q0_1 q0_2) (and q0_1 q0_3) (and q0_1 q0_4) (and q0_1 q0_5) (and q0_2 q0_3) (and q0_2 q0_4) (and q0_2 q0_5) (and q0_3 q0_4) (and q0_3 q0_5) (and q0_4 q0_5))))
(assert (not (or (and q1_0 q1_1) (and q1_0 q1_2) (and q1_0 q1_3) (and q1_0 q1_4) (and q1_0 q1_5) (and q1_1 q1_2) (and q1_1 q1_3) (and q1_1 q1_4) (and q1_1 q1_5) (and q1_2 q1_3) (and q1_2 q1_4) (and q1_2 q1_5) (and q1_3 q1_4) (and q1_3 q1_5) (and q1_4 q1_5))))
(assert (not (or (and q2_0 q2_1) (and q2_0 q2_2) (and q2_0 q2_3) (and q2_0 q2_4) (and q2_0 q2_5) (and q2_1 q2_2) (and q2_1 q2_3) (and q2_1 q2_4) (and q2_1 q2_5) (and q2_2 q2_3) (and q2_2 q2_4) (and q2_2 q2_5) (and q2_3 q2_4) (and q2_3 q2_5) (and q2_4 q2_5))))
(assert (not (or (and q3_0 q3_1) (and q3_0 q3_2) (and q3_0 q3_3) (and q3_0 q3_4) (and q3_0 q3_5) (and q3_1 q3_2) (and q3_1 q3_3) (and q3_1 q3_4) (and q3_1 q3_5) (and q3_2 q3_3) (and q3_2 q3_4) (and q3_2 q3_5) (and q3_3 q3_4) (and q3_3 q3_5) (and q3_4 q3_5))))
(assert (not (or (and q4_0 q4_1) (and q4_0 q4_2) (and q4_0 q4_3) (and q4_0 q4_4) (and q4_0 q4_5) (and q4_1 q4_2) (and q4_1 q4_3) (and q4_1 q4_4) (and q4_1 q4_5) (and q4_2 q4_3) (and q4_2 q4_4) (and q4_2 q4_5) (and q4_3 q4_4) (and q4_3 q4_5) (and q4_4 q4_5))))
(assert (not (or (and q5_0 q5_1) (and q5_0 q5_2) (and q5_0 q5_3) (and q5_0 q5_4) (and q5_0 q5_5) (and q5_1 q5_2) (and q5_1 q5_3) (and q5_1 q5_4) (and q5_1 q5_5) (and q5_2 q5_3) (and q5_2 q5_4) (and q5_2 q5_5) (and q5_3 q5_4) (and q5_3 q5_5) (and q5_4 q5_5))))
;cada coluna possui no máximo uma rainha
(assert (not (or (and q0_0 q1_0) (and q0_0 q2_0) (and q0_0 q3_0) (and q0_0 q4_0) (and q0_0 q5_0) (and q1_0 q2_0) (and q1_0 q3_0) (and q1_0 q4_0) (and q1_0 q5_0) (and q2_0 q3_0) (and q2_0 q4_0) (and q2_0 q5_0) (and q3_0 q4_0) (and q3_0 q5_0) (and q4_0 q5_0))))
(assert (not (or (and q0_1 q1_1) (and q0_1 q2_1) (and q0_1 q3_1) (and q0_1 q4_1) (and q0_1 q5_1) (and q1_1 q2_1) (and q1_1 q3_1) (and q1_1 q4_1) (and q1_1 q5_1) (and q2_1 q3_1) (and q2_1 q4_1) (and q2_1 q5_1) (and q3_1 q4_1) (and q3_1 q5_1) (and q4_1 q5_1))))
(assert (not (or (and q0_2 q1_2) (and q0_2 q2_2) (and q0_2 q3_2) (and q0_2 q4_2) (and q0_2 q5_2) (and q1_2 q2_2) (and q1_2 q3_2) (and q1_2 q4_2) (and q1_2 q5_2) (and q2_2 q3_2) (and q2_2 q4_2) (and q2_2 q5_2) (and q3_2 q4_2) (and q3_2 q5_2) (and q4_2 q5_2))))
(assert (not (or (and q0_3 q1_3) (and q0_3 q2_3) (and q0_3 q3_3) (and q0_3 q4_3) (and q0_3 q5_3) (and q1_3 q2_3) (and q1_3 q3_3) (and q1_3 q4_3) (and q1_3 q5_3) (and q2_3 q3_3) (and q2_3 q4_3) (and q2_3 q5_3) (and q3_3 q4_3) (and q3_3 q5_3) (and q4_3 q5_3))))
(assert (not (or (and q0_4 q1_4) (and q0_4 q2_4) (and q0_4 q3_4) (and q0_4 q4_4) (and q0_4 q5_4) (and q1_4 q2_4) (and q1_4 q3_4) (and q1_4 q4_4) (and q1_4 q5_4) (and q2_4 q3_4) (and q2_4 q4_4) (and q2_4 q5_4) (and q3_4 q4_4) (and q3_4 q5_4) (and q4_4 q5_4))))
(assert (not (or (and q0_5 q1_5) (and q0_5 q2_5) (and q0_5 q3_5) (and q0_5 q4_5) (and q0_5 q5_5) (and q1_5 q2_5) (and q1_5 q3_5) (and q1_5 q4_5) (and q1_5 q5_5) (and q2_5 q3_5) (and q2_5 q4_5) (and q2_5 q5_5) (and q3_5 q4_5) (and q3_5 q5_5) (and q4_5 q5_5))))
;cada diagonal possui no máximo uma rainha
(assert (not (or (and q0_4 q1_5))))
(assert (not (or (and q0_3 q1_4) (and q0_3 q2_5) (and q1_4 q2_5))))
(assert (not (or (and q0_2 q1_3) (and q0_2 q2_4) (and q0_2 q3_5) (and q1_3 q2_4) (and q1_3 q3_5) (and q2_4 q3_5))))
(assert (not (or (and q0_1 q1_2) (and q0_1 q2_3) (and q0_1 q3_4) (and q0_1 q4_5) (and q1_2 q2_3) (and q1_2 q3_4) (and q1_2 q4_5) (and q2_3 q3_4) (and q2_3 q4_5) (and q3_4 q4_5))))
(assert (not (or (and q0_0 q1_1) (and q0_0 q2_2) (and q0_0 q3_3) (and q0_0 q4_4) (and q0_0 q5_5) (and q1_1 q2_2) (and q1_1 q3_3) (and q1_1 q4_4) (and q1_1 q5_5) (and q2_2 q3_3) (and q2_2 q4_4) (and q2_2 q5_5) (and q3_3 q4_4) (and q3_3 q5_5) (and q4_4 q5_5))))
(assert (not (or (and q1_0 q2_1) (and q1_0 q3_2) (and q1_0 q4_3) (and q1_0 q5_4) (and q2_1 q3_2) (and q2_1 q4_3) (and q2_1 q5_4) (and q3_2 q4_3) (and q3_2 q5_4) (and q4_3 q5_4))))
(assert (not (or (and q2_0 q3_1) (and q2_0 q4_2) (and q2_0 q5_3) (and q3_1 q4_2) (and q3_1 q5_3) (and q4_2 q5_3))))
(assert (not (or (and q3_0 q4_1) (and q3_0 q5_2) (and q4_1 q5_2))))
(assert (not (or (and q4_0 q5_1))))
(assert (not (or (and q0_1 q1_0))))
(assert (not (or (and q0_2 q1_1) (and q0_2 q2_0) (and q1_1 q2_0))))
(assert (not (or (and q0_3 q1_2) (and q0_3 q2_1) (and q0_3 q3_0) (and q1_2 q2_1) (and q1_2 q3_0) (and q2_1 q3_0))))
(assert (not (or (and q0_4 q1_3) (and q0_4 q2_2) (and q0_4 q3_1) (and q0_4 q4_0) (and q1_3 q2_2) (and q1_3 q3_1) (and q1_3 q4_0) (and q2_2 q3_1) (and q2_2 q4_0) (and q3_1 q4_0))))
(assert (not (or (and q0_5 q1_4) (and q0_5 q2_3) (and q0_5 q3_2) (and q0_5 q4_1) (and q0_5 q5_0) (and q1_4 q2_3) (and q1_4 q3_2) (and q1_4 q4_1) (and q1_4 q5_0) (and q2_3 q3_2) (and q2_3 q4_1) (and q2_3 q5_0) (and q3_2 q4_1) (and q3_2 q5_0) (and q4_1 q5_0))))
(assert (not (or (and q1_5 q2_4) (and q1_5 q3_3) (and q1_5 q4_2) (and q1_5 q5_1) (and q2_4 q3_3) (and q2_4 q4_2) (and q2_4 q5_1) (and q3_3 q4_2) (and q3_3 q5_1) (and q4_2 q5_1))))
(assert (not (or (and q2_5 q3_4) (and q2_5 q4_3) (and q2_5 q5_2) (and q3_4 q4_3) (and q3_4 q5_2) (and q4_3 q5_2))))
(assert (not (or (and q3_5 q4_4) (and q3_5 q5_3) (and q4_4 q5_3))))
(assert (not (or (and q4_5 q5_4))))
(check-sat)
(get-model)