-
Notifications
You must be signed in to change notification settings - Fork 22
/
rosalind_2sat.py
127 lines (115 loc) · 4.05 KB
/
rosalind_2sat.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
# ^_^ coding ^_^
"""
2-Satisfiability
http://rosalind.info/problems/2sat/
Given: A positive integer k≤20 and k 2SAT formulas represented as follows. The first line gives the number of variables n≤103 and the number of clauses m≤104, each of the following m lines gives a clause of length 2 by specifying two different literals: e.g., a clause (x3∨x¯¯¯5) is given by 3 -5.
Return: For each formula, output 0 if it cannot be satisfied or 1 followed by a satisfying assignment otherwise.
"""
# the input:
# ==============================
data = "../data/rosalind_2sat.txt"
graphs = []
graphs_t = []
variables = []
clauses = []
with open(data, "r") as f:
k = int(f.readline().strip())
for line in f:
if line.strip():
a, b = map(int, line.strip().split(" "))
if a>0 and b>0:
# graph[2*abs(a)-2].append(2*abs(b)-1)
graph[2*abs(a)-1].append(2*abs(b)-2) #a-, b
graph[2*abs(b)-1].append(2*abs(a)-2) #b-, a
# graph[2*abs(b)-2].append(2*abs(a)-1)
graph_t[2*abs(b)-2].append(2*abs(a)-1)
graph_t[2*abs(a)-2].append(2*abs(b)-1)
elif a<0 and b>0:
# graph[2*abs(a)-1].append(2*abs(b)-1)
graph[2*abs(a)-2].append(2*abs(b)-2) #a-, b
graph[2*abs(b)-1].append(2*abs(a)-1) #b-, a
# graph[2*abs(b)-2].append(2*abs(a)-2)
graph_t[2*abs(b)-2].append(2*abs(a)-2)
graph_t[2*abs(a)-1].append(2*abs(b)-1)
elif a>0 and b<0:
# graph[2*abs(a)-2].append(2*abs(b)-2)
graph[2*abs(a)-1].append(2*abs(b)-1) #a-, b
graph[2*abs(b)-2].append(2*abs(a)-2) #b-, a
# graph[2*abs(b)-1].append(2*abs(a)-1)
graph_t[2*abs(b)-1].append(2*abs(a)-1)
graph_t[2*abs(a)-2].append(2*abs(b)-2)
else:
# graph[2*abs(a)-1].append(2*abs(b)-2)
graph[2*abs(a)-2].append(2*abs(b)-1) #a-, b
graph[2*abs(b)-2].append(2*abs(a)-1) #b-, a
# graph[2*abs(b)-1].append(2*abs(a)-2)
graph_t[2*abs(b)-1].append(2*abs(a)-2)
graph_t[2*abs(a)-1].append(2*abs(b)-2)
else:
variable, clause = map(int, f.readline().strip().split(" "))
variables.append(variable)
clauses.append(clause)
graph = {v:[] for v in range(2*variable)}
graphs.append(graph)
graph_t = {v:[] for v in range(2*variable)}
graphs_t.append(graph_t)
# print(graphs)
# print(graphs_t)
# print(variables)
# print(clauses)
# the solution:
# ==============================
def dfs1(v, used, order):
if used[v]:
return
used[v] = True
for u in graph[v]:
if not used[u]:
dfs1(u, used, order)
order.append(v)
def dfs2(v, cl, comp, graph_t):
comp[v] = cl
for u in graph_t[v]:
if comp[u] == -1:
dfs2(u, cl, comp, graph_t)
def solve_2sat(n, graph, graph_t):
order = []
used = [False] * n
for i in range(n):
if not used[i]:
dfs1(i, used, order)
# print(order)
comp = [-1] * n
j = 0
for i in range(n):
v = order[n-i-1]
if comp[v] == -1:
j += 1
dfs2(v, j, comp, graph_t)
assignment = [False] * int(n/2)
# print(assignment)
for i in range(0, n, 2):
if comp[i] == comp[i+1]:
print(0)
return False
assignment[int(i/2)] = comp[i] > comp[i+1]
# output results:
# print(assignment)
print(1, end=" ")
for i in range(len(assignment)):
if assignment[i]:
print(i+1, end=" ")
else:
print(-(i+1), end=" ")
print()
return True
# the results:
for i in range(k):
# print(i)
graph = graphs[i]
graph_t = graphs_t[i]
variable = variables[i]
solve_2sat(variable*2, graph, graph_t)
# reference url:
# 1. https://cp-algorithms.com/graph/2SAT.html
# 2. https://www.geeksforgeeks.org/2-satisfiability-2-sat-problem/