1717
1818class Clause :
1919 """
20- A clause represented in Conjunctive Normal Form.
21- A clause is a set of literals, either complemented or otherwise.
22- 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)
20+ | A clause represented in Conjunctive Normal Form.
21+ | A clause is a set of literals, either complemented or otherwise.
22+ | 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)
2525
2626 Create model
27+
2728 >>> clause = Clause(["A1", "A2'", "A3"])
2829 >>> clause.evaluate({"A1": True})
2930 True
@@ -39,6 +40,7 @@ def __init__(self, literals: list[str]) -> None:
3940 def __str__ (self ) -> str :
4041 """
4142 To print a clause as in Conjunctive Normal Form.
43+
4244 >>> str(Clause(["A1", "A2'", "A3"]))
4345 "{A1 , A2' , A3}"
4446 """
@@ -47,6 +49,7 @@ def __str__(self) -> str:
4749 def __len__ (self ) -> int :
4850 """
4951 To print a clause as in Conjunctive Normal Form.
52+
5053 >>> len(Clause([]))
5154 0
5255 >>> len(Clause(["A1", "A2'", "A3"]))
@@ -71,12 +74,12 @@ def assign(self, model: dict[str, bool | None]) -> None:
7174
7275 def evaluate (self , model : dict [str , bool | None ]) -> bool | None :
7376 """
74- Evaluates the clause with the assignments in model.
75- 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.
77+ | Evaluates the clause with the assignments in model.
78+ | This has the following steps:
79+ | 1. Return `` True`` if both a literal and its complement exist in the clause.
80+ | 2. Return `` True`` if a single literal has the assignment `` True`` .
81+ | 3. Return `` None`` (unable to complete evaluation) if a literal has no assignment.
82+ | 4. Compute disjunction of all values assigned in clause.
8083 """
8184 for literal in self .literals :
8285 symbol = literal .rstrip ("'" ) if literal .endswith ("'" ) else literal + "'"
@@ -92,10 +95,10 @@ def evaluate(self, model: dict[str, bool | None]) -> bool | None:
9295
9396class Formula :
9497 """
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))
98+ | A formula represented in Conjunctive Normal Form.
99+ | A formula is a set of clauses.
100+ | For example,
101+ | {{A1, A2, A3'}, {A5', A2', A1}} is ((A1 v A2 v A3') and (A5' v A2' v A1))
99102 """
100103
101104 def __init__ (self , clauses : Iterable [Clause ]) -> None :
@@ -107,16 +110,17 @@ def __init__(self, clauses: Iterable[Clause]) -> None:
107110 def __str__ (self ) -> str :
108111 """
109112 To print a formula as in Conjunctive Normal Form.
110- str(Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]))
113+
114+ >>> str(Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])]))
111115 "{{A1 , A2' , A3} , {A5' , A2' , A1}}"
112116 """
113117 return "{" + " , " .join (str (clause ) for clause in self .clauses ) + "}"
114118
115119
116120def generate_clause () -> Clause :
117121 """
118- Randomly generate a clause.
119- All literals have the name Ax, where x is an integer from 1 to 5 .
122+ | Randomly generate a clause.
123+ | All literals have the name Ax, where x is an integer from ``1`` to ``5`` .
120124 """
121125 literals = []
122126 no_of_literals = random .randint (1 , 5 )
@@ -149,11 +153,11 @@ def generate_formula() -> Formula:
149153
150154def generate_parameters (formula : Formula ) -> tuple [list [Clause ], list [str ]]:
151155 """
152- Return the clauses and symbols from a formula.
153- A symbol is the uncomplemented form of a literal.
154- For example,
155- Symbol of A3 is A3.
156- Symbol of A5' is A5.
156+ | Return the clauses and symbols from a formula.
157+ | A symbol is the uncomplemented form of a literal.
158+ | For example,
159+ | * Symbol of A3 is A3.
160+ | * Symbol of A5' is A5.
157161
158162 >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
159163 >>> clauses, symbols = generate_parameters(formula)
@@ -177,21 +181,20 @@ def find_pure_symbols(
177181 clauses : list [Clause ], symbols : list [str ], model : dict [str , bool | None ]
178182) -> tuple [list [str ], dict [str , bool | None ]]:
179183 """
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.
184+ | Return pure symbols and their values to satisfy clause.
185+ | Pure symbols are symbols in a formula that exist only in one form,
186+ | either complemented or otherwise.
187+ | For example,
188+ | {{ A4 , A3 , A5' , A1 , A3'} , {A4 } , {A3} } has pure symbols A4, A5' and A1.
189+
186190 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.
191+ 1. Ignore clauses that have already evaluated to be `` True`` .
192+ 2. Find symbols that occur only in one form in the rest of the clauses.
193+ 3. Assign value `` True`` or `` False`` depending on whether the symbols occurs
194+ in normal or complemented form respectively.
191195
192196 >>> formula = Formula([Clause(["A1", "A2'", "A3"]), Clause(["A5'", "A2'", "A1"])])
193197 >>> clauses, symbols = generate_parameters(formula)
194-
195198 >>> pure_symbols, values = find_pure_symbols(clauses, symbols, {})
196199 >>> pure_symbols
197200 ['A1', 'A2', 'A3', 'A5']
@@ -230,21 +233,20 @@ def find_unit_clauses(
230233 model : dict [str , bool | None ], # noqa: ARG001
231234) -> tuple [list [str ], dict [str , bool | None ]]:
232235 """
233- Returns the unit symbols and their values to satisfy clause.
234- 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
237- 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.
236+ | Returns the unit symbols and their values to satisfy clause.
237+ | Unit symbols are symbols in a formula that are:
238+ | - Either the only symbol in a clause
239+ | - Or all other literals in that clause have been assigned `` False``
240+ | This has the following steps:
241+ | 1. Find symbols that are the only occurrences in a clause.
242+ | 2. Find symbols in a clause where all other literals are assigned `` False`` .
243+ | 3. Assign `` True`` or `` False`` depending on whether the symbols occurs in
244+ | normal or complemented form respectively.
242245
243246 >>> clause1 = Clause(["A4", "A3", "A5'", "A1", "A3'"])
244247 >>> clause2 = Clause(["A4"])
245248 >>> clause3 = Clause(["A3"])
246249 >>> clauses, symbols = generate_parameters(Formula([clause1, clause2, clause3]))
247-
248250 >>> unit_clauses, values = find_unit_clauses(clauses, {})
249251 >>> unit_clauses
250252 ['A4', 'A3']
@@ -278,16 +280,15 @@ def dpll_algorithm(
278280 clauses : list [Clause ], symbols : list [str ], model : dict [str , bool | None ]
279281) -> tuple [bool | None , dict [str , bool | None ] | None ]:
280282 """
281- Returns the model if the formula is satisfiable, else None
282- 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.
283+ | Returns the model if the formula is satisfiable, else `` None``
284+ | This has the following steps:
285+ | 1. If every clause in clauses is `` True`` , return `` True`` .
286+ | 2. If some clause in clauses is `` False`` , return `` False`` .
287+ | 3. Find pure symbols.
288+ | 4. Find unit symbols.
287289
288290 >>> formula = Formula([Clause(["A4", "A3", "A5'", "A1", "A3'"]), Clause(["A4"])])
289291 >>> clauses, symbols = generate_parameters(formula)
290-
291292 >>> soln, model = dpll_algorithm(clauses, symbols, {})
292293 >>> soln
293294 True
0 commit comments