2
2
Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete,
3
3
backtracking-based search algorithm for deciding the satisfiability of
4
4
propositional logic formulae in conjunctive normal form,
5
- i.e, for solving the CNF-SAT problem.
5
+ i.e, for solving the Conjunctive Normal Form SATisfiability( CNF-SAT) problem.
6
6
7
7
For more information about the algorithm:
8
8
https://en.wikipedia.org/wiki/DPLL_algorithm
@@ -21,14 +21,12 @@ class Clause:
21
21
{A5', A2', A1} is the clause (A5' v A2' v A1)
22
22
23
23
Create a set of literals and a clause with them
24
- >>> literals = ["A1", "A2'", "A3"]
25
- >>> clause = Clause(literals)
26
- >>> print(clause)
27
- { A1 , A2' , A3 }
24
+ >>> str(Clause(["A1", "A2'", "A3"]))
25
+ "{A1 , A2' , A3}"
28
26
29
27
Create model
30
- >>> model = { "A1": True}
31
- >>> clause.evaluate(model )
28
+ >>> clause = Clause([ "A1", "A2'", "A3"])
29
+ >>> clause.evaluate({"A1": True} )
32
30
True
33
31
"""
34
32
@@ -43,16 +41,8 @@ def __init__(self, literals: List[int]) -> None:
43
41
def __str__ (self ) -> str :
44
42
"""
45
43
To print a clause as in CNF.
46
- Variable clause holds the string representation.
47
44
"""
48
- clause = "{ "
49
- for i in range (0 , self .no_of_literals ):
50
- clause += str (list (self .literals .keys ())[i ]) + " "
51
- if i != self .no_of_literals - 1 :
52
- clause += ", "
53
- clause += "}"
54
-
55
- return clause
45
+ return "{" + " , " .join (self .literals ) + "}"
56
46
57
47
def assign (self , model : Dict [str , bool ]) -> None :
58
48
"""
@@ -110,12 +100,9 @@ class Formula:
110
100
{{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1))
111
101
112
102
Create two clauses and a formula with them
113
- >>> clause1 = Clause(["A1", "A2'", "A3"])
114
- >>> clause2 = Clause(["A5'", "A2'", "A1"])
115
-
116
- >>> formula = Formula([clause1, clause2])
117
- >>> print(formula)
118
- {{ A1 , A2' , A3 } , { A5' , A2' , A1 }}
103
+ >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
104
+ >>> str(formula)
105
+ "{{A1 , A2' , A3} , {A5' , A2' , A1}}"
119
106
"""
120
107
121
108
def __init__ (self , clauses : List [Clause ]) -> None :
@@ -128,18 +115,8 @@ def __init__(self, clauses: List[Clause]) -> None:
128
115
def __str__ (self ) -> str :
129
116
"""
130
117
To print a formula as in CNF.
131
- Variable formula holds the string representation.
132
118
"""
133
- formula = "{"
134
- clause_repr = " , "
135
- clauses_as_strings = [str (clause ) for clause in self .clauses ]
136
-
137
- clause_repr = clause_repr .join (clauses_as_strings )
138
-
139
- formula += clause_repr
140
- formula += "}"
141
-
142
- return formula
119
+ return "{" + " , " .join (str (clause ) for clause in self .clauses ) + "}"
143
120
144
121
145
122
def generate_clause () -> Clause :
@@ -190,15 +167,12 @@ def generate_parameters(formula: Formula) -> (List[Clause], List[str]):
190
167
Symbol of A3 is A3.
191
168
Symbol of A5' is A5.
192
169
193
- >>> clause1 = Clause(["A1", "A2'", "A3"])
194
- >>> clause2 = Clause(["A5'", "A2'", "A1"])
195
-
196
- >>> formula = Formula([clause1, clause2])
170
+ >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
197
171
>>> clauses, symbols = generate_parameters(formula)
198
172
>>> clauses_list = [str(i) for i in clauses]
199
- >>> print( clauses_list)
200
- ["{ A1 , A2' , A3 }", "{ A5' , A2' , A1 }"]
201
- >>> print( symbols)
173
+ >>> clauses_list
174
+ ["{A1 , A2' , A3}", "{A5' , A2' , A1}"]
175
+ >>> symbols
202
176
['A1', 'A2', 'A3', 'A5']
203
177
"""
204
178
clauses = formula .clauses
@@ -227,16 +201,14 @@ def find_pure_symbols(
227
201
3. Assign value True or False depending on whether the symbols occurs
228
202
in normal or complemented form respectively.
229
203
230
- >>> clause1 = Clause(["A1", "A2'", "A3"])
231
- >>> clause2 = Clause(["A5'", "A2'", "A1"])
232
-
233
- >>> formula = Formula([clause1, clause2])
204
+ >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
234
205
>>> clauses, symbols = generate_parameters(formula)
235
206
236
- >>> model = {}
237
- >>> pure_symbols, values = find_pure_symbols(clauses, symbols, model)
238
- >>> print(pure_symbols, values)
239
- ['A1', 'A2', 'A3', 'A5'] {'A1': True, 'A2': False, 'A3': True, 'A5': False}
207
+ >>> pure_symbols, values = find_pure_symbols(clauses, symbols, {})
208
+ >>> pure_symbols
209
+ ['A1', 'A2', 'A3', 'A5']
210
+ >>> values
211
+ {'A1': True, 'A2': False, 'A3': True, 'A5': False}
240
212
"""
241
213
pure_symbols = []
242
214
assignment = dict ()
@@ -282,15 +254,13 @@ def find_unit_clauses(
282
254
>>> clause1 = Clause(["A4", "A3", "A5'", "A1", "A3'"])
283
255
>>> clause2 = Clause(["A4"])
284
256
>>> clause3 = Clause(["A3"])
257
+ >>> clauses, symbols = generate_parameters(Formula([clause1, clause2, clause3]))
285
258
286
- >>> formula = Formula([clause1, clause2, clause3])
287
- >>> clauses, symbols = generate_parameters(formula)
288
-
289
- >>> model = {}
290
- >>> unit_clauses, values = find_unit_clauses(clauses, model)
291
-
292
- >>> print(unit_clauses, values)
293
- ['A4', 'A3'] {'A4': True, 'A3': True}
259
+ >>> unit_clauses, values = find_unit_clauses(clauses, {})
260
+ >>> unit_clauses
261
+ ['A4', 'A3']
262
+ >>> values
263
+ {'A4': True, 'A3': True}
294
264
"""
295
265
unit_symbols = []
296
266
for clause in clauses :
@@ -326,18 +296,14 @@ def dpll_algorithm(
326
296
3. Find pure symbols.
327
297
4. Find unit symbols.
328
298
329
- >>> c1 = Clause(["A4", "A3", "A5'", "A1", "A3'"])
330
- >>> c2 = Clause(["A4"])
331
- >>> c3 = Clause(["A3"])
332
-
333
- >>> f = Formula([c1, c2, c3])
334
- >>> c, s = generate_parameters(f)
335
-
336
- >>> model = {}
337
- >>> soln, model = dpll_algorithm(c, s, model)
299
+ >>> formula = Formula([Clause(["A4", "A3", "A5'", "A1", "A3'"]), Clause(["A4"])])
300
+ >>> clauses, symbols = generate_parameters(formula)
338
301
339
- >>> print(soln, model)
340
- True {'A4': True, 'A3': True}
302
+ >>> soln, model = dpll_algorithm(clauses, symbols, {})
303
+ >>> soln
304
+ True
305
+ >>> model
306
+ {'A4': True}
341
307
"""
342
308
check_clause_all_true = True
343
309
for clause in clauses :
@@ -389,7 +355,7 @@ def dpll_algorithm(
389
355
doctest .testmod ()
390
356
391
357
formula = generate_formula ()
392
- print (f"The formula { formula } is" , end = " " )
358
+ print (f"The formula \n { formula } \n is" , end = " " )
393
359
394
360
clauses , symbols = generate_parameters (formula )
395
361
0 commit comments