-
Notifications
You must be signed in to change notification settings - Fork 0
/
SAT SOLVER
119 lines (93 loc) · 2.38 KB
/
SAT SOLVER
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
interpret = [] # global
class node:
def __init__(self, data):
self.data = data
self.next = None
class LinkedList:
def __init__(self):
self.head = None
def insert(self, data): # inserting a node in the LL
newNode = node(data)
if(self.head):
current = self.head
while(current.next):
current = current.next
current.next = newNode
else:
self.head = newNode
def printLL(self): # printing the LL
current = self.head
while(current):
print(current.data)
current = current.next
def add_literal(data): # adding literal to the interpret if possible else return None
if (interpret == []) :
interpret.append(data)
return data
for lit in interpret:
if lit + data ==0:
return None
interpret.append(data)
return data
def solve(node): # recursive function to solve the cnf
if node == None :
return True
for lit in node.data :
if add_literal(lit) is None:
continue
else :
if solve(node.next) is False:
interpret.pop()
continue
else :
return True
return False
def search(data): # searching a literal in the interpret
for p in interpret:
if p == data:
return True
return False
def int_to_model(v) : # converting interpret to the model
model = []
for i in range(1,v+1) :
if search(i) is True:
model.append(i)
elif search(-i) is True:
model.append(-i)
else:
model.append(i)
return model
# main
cnf = LinkedList() # LL for clauses
file_name = input("Enter the file location :")
file = open(file_name)
# print(file.readline().strip()
# print(len(file.readline().strip()))
c = 0
v = 0
line = file.readline().strip()
while True :
if line.startswith('c') :
line = file.readline().strip()
continue
if line.startswith('p') :
words = line.split()
v = int(words[2])
c = int(words[3])
break
# print(s.variables)
while c >0 :
line = file.readline().strip()
words = line.split()
clause = [int(word) for word in words]
clause.pop()
cnf.insert(clause)
c = c-1
file.close()
ans = solve(cnf.head)
if ans is True:
model = int_to_model(v)
print(model)
else:
print("UNSAT")
# print(interpret)C:\sat solver\Assignment 2\abc.cnf