Skip to content

Commit dde4611

Browse files
ShivanirudhShivanirudh
committed
DPLL algorithm
1 parent fdba34f commit dde4611

File tree

1 file changed

+314
-0
lines changed

1 file changed

+314
-0
lines changed

‎other/dpll.py

Lines changed: 314 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,314 @@
1+
"""
2+
Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm
3+
for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.
4+
5+
For more information about the algorithm: https://en.wikipedia.org/wiki/DPLL_algorithm
6+
"""
7+
8+
import random
9+
10+
11+
class Clause():
12+
"""
13+
A clause represented in CNF.
14+
A clause is a set of literals, either complemented or otherwise.
15+
For example:
16+
{A1, A2, A3'} is the clause (A1 v A2 v A3')
17+
{A5', A2', A1} is the clause (A5' v A2' v A1)
18+
"""
19+
20+
def __init__(self, no_of_literals, literals):
21+
"""
22+
Represent the number of literals, the literals themselves, and an assignment in a clause."
23+
"""
24+
self.no_of_literals = no_of_literals
25+
self.literals = [l for l in literals]
26+
self.literal_values = dict()
27+
for l in self.literals:
28+
self.literal_values[l] = None # Assign all literals to None initially
29+
30+
def __str__(self):
31+
"""
32+
To print a clause as in CNF.
33+
Variable clause holds the string representation.
34+
"""
35+
clause = "{ "
36+
for i in range(0, self.no_of_literals):
37+
clause += (self.literals[i] + " ")
38+
if i != self.no_of_literals - 1:
39+
clause += ", "
40+
clause += "}"
41+
42+
return clause
43+
44+
def assign(self, model):
45+
"""
46+
Assign values to literals of the clause as given by model.
47+
"""
48+
i = 0
49+
while i < self.no_of_literals:
50+
symbol = self.literals[i][:2]
51+
if symbol in model.keys():
52+
val = model[symbol]
53+
else:
54+
i += 1
55+
continue
56+
if val != None:
57+
if self.literals[i][-1] == "'":
58+
val = not val #Complement assignment if literal is in complemented form
59+
self.literal_values[self.literals[i]] = val
60+
i += 1
61+
62+
def evaluate(self, model):
63+
"""
64+
Evaluates the clause till the extent possible with the current assignments in model.
65+
This has the following steps:
66+
1. Return True if both a literal and its complement exist in the clause.
67+
2. Return True if a single literal has the assignment True.
68+
3. Return None(unable to complete evaluation) if a literal has no assignment.
69+
4. Compute disjunction of all values assigned in clause.
70+
"""
71+
for l in self.literals:
72+
if len(l) == 2:
73+
symbol = l + "'"
74+
if symbol in self.literals:
75+
return True
76+
else:
77+
symbol = l[:2]
78+
if symbol in self.literals:
79+
return True
80+
81+
self.assign(model)
82+
result = False
83+
for j in self.literal_values.values():
84+
if j == True:
85+
return True
86+
elif j == None:
87+
return None
88+
for j in self.literal_values.values():
89+
result = result or j
90+
return result
91+
92+
class Formula():
93+
"""
94+
A formula represented in CNF.
95+
A formula is a set of clauses.
96+
For example,
97+
{{A1, A2, A3'}, {A5', A2', A1}} is the formula ((A1 v A2 v A3') and (A5' v A2' v A1))
98+
"""
99+
def __init__(self, no_of_clauses, clauses):
100+
"""
101+
Represent the number of clauses and the clauses themselves.
102+
"""
103+
self.no_of_clauses = no_of_clauses
104+
self.clauses = [c for c in clauses]
105+
106+
def __str__(self):
107+
"""
108+
To print a formula as in CNF.
109+
Variable formula holds the string representation.
110+
"""
111+
formula = "{ "
112+
for i in range(0, self.no_of_clauses):
113+
formula += (str(self.clauses[i]) + " ")
114+
if i != self.no_of_clauses - 1:
115+
formula += ", "
116+
formula += "}"
117+
118+
return formula
119+
120+
def generate_clause():
121+
"""
122+
Randomly generate a clause.
123+
All literals have the name Ax, where x is an integer from 1 to 5.
124+
"""
125+
literals = []
126+
no_of_literals = random.randint(1, 5)
127+
base_var = "A"
128+
i = 0
129+
while i < no_of_literals:
130+
var_no = random.randint(1, 5)
131+
var_name = base_var+str(var_no)
132+
var_complement = random.randint(0, 1)
133+
if var_complement == 1:
134+
var_name += "'"
135+
if var_name in literals:
136+
i -= 1
137+
else:
138+
literals.append(var_name)
139+
i+=1
140+
clause = Clause(no_of_literals, literals)
141+
return clause
142+
143+
def generate_formula():
144+
"""
145+
Randomly generate a formula.
146+
"""
147+
clauses = []
148+
no_of_clauses = random.randint(1, 10)
149+
i = 0
150+
while i < no_of_clauses:
151+
clause = generate_clause()
152+
if clause in clauses:
153+
i -= 1
154+
else:
155+
clauses.append(clause)
156+
i += 1
157+
formula = Formula(no_of_clauses, clauses)
158+
return formula
159+
160+
def generate_parameters(formula):
161+
"""
162+
Return the clauses and symbols from a formula.
163+
A symbol is the uncomplemented form of a literal.
164+
For example,
165+
Symbol of A3 is A3.
166+
Symbol of A5' is A5.
167+
168+
"""
169+
clauses = formula.clauses
170+
symbols_set = []
171+
for clause in formula.clauses:
172+
for literal in clause.literals:
173+
symbol = literal[:2]
174+
if symbol not in symbols_set:
175+
symbols_set.append(symbol)
176+
return clauses, symbols_set
177+
178+
def find_pure_symbols(clauses, symbols, model):
179+
"""
180+
Return pure symbols and their assignments to satisfy the clause, if figurable.
181+
Pure symbols are symbols in a formula that exist only in one form, either complemented or otherwise.
182+
For example,
183+
{ { A4 , A3 , A5' , A1 , A3' } , { A4 } , { A3 } } has the pure symbols A4, A5' and A1.
184+
This has the following steps:
185+
1. Ignore clauses that have already evaluated to be True.
186+
2. Find symbols that occur only in one form in the rest of the clauses.
187+
3. Assign value True or False depending on whether the symbols occurs in normal or complemented form respectively.
188+
"""
189+
pure_symbols = []
190+
assignment = dict()
191+
literals = []
192+
193+
for clause in clauses:
194+
if clause.evaluate(model) == True:
195+
continue
196+
for l in clause.literals:
197+
literals.append(l)
198+
199+
for s in symbols:
200+
sym = (s + "'")
201+
if (s in literals and sym not in literals) or (s not in literals and sym in literals):
202+
pure_symbols.append(s)
203+
for p in pure_symbols:
204+
assignment[p] = None
205+
for s in pure_symbols:
206+
sym = (s + "'")
207+
if s in literals:
208+
assignment[s] = True
209+
elif sym in literals:
210+
assignment[s] = False
211+
return pure_symbols, assignment
212+
213+
def find_unit_clauses(clauses, model):
214+
"""
215+
Returns the unit symbols and their assignments to satisfy the clause, if figurable.
216+
Unit symbols are symbols in a formula that are:
217+
- Either the only symbol in a clause
218+
- Or all other literals in that clause have been assigned False
219+
This has the following steps:
220+
1. Find symbols that are the only occurences in a clause.
221+
2. Find symbols in a clause where all other literals are assigned to be False.
222+
3. Assign True or False depending on whether the symbols occurs in normal or complemented form respectively.
223+
"""
224+
unit_symbols = []
225+
for clause in clauses:
226+
if clause.no_of_literals == 1:
227+
unit_symbols.append(clause.literals[0])
228+
else:
229+
Fcount, Ncount = 0, 0
230+
for l,v in clause.literal_values.items():
231+
if v == False:
232+
Fcount += 1
233+
elif v == None:
234+
sym = l
235+
Ncount += 1
236+
if Fcount == clause.no_of_literals - 1 and Ncount == 1:
237+
unit.append(sym)
238+
assignment = dict()
239+
for i in unit_symbols:
240+
symbol = i[:2]
241+
if len(i) == 2:
242+
assignment[symbol] = True
243+
else:
244+
assignment[symbol] = False
245+
unit_symbols = [i[:2] for i in unit_symbols]
246+
247+
return unit_symbols, assignment
248+
249+
def DPLL(clauses, symbols, model):
250+
"""
251+
Returns the model if the formula is satisfiable, else None
252+
This has the following steps:
253+
1. If every clause in clauses is True, return True.
254+
2. If some clause in clauses is False, return False.
255+
3. Find pure symbols.
256+
4. Find unit symbols.
257+
"""
258+
check_clause_all_true = True
259+
for clause in clauses:
260+
clause_check = clause.evaluate(model)
261+
if clause_check == False:
262+
return False, None
263+
elif clause_check == None:
264+
check_clause_all_true = False
265+
continue
266+
267+
if check_clause_all_true:
268+
return True, model
269+
270+
pure_symbols, assignment = find_pure_symbols(clauses, symbols, model)
271+
P = None
272+
if len(pure_symbols) > 0:
273+
P, value = pure_symbols[0], assignment[pure_symbols[0]]
274+
275+
if P:
276+
tmp_model = model
277+
tmp_model[P] = value
278+
tmp_symbols = [i for i in symbols]
279+
if P in tmp_symbols:
280+
tmp_symbols.remove(P)
281+
return DPLL(clauses, tmp_symbols, tmp_model)
282+
283+
unit_symbols, assignment = find_unit_clauses(clauses, model)
284+
P = None
285+
if len(unit_symbols) > 0:
286+
P, value = unit_symbols[0], assignment[unit_symbols[0]]
287+
if P:
288+
tmp_model = model
289+
tmp_model[P]=value
290+
tmp_symbols = [i for i in symbols]
291+
if P in tmp_symbols:
292+
tmp_symbols.remove(P)
293+
return DPLL(clauses, tmp_symbols, tmp_model)
294+
P = symbols[0]
295+
rest = symbols[1:]
296+
tmp1, tmp2 = model, model
297+
tmp1[P], tmp2[P] = True, False
298+
299+
return DPLL(clauses, rest, tmp1) or DPLL(clauses, rest, tmp2)
300+
301+
if __name__ == "__main__":
302+
#import doctest
303+
#doctest.testmod()
304+
formula = generate_formula()
305+
print(formula)
306+
307+
clauses, symbols = generate_parameters(formula)
308+
309+
solution, model = DPLL(clauses, symbols, {})
310+
311+
if solution:
312+
print(model)
313+
else:
314+
print("Not satisfiable")

0 commit comments

Comments
 (0)