-
Notifications
You must be signed in to change notification settings - Fork 0
/
q4.py
69 lines (53 loc) · 1.7 KB
/
q4.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
# Provide user with current URL location
import os
import copy
path = os.getcwd()
# print(path)
print("If the file is not parsing properly, please delete any blank lines at the end and try again. Thanks :)")
print()
def load_dimacs():
clause_set = []
# Take url as input and read associated DIMACS file
url = input("Enter url of DIMACS file (including .txt extension): ")
# Interpret user input to reduce chance of error
if url[-4:] != ".txt":
url = url + ".txt"
if url[0] != "\\":
url = "\\" + url
url = path + url
f = open(url, "r")
data = f.read()
sat_list = data.split("\n")
f.close()
# Parse each line of DIMACS file as CNF
i = 0
while i < len(sat_list):
# Ignore blank lines
if not sat_list[i]:
i += 1
continue
# Ignore non-comment lines
elif sat_list[i][0] == "c":
i += 1
continue
# Ignore problem line
elif sat_list[i][0] == "p":
i += 1
continue
# Split SAT line by space
expression = sat_list[i].split()
# If a 0 is at the end of a line the expression is not finished, so read the next line
while expression[-1] != "0":
i += 1
expression += sat_list[i].split()
if expression[-1] == "0":
break
# Remove end 0 and append to clause set
expression.pop()
clause_set.append(expression)
i += 1
clause_set_format = copy.deepcopy(clause_set)
clause_set_format = [list(map(int, i)) for i in clause_set_format]
return clause_set_format
clauses = load_dimacs()
print("Output clause set: " + str(clauses))