-
Notifications
You must be signed in to change notification settings - Fork 2
/
nuesslein2.py
70 lines (60 loc) · 2.54 KB
/
nuesslein2.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
import utils
import numpy as np
class nuesslein2:
def __init__(self, formula, V):
# sort the formula (i.e. all negative literals are at the back of the clause)
self.formula = [sorted(c, reverse=True) for c in formula]
self.V = V
self.Q = {}
# new values are added to the QUBO-Matrix Q via this monitor
def add(self, x, y, value):
x = np.abs(x) - 1
y = np.abs(y) - 1
if x > y:
x,y = y,x
if (x,y) in self.Q.keys():
self.Q[(x,y)] += value
else:
self.Q[(x,y)] = value
# this function creates the QUBO-Matrix Q
def fillQ(self):
for i, c in enumerate(self.formula):
if list(np.sign(c)) == [1, 1, 1]:
self.add(c[0], c[1], 2)
self.add(c[0], self.V + i + 1, -2)
self.add(c[1], self.V + i + 1, -2)
self.add(c[2], c[2], -1)
self.add(c[2], self.V + i + 1, 1)
self.add(self.V + i + 1, self.V + i + 1, 1)
elif list(np.sign(c)) == [1, 1, -1]:
self.add(c[0], c[1], 2)
self.add(c[0], self.V + i + 1, -2)
self.add(c[1], self.V + i + 1, -2)
self.add(c[2], c[2], 1)
self.add(c[2], self.V + i + 1, -1)
self.add(self.V + i + 1, self.V + i + 1, 2)
elif list(np.sign(c)) == [1, -1, -1]:
self.add(c[0], c[0], 2)
self.add(c[0], c[1], -2)
self.add(c[0], self.V + i + 1, -2)
self.add(c[1], self.V + i + 1, 2)
self.add(c[2], c[2], 1)
self.add(c[2], self.V + i + 1, -1)
else:
self.add(c[0], c[0], -1)
self.add(c[0], c[1], 1)
self.add(c[0], c[2], 1)
self.add(c[0], self.V + i + 1, 1)
self.add(c[1], c[1], -1)
self.add(c[1], c[2], 1)
self.add(c[1], self.V + i + 1, 1)
self.add(c[2], c[2], -1)
self.add(c[2], self.V + i + 1, 1)
self.add(self.V + i + 1, self.V + i + 1, -1)
# this function starts creating Q, solving it and interpreting the solution
# (e.g. deciding whether the formula is satisfiable or not)
def solve(self):
self.fillQ()
answer = utils.solve_with_qbsolv(self.Q)
assignment = [answer[i] for i in range(self.V)]
return utils.check_solution(self.formula, assignment)