-
Notifications
You must be signed in to change notification settings - Fork 0
/
example.py
executable file
·113 lines (70 loc) · 2.2 KB
/
example.py
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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
import clingo
import itertools
import numpy as np
import math
asp_code = ""
n = 2
m = 4
u = 3
# asp_code = """#const n={}.
# #const m={}.
# #const u={}.
# """.format(n, m, u)
# asp_code += """n { item(1..u) } m.
# """
# asp_code += """given_item(1..u).
# not_item(I):- not item(I), given_item(I).
# item(I):- not not_item(I), given_item(I).
# ctr(I, K+1):- ctr(I-1, K), item(I).
# ctr(I, K):- ctr(I-1, K), not_item(I).
# :- ctr(u, K), K > m.
# :- ctr(u, K), K < n.
# ctr(0, 0).
# """
###################################
asp_code += """binary(1..1000).
1{ choice(X): binary(X)}1.
#show choice/1.\n
"""
print(asp_code)
control = clingo.Control()
control.add("base", [], asp_code)
control.ground([("base", [])])
def on_model(model):
print(model.symbols(shown=True))
control.configuration.solve.models = 0;
answer = control.solve(on_model=on_model)
if answer.satisfiable:
print("satisfiable:")
else:
print("unsatisfiable")
################################
# asp_code += """b.
# item(1..u) :- b.
# c :- d, not e.
# d:- ctrl(1, n).
# e:- ctru(1, m+1).
# :- b, not c.
# """
# asp_code += """ctrl(I, 1) :- item(I), I >= n, I <= u.
# """
# asp_code += """ctrl(I, 1) :- not item(I-u), I >= (max(n, u+1)), I <= u+v."""
# asp_code += """ctrl(I, K) :- ctrl(I, K-1), item(I), K > 1, K <= n, I >= n-I+1, I <= u.
# """
# asp_code += """ctrl(I, K) :- ctrl(I+1, K), not item(I), K > 1, K <= n, I >= n-I+1, I <= u.
# """
# asp_code += """ctrl(I, K) :- ctrl(I, K-1), not item(I-u), K > 1, K <= n, I >= max(n, u+1), I <= u+v-K+1.
# """
# asp_code += """ctrl(I, K) :- ctrl(I+1, K), not not item(I-u), K > 1, K <= n, I >= max(n, u+1), I < u+v-I+1.
# """
# asp_code += """ctru(J, 1) :- item(J), J >= m, J <= u.
# """
# asp_code += """ctru(J, 1) :- not item(J-u), J >= (max(m, u+1)), J <= u+v."""
# asp_code += """ctru(J, K) :- ctru(J, K-1), item(J), K > 1, K <= m, J >= n-J+1, J <= u.
# """
# asp_code += """ctru(J, K) :- ctru(J+1, K), not item(J), K > 1, K <= m, J >= m-J+1, J <= u.
# """
# asp_code += """ctru(J, K) :- ctru(J, K-1), not item(J-u), K > 1, K <= m, J >= max(m, u+1), J <= u+v-K+1.
# """
# asp_code += """ctru(J, K) :- ctru(J+1, K), not not item(J-u), K > 1, K <= m, J >= max(m, J+1), J < u+v-J+1.
# """