17
17
18
18
class Clause :
19
19
"""
20
- A clause represented in Conjunctive Normal Form.
21
- A clause is a set of literals, either complemented or otherwise.
20
+ | A clause represented in Conjunctive Normal Form.
21
+ | A clause is a set of literals, either complemented or otherwise.
22
+
22
23
For example:
23
- {A1, A2, A3'} is the clause (A1 v A2 v A3')
24
- {A5', A2', A1} is the clause (A5' v A2' v A1)
24
+ * {A1, A2, A3'} is the clause (A1 v A2 v A3')
25
+ * {A5', A2', A1} is the clause (A5' v A2' v A1)
25
26
26
27
Create model
28
+
27
29
>>> clause = Clause(["A1", "A2'", "A3"])
28
30
>>> clause.evaluate({"A1": True})
29
31
True
@@ -39,6 +41,7 @@ def __init__(self, literals: list[str]) -> None:
39
41
def __str__ (self ) -> str :
40
42
"""
41
43
To print a clause as in Conjunctive Normal Form.
44
+
42
45
>>> str(Clause(["A1", "A2'", "A3"]))
43
46
"{A1 , A2' , A3}"
44
47
"""
@@ -47,6 +50,7 @@ def __str__(self) -> str:
47
50
def __len__ (self ) -> int :
48
51
"""
49
52
To print a clause as in Conjunctive Normal Form.
53
+
50
54
>>> len(Clause([]))
51
55
0
52
56
>>> len(Clause(["A1", "A2'", "A3"]))
@@ -72,11 +76,13 @@ def assign(self, model: dict[str, bool | None]) -> None:
72
76
def evaluate (self , model : dict [str , bool | None ]) -> bool | None :
73
77
"""
74
78
Evaluates the clause with the assignments in model.
79
+
75
80
This has the following steps:
76
- 1. Return True if both a literal and its complement exist in the clause.
77
- 2. Return True if a single literal has the assignment True.
78
- 3. Return None(unable to complete evaluation) if a literal has no assignment.
79
- 4. Compute disjunction of all values assigned in clause.
81
+ 1. Return ``True`` if both a literal and its complement exist in the clause.
82
+ 2. Return ``True`` if a single literal has the assignment ``True``.
83
+ 3. Return ``None`` (unable to complete evaluation)
84
+ if a literal has no assignment.
85
+ 4. Compute disjunction of all values assigned in clause.
80
86
"""
81
87
for literal in self .literals :
82
88
symbol = literal .rstrip ("'" ) if literal .endswith ("'" ) else literal + "'"
@@ -92,10 +98,10 @@ def evaluate(self, model: dict[str, bool | None]) -> bool | None:
92
98
93
99
class Formula :
94
100
"""
95
- A formula represented in Conjunctive Normal Form.
96
- A formula is a set of clauses.
97
- For example,
98
- {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1))
101
+ | A formula represented in Conjunctive Normal Form.
102
+ | A formula is a set of clauses.
103
+ | For example,
104
+ | {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1))
99
105
"""
100
106
101
107
def __init__ (self , clauses : Iterable [Clause ]) -> None :
@@ -107,16 +113,17 @@ def __init__(self, clauses: Iterable[Clause]) -> None:
107
113
def __str__ (self ) -> str :
108
114
"""
109
115
To print a formula as in Conjunctive Normal Form.
110
- str(Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]))
116
+
117
+ >>> str(Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]))
111
118
"{{A1 , A2' , A3} , {A5' , A2' , A1}}"
112
119
"""
113
120
return "{" + " , " .join (str (clause ) for clause in self .clauses ) + "}"
114
121
115
122
116
123
def generate_clause () -> Clause :
117
124
"""
118
- Randomly generate a clause.
119
- All literals have the name Ax, where x is an integer from 1 to 5 .
125
+ | Randomly generate a clause.
126
+ | All literals have the name Ax, where x is an integer from ``1`` to ``5`` .
120
127
"""
121
128
literals = []
122
129
no_of_literals = random .randint (1 , 5 )
@@ -149,11 +156,12 @@ def generate_formula() -> Formula:
149
156
150
157
def generate_parameters (formula : Formula ) -> tuple [list [Clause ], list [str ]]:
151
158
"""
152
- Return the clauses and symbols from a formula.
153
- A symbol is the uncomplemented form of a literal.
159
+ | Return the clauses and symbols from a formula.
160
+ | A symbol is the uncomplemented form of a literal.
161
+
154
162
For example,
155
- Symbol of A3 is A3.
156
- Symbol of A5' is A5.
163
+ * Symbol of A3 is A3.
164
+ * Symbol of A5' is A5.
157
165
158
166
>>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
159
167
>>> clauses, symbols = generate_parameters(formula)
@@ -177,21 +185,20 @@ def find_pure_symbols(
177
185
clauses : list [Clause ], symbols : list [str ], model : dict [str , bool | None ]
178
186
) -> tuple [list [str ], dict [str , bool | None ]]:
179
187
"""
180
- Return pure symbols and their values to satisfy clause.
181
- Pure symbols are symbols in a formula that exist only
182
- in one form, either complemented or otherwise.
183
- For example,
184
- { { A4 , A3 , A5' , A1 , A3' } , { A4 } , { A3 } } has
185
- pure symbols A4, A5' and A1.
188
+ | Return pure symbols and their values to satisfy clause.
189
+ | Pure symbols are symbols in a formula that exist only in one form,
190
+ | either complemented or otherwise.
191
+ | For example,
192
+ | {{ A4 , A3 , A5' , A1 , A3'} , {A4 } , {A3} } has pure symbols A4, A5' and A1.
193
+
186
194
This has the following steps:
187
- 1. Ignore clauses that have already evaluated to be True.
188
- 2. Find symbols that occur only in one form in the rest of the clauses.
189
- 3. Assign value True or False depending on whether the symbols occurs
190
- in normal or complemented form respectively.
195
+ 1. Ignore clauses that have already evaluated to be `` True`` .
196
+ 2. Find symbols that occur only in one form in the rest of the clauses.
197
+ 3. Assign value `` True`` or `` False`` depending on whether the symbols occurs
198
+ in normal or complemented form respectively.
191
199
192
200
>>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
193
201
>>> clauses, symbols = generate_parameters(formula)
194
-
195
202
>>> pure_symbols, values = find_pure_symbols(clauses, symbols, {})
196
203
>>> pure_symbols
197
204
['A1', 'A2', 'A3', 'A5']
@@ -231,20 +238,21 @@ def find_unit_clauses(
231
238
) -> tuple [list [str ], dict [str , bool | None ]]:
232
239
"""
233
240
Returns the unit symbols and their values to satisfy clause.
241
+
234
242
Unit symbols are symbols in a formula that are:
235
- - Either the only symbol in a clause
236
- - Or all other literals in that clause have been assigned False
243
+ - Either the only symbol in a clause
244
+ - Or all other literals in that clause have been assigned ``False``
245
+
237
246
This has the following steps:
238
- 1. Find symbols that are the only occurrences in a clause.
239
- 2. Find symbols in a clause where all other literals are assigned False.
240
- 3. Assign True or False depending on whether the symbols occurs in
241
- normal or complemented form respectively.
247
+ 1. Find symbols that are the only occurrences in a clause.
248
+ 2. Find symbols in a clause where all other literals are assigned `` False`` .
249
+ 3. Assign `` True`` or `` False`` depending on whether the symbols occurs in
250
+ normal or complemented form respectively.
242
251
243
252
>>> clause1 = Clause(["A4", "A3", "A5'", "A1", "A3'"])
244
253
>>> clause2 = Clause(["A4"])
245
254
>>> clause3 = Clause(["A3"])
246
255
>>> clauses, symbols = generate_parameters(Formula([clause1, clause2, clause3]))
247
-
248
256
>>> unit_clauses, values = find_unit_clauses(clauses, {})
249
257
>>> unit_clauses
250
258
['A4', 'A3']
@@ -278,16 +286,16 @@ def dpll_algorithm(
278
286
clauses : list [Clause ], symbols : list [str ], model : dict [str , bool | None ]
279
287
) -> tuple [bool | None , dict [str , bool | None ] | None ]:
280
288
"""
281
- Returns the model if the formula is satisfiable, else None
289
+ Returns the model if the formula is satisfiable, else ``None``
290
+
282
291
This has the following steps:
283
- 1. If every clause in clauses is True, return True.
284
- 2. If some clause in clauses is False, return False.
285
- 3. Find pure symbols.
286
- 4. Find unit symbols.
292
+ 1. If every clause in clauses is `` True`` , return `` True`` .
293
+ 2. If some clause in clauses is `` False`` , return `` False`` .
294
+ 3. Find pure symbols.
295
+ 4. Find unit symbols.
287
296
288
297
>>> formula = Formula([Clause(["A4", "A3", "A5'", "A1", "A3'"]), Clause(["A4"])])
289
298
>>> clauses, symbols = generate_parameters(formula)
290
-
291
299
>>> soln, model = dpll_algorithm(clauses, symbols, {})
292
300
>>> soln
293
301
True
0 commit comments