# Untitled

a guest
Jul 6th, 2024
102
0
Never
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
1.
2. import random
3. from collections import defaultdict
4. import matplotlib.pyplot as plt
6.
7. # Tarjan's algorithm for finding SCCs
8. def tarjan_scc(graph, n):
9. index = 0
10. indices = [-1] * (2 * n + 1)
11. lowlink = [-1] * (2 * n + 1)
12. on_stack = [False] * (2 * n + 1)
13. stack = []
14. sccs = []
15.
16. def strong_connect(v):
17. nonlocal index
18. indices[v] = index
20. index += 1
21. stack.append(v)
22. on_stack[v] = True
23.
24. for w in graph[v]:
25. if indices[w] == -1:
26. strong_connect(w)
28. elif on_stack[w]:
30.
32. scc = []
33. while True:
34. w = stack.pop()
35. on_stack[w] = False
36. scc.append(w)
37. if w == v:
38. break
39. sccs.append(scc)
40.
41. for v in range(-n, n + 1):
42. if v != 0 and indices[v] == -1:
43. strong_connect(v)
44.
45. return sccs
46.
47. # 3-SAT Solver with Layering
48. def solve_3sat_problem(clauses):
49. n = max(abs(literal) for clause in clauses for literal in clause)
50. graph = defaultdict(list)
51.
53. graph[-u].append(v)
54. graph[-v].append(w)
55. graph[-w].append(u)
56.
57. for u, v, w in clauses:
59.
60. sccs = tarjan_scc(graph, n)
61. assignment = [-1] * (n + 1)
62. scc_index = {v: i for i, scc in enumerate(sccs) for v in scc}
63.
64. for i in range(1, n + 1):
65. if scc_index[i] == scc_index[-i]:
66. return [] # No solution exists
67. assignment[i] = scc_index[-i] > scc_index[i]
68.
69. return [i if assignment[i] else -i for i in range(1, n + 1)]
70.
71. # Visualization function for 3-SAT solutions
72. def visualize_3sat_solution(clauses, solution, is_valid):
73. fig, ax = plt.subplots(figsize=(10, 8))
74. ax.set_title(f"3-SAT Problem Solution\nValid: {is_valid}")
75. ax.set_xlabel("Clauses")
76. ax.set_ylabel("Number of Literals")
77.
78. sample_size = min(50, len(clauses))
79. sample_clauses = clauses[:sample_size]
80.
81. literals = [literal for clause in sample_clauses for literal in clause]
82. counts = defaultdict(int)
83. for literal in literals:
84. counts[literal] += 1
85.
86. literals, occurrences = zip(*sorted(counts.items()))
87.
88. ax.bar(literals, occurrences)
89. plt.show()
90.
91. # 3-SAT solution validation
92. def validate_3sat_solution(clauses, solution):
93. if not solution:
94. return False
95.
96. assignment = {abs(lit): (lit > 0) for lit in solution}
97.
98. for u, v, w in clauses:
99. if not ((assignment[abs(u)] if u > 0 else not assignment[abs(u)]) or
100. (assignment[abs(v)] if v > 0 else not assignment[abs(v)]) or
101. (assignment[abs(w)] if w > 0 else not assignment[abs(w)])):
102. return False
103.
104. return True
105.
106. # Generate random 3-SAT problem
107. def generate_random_3sat(num_variables, num_clauses):
108. clauses = []
109. for _ in range(num_clauses):
110. clause = tuple(random.sample([random.choice([-1, 1]) * i for i in range(1, num_variables + 1)], 3))
111. clauses.append(clause)
112. return clauses
113.
114. # Split clauses into layers
115. def split_into_layers(clauses, num_layers):
116. layers = [[] for _ in range(num_layers)]
117. for i, clause in enumerate(clauses):
118. layers[i % num_layers].append(clause)
119. return layers
120.
121. # Solve and validate each layer in parallel
122. def process_layer(layer):
123. solution = solve_3sat_problem(layer)
124. is_valid = validate_3sat_solution(layer, solution)
125. return solution, is_valid
126.
127. # Translate solution to clauses
128. def translate_solution_to_clauses(solution, num_variables):
129. clauses = []
130. for lit in solution:
131. a = lit
132. b = random.choice([i for i in range(1, num_variables + 1) if i != abs(a)]) * random.choice([-1, 1])
133. c = random.choice([i for i in range(1, num_variables + 1) if i != abs(a) and i != abs(b)]) * random.choice([-1, 1])
134. clause = (a, b, c)
135. clauses.append(clause)
136. return clauses
137.
138. # Example usage
139. num_variables = 10
140. num_clauses = 30
141. num_layers = 10
142. clauses = generate_random_3sat(num_variables, num_clauses)
143. layers = split_into_layers(clauses, num_layers)
144.
146. futures = [executor.submit(process_layer, layer) for layer in layers]
147. results = [future.result() for future in futures]
148.
149. overall_valid_count = 0
150.
151. for i, (solution, is_valid) in enumerate(results):
152. print(f"Layer {i+1} Solution:", solution)
153. print(f"Is the solution valid for Layer {i+1}?", is_valid)
154. visualize_3sat_solution(layers[i], solution, is_valid)
155. translated_clauses = translate_solution_to_clauses(solution, num_variables)
156. print(f"Translated Clauses for Layer {i+1}:", translated_clauses)
157. overall_valid_count += is_valid
158. print()
159.
160. # Calculate precision
161. precision = overall_valid_count / num_layers * 100
162. print(f"Overall Precision: {precision}%")