1717
1818class Clause :
1919 """
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+
2223 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)
2526
2627 Create model
28+
2729 >>> clause = Clause(["A1", "A2'", "A3"])
2830 >>> clause.evaluate({"A1": True})
2931 True
@@ -39,6 +41,7 @@ def __init__(self, literals: list[str]) -> None:
3941 def __str__ (self ) -> str :
4042 """
4143 To print a clause as in Conjunctive Normal Form.
44+
4245 >>> str(Clause(["A1", "A2'", "A3"]))
4346 "{A1 , A2' , A3}"
4447 """
@@ -47,6 +50,7 @@ def __str__(self) -> str:
4750 def __len__ (self ) -> int :
4851 """
4952 To print a clause as in Conjunctive Normal Form.
53+
5054 >>> len(Clause([]))
5155 0
5256 >>> len(Clause(["A1", "A2'", "A3"]))
@@ -72,11 +76,13 @@ def assign(self, model: dict[str, bool | None]) -> None:
7276 def evaluate (self , model : dict [str , bool | None ]) -> bool | None :
7377 """
7478 Evaluates the clause with the assignments in model.
79+
7580 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.
8086 """
8187 for literal in self .literals :
8288 symbol = literal .rstrip ("'" ) if literal .endswith ("'" ) else literal + "'"
@@ -92,10 +98,10 @@ def evaluate(self, model: dict[str, bool | None]) -> bool | None:
9298
9399class Formula :
94100 """
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))
99105 """
100106
101107 def __init__ (self , clauses : Iterable [Clause ]) -> None :
@@ -107,16 +113,17 @@ def __init__(self, clauses: Iterable[Clause]) -> None:
107113 def __str__ (self ) -> str :
108114 """
109115 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"])]))
111118 "{{A1 , A2' , A3} , {A5' , A2' , A1}}"
112119 """
113120 return "{" + " , " .join (str (clause ) for clause in self .clauses ) + "}"
114121
115122
116123def generate_clause () -> Clause :
117124 """
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`` .
120127 """
121128 literals = []
122129 no_of_literals = random .randint (1 , 5 )
@@ -149,11 +156,12 @@ def generate_formula() -> Formula:
149156
150157def generate_parameters (formula : Formula ) -> tuple [list [Clause ], list [str ]]:
151158 """
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+
154162 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.
157165
158166 >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
159167 >>> clauses, symbols = generate_parameters(formula)
@@ -177,21 +185,20 @@ def find_pure_symbols(
177185 clauses : list [Clause ], symbols : list [str ], model : dict [str , bool | None ]
178186) -> tuple [list [str ], dict [str , bool | None ]]:
179187 """
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+
186194 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.
191199
192200 >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
193201 >>> clauses, symbols = generate_parameters(formula)
194-
195202 >>> pure_symbols, values = find_pure_symbols(clauses, symbols, {})
196203 >>> pure_symbols
197204 ['A1', 'A2', 'A3', 'A5']
@@ -231,20 +238,21 @@ def find_unit_clauses(
231238) -> tuple [list [str ], dict [str , bool | None ]]:
232239 """
233240 Returns the unit symbols and their values to satisfy clause.
241+
234242 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+
237246 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.
242251
243252 >>> clause1 = Clause(["A4", "A3", "A5'", "A1", "A3'"])
244253 >>> clause2 = Clause(["A4"])
245254 >>> clause3 = Clause(["A3"])
246255 >>> clauses, symbols = generate_parameters(Formula([clause1, clause2, clause3]))
247-
248256 >>> unit_clauses, values = find_unit_clauses(clauses, {})
249257 >>> unit_clauses
250258 ['A4', 'A3']
@@ -278,16 +286,16 @@ def dpll_algorithm(
278286 clauses : list [Clause ], symbols : list [str ], model : dict [str , bool | None ]
279287) -> tuple [bool | None , dict [str , bool | None ] | None ]:
280288 """
281- Returns the model if the formula is satisfiable, else None
289+ Returns the model if the formula is satisfiable, else ``None``
290+
282291 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.
287296
288297 >>> formula = Formula([Clause(["A4", "A3", "A5'", "A1", "A3'"]), Clause(["A4"])])
289298 >>> clauses, symbols = generate_parameters(formula)
290-
291299 >>> soln, model = dpll_algorithm(clauses, symbols, {})
292300 >>> soln
293301 True
0 commit comments