-
Notifications
You must be signed in to change notification settings - Fork 2
/
Copy pathDPLL.py
163 lines (135 loc) · 4.94 KB
/
DPLL.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
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
import sys
from copy import deepcopy
truth_assignment = []
unit_propa = 0
splitting = -1
def remove_liter(cnf):
new_liters = list(set(''.join(cnf)))
if '!' in new_liters:
new_liters.remove('!')
if '\n' in new_liters:
new_liters.remove('\n')
if ' ' in new_liters:
new_liters.remove(' ')
return new_liters
def preproc(input_cnf):
liters = list(set(input_cnf))
if '!' in liters:
liters.remove('!')
if '\n' in liters:
liters.remove('\n')
if ' ' in liters:
liters.remove(' ')
# liters = dict(zip(liters, [False] * len(liters)))
liters = list(liters)
input_cnf = input_cnf.splitlines()
return liters, input_cnf
def dpll(cnf, liters):
global truth_assignment, unit_propa, splitting
splitting += 1
# ------------start unit propa-----------------
while True:
if len(liters) == 1 and len(cnf) > 1:
print('--------------------------------------------------')
print(cnf)
print(liters)
break
delete_list = []
unit_clause = None
cnf = list(set(cnf))
print('--------------------------------------------------')
print('CNF : ', cnf)
print('Liters : ', liters)
# find unit clause
for i in range(len(cnf)):
if ' ' not in cnf[i]:
unit_clause = cnf[i]
truth_assignment.append(unit_clause)
print('Unit : ', unit_clause)
del cnf[i]
break
# exception handle
if unit_clause:
for i in range(len(cnf)):
if '!' in unit_clause:
if unit_clause.replace('!', '') == cnf[i]:
return False
else:
if '!' + unit_clause == cnf[i]:
return False
if unit_clause and '!' not in unit_clause:
unit_propa += 1
for j in range(len(cnf)):
if '!' + unit_clause in cnf[j]:
if '!' + unit_clause == cnf[j]:
delete_list.append(j)
else:
cnf[j] = cnf[j].replace('!' + unit_clause, ' ')
cnf[j] = cnf[j].strip(' ')
# cnf.remove('')
elif unit_clause in cnf[j]:
delete_list.append(j)
for index in sorted(delete_list, reverse=True):
del cnf[index]
liters = remove_liter(cnf)
elif unit_clause and '!' in unit_clause:
unit_propa += 1
for j in range(len(cnf)):
if unit_clause in cnf[j]:
delete_list.append(j)
elif unit_clause.replace('!', '') in cnf[j]:
if unit_clause.replace('!', '') == cnf[j]:
delete_list.append(j)
else:
cnf[j] = cnf[j].replace(unit_clause.replace('!', ''), ' ')
cnf[j] = cnf[j].strip(' ')
for index in sorted(delete_list, reverse=True):
del cnf[index]
liters = remove_liter(cnf)
else:
break
# --------------end unit propa----------------------
# checking clause
if cnf == []:
return True
elif len(liters) == 1 and len(cnf) > 1:
return False
# case-splitting
if dpll(cnf + [liters[0]], deepcopy(liters)) or dpll(cnf + ['!' + liters[0]], deepcopy(liters)):
return True
else:
return False
def main():
global truth_assignment
input_cnf = open(sys.argv[1], 'r').read()
liters, cnf = preproc(input_cnf)
if dpll(cnf, liters):
print('--------------------------------------------------')
print('[Result] : Satisfiable')
# print truth assignment
for i in range(len(truth_assignment) - 1, 0, -1):
for j in range(i - 1, -1, -1):
if '!' in truth_assignment[i]:
if truth_assignment[i] == truth_assignment[j] or truth_assignment[i].replace('!', '') == \
truth_assignment[j]:
truth_assignment[j] = ''
else:
if truth_assignment[i] == truth_assignment[j]:
truth_assignment[j] = ''
if '' in truth_assignment:
truth_assignment = list(set(truth_assignment))
truth_assignment.remove('')
print('[Truth Assignment] | ', end='')
for i in truth_assignment:
if '!' in i:
print(i.replace('!', ''), ' : False', end=' | ')
else:
print(i, ' : True', end=' | ')
print('')
else:
print('--------------------------------------------------')
print('[Result] : UnSatisfiable')
print('[Unit propagation Count] : ', unit_propa)
print('[Splitting Count] : ', splitting)
if __name__ == '__main__':
main()