-
Notifications
You must be signed in to change notification settings - Fork 0
/
main.py
153 lines (141 loc) · 3.66 KB
/
main.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
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
from z3 import *
#from z3 import *
#s = Optimize()
#x = Int('x')
#y = Int('y')
#z = Int('z')
#a = Bool('a')
#b = Bool('b')
#c = Bool('c')
#c = Bool('d')
#a = (x+y+z == 1)
#b = (x+y+z == 2)
#c = (x+y+z == 3)
#d = (x+y+z == 4)
##our threshold k
#k=2
#s.add(z3.PbGe([(a,1),(b,1),(c,1),(d,1)], k))
#print(s.check())
#print(s.model())
x0 = Real('x0')
x1 = Real('x1')
x2 = Real('x2')
x3 = Real('x3')
x4 = Real('x4')
x5 = Real('x5')
x6 = Real('x6')
x7 = Real('x7')
x8 = Real('x8')
x9 = Real('x9')
b0 = Bool('b0')
b1 = Bool('b1')
b2 = Bool('b2')
b3 = Bool('b3')
b4 = Bool('b4')
b5 = Bool('b5')
b6 = Bool('b6')
b7 = Bool('b7')
b8 = Bool('b8')
b9 = Bool('b9')
b10 = Bool('b10')
b11 = Bool('b11')
b12 = Bool('b12')
b13 = Bool('b13')
b14 = Bool('b14')
b15 = Bool('b15')
b16 = Bool('b16')
b17 = Bool('b17')
b18 = Bool('b18')
b19 = Bool('b19')
s = Optimize()
#b0 = (6*x0+10*x1+11*x2+3*x3==17)
#b1 = (10*x0+1*x1+8*x2+7*x3==8)
#b2 = (4*x0+3*x1+14*x2+2*x3==17)
#b3 = (15*x0+2*x1+11*x2+2*x3==0)
#b4 = (5*x0+15*x1+10*x2+3*x3==0)
#b5 = (14*x0+5*x1+17*x2+9*x3==0)
#b6 = (17*x0+5*x1+13*x2+14*x3==0)
#b7 = (16*x0+2*x1+5*x2+17*x3==0)
b0 = (98*x0+1*x1+37*x2+93*x3+6*x4+33*x5+91*x6+29*x7+37*x8+38*x9==94)
b1 = (6*x0+93*x1+90*x2+51*x3+30*x4+33*x5+94*x6+98*x7+19*x8+35*x9==91)
b2 = (36*x0+16*x1+63*x2+55*x3+69*x4+86*x5+96*x6+58*x7+74*x8+84*x9==85)
b3 = (61*x0+79*x1+76*x2+0*x3+51*x4+73*x5+10*x6+81*x7+8*x8+52*x9==39)
b4 = (16*x0+82*x1+23*x2+40*x3+48*x4+30*x5+101*x6+62*x7+66*x8+59*x9==32)
b5 = (33*x0+83*x1+23*x2+64*x3+12*x4+45*x5+93*x6+39*x7+25*x8+89*x9==39)
b6 = (40*x0+28*x1+97*x2+16*x3+76*x4+71*x5+6*x6+21*x7+87*x8+7*x9==100)
b7 = (68*x0+34*x1+14*x2+94*x3+75*x4+85*x5+0*x6+1*x7+29*x8+5*x9==50)
b8 = (58*x0+57*x1+81*x2+73*x3+68*x4+46*x5+65*x6+54*x7+83*x8+49*x9==57)
b9 = (37*x0+74*x1+0*x2+1*x3+98*x4+88*x5+65*x6+82*x7+25*x8+4*x9==0)
b10 = (65*x0+53*x1+88*x2+81*x3+33*x4+56*x5+53*x6+84*x7+37*x8+93*x9==0)
b11 = (99*x0+25*x1+55*x2+53*x3+32*x4+48*x5+77*x6+80*x7+91*x8+54*x9==0)
b12 = (32*x0+98*x1+10*x2+91*x3+2*x4+34*x5+87*x6+0*x7+30*x8+43*x9==0)
b13 = (83*x0+24*x1+1*x2+60*x3+66*x4+3*x5+57*x6+29*x7+71*x8+81*x9==0)
b14 = (52*x0+13*x1+90*x2+77*x3+101*x4+97*x5+63*x6+101*x7+69*x8+87*x9==0)
b15 = (5*x0+74*x1+90*x2+81*x3+64*x4+5*x5+95*x6+87*x7+12*x8+32*x9==0)
b16 = (46*x0+16*x1+80*x2+53*x3+94*x4+33*x5+70*x6+88*x7+37*x8+21*x9==0)
b17 = (34*x0+81*x1+54*x2+49*x3+26*x4+6*x5+51*x6+17*x7+61*x8+14*x9==0)
b18 = (17*x0+53*x1+25*x2+81*x3+97*x4+99*x5+97*x6+33*x7+41*x8+8*x9==0)
b19 = (80*x0+28*x1+23*x2+24*x3+29*x4+48*x5+42*x6+11*x7+62*x8+14*x9==0)
s.add_soft(b0)
s.add_soft(b1)
s.add_soft(b2)
s.add_soft(b3)
s.add_soft(b4)
s.add_soft(b5)
s.add_soft(b6)
s.add_soft(b7)
s.add_soft(b8)
s.add_soft(b9)
s.add_soft(b10)
s.add_soft(b11)
s.add_soft(b12)
s.add_soft(b13)
s.add_soft(b14)
s.add_soft(b15)
s.add_soft(b16)
s.add_soft(b17)
s.add_soft(b18)
s.add_soft(b19)
print(s.check())
print(s.model())
m = s.model()
c0 = m.evaluate(b0)
c1 = m.evaluate(b1)
c2 = m.evaluate(b2)
c3 = m.evaluate(b3)
c4 = m.evaluate(b4)
c5 = m.evaluate(b5)
c6 = m.evaluate(b6)
c7 = m.evaluate(b7)
c8 = m.evaluate(b8)
c9 = m.evaluate(b9)
c10 = m.evaluate(b10)
c11 = m.evaluate(b11)
c12 = m.evaluate(b12)
c13 = m.evaluate(b13)
c14 = m.evaluate(b14)
c15 = m.evaluate(b15)
c16 = m.evaluate(b16)
c17 = m.evaluate(b17)
c18 = m.evaluate(b18)
c19 = m.evaluate(b19)
print(f'c0 = {c0}')
print(f'c1 = {c1}')
print(f'c2 = {c2}')
print(f'c3 = {c3}')
print(f'c4 = {c4}')
print(f'c5 = {c5}')
print(f'c6 = {c6}')
print(f'c7 = {c7}')
print(f'c8 = {c8}')
print(f'c9 = {c9}')
print(f'c10 = {c10}')
print(f'c11 = {c11}')
print(f'c12 = {c12}')
print(f'c13 = {c13}')
print(f'c14 = {c14}')
print(f'c15 = {c15}')
print(f'c16 = {c16}')
print(f'c17 = {c17}')
print(f'c18 = {c18}')
print(f'c19 = {c19}')