Returns the model if the formula is satisfiable, else ``None`` This has the following steps: 1. If every clause in clauses is ``True``, return ``True``. 2. If some clause in clauses is ``False``, return ``False``. 3. Find pure symbols. 4. Find unit symbols. >>>
(
clauses: list[Clause], symbols: list[str], model: dict[str, bool | None]
)
| 283 | |
| 284 | |
| 285 | def dpll_algorithm( |
| 286 | clauses: list[Clause], symbols: list[str], model: dict[str, bool | None] |
| 287 | ) -> tuple[bool | None, dict[str, bool | None] | None]: |
| 288 | """ |
| 289 | Returns the model if the formula is satisfiable, else ``None`` |
| 290 | |
| 291 | This has the following steps: |
| 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. |
| 296 | |
| 297 | >>> formula = Formula([Clause(["A4", "A3", "A5'", "A1", "A3'"]), Clause(["A4"])]) |
| 298 | >>> clauses, symbols = generate_parameters(formula) |
| 299 | >>> soln, model = dpll_algorithm(clauses, symbols, {}) |
| 300 | >>> soln |
| 301 | True |
| 302 | >>> model |
| 303 | {'A4': True} |
| 304 | """ |
| 305 | check_clause_all_true = True |
| 306 | for clause in clauses: |
| 307 | clause_check = clause.evaluate(model) |
| 308 | if clause_check is False: |
| 309 | return False, None |
| 310 | elif clause_check is None: |
| 311 | check_clause_all_true = False |
| 312 | continue |
| 313 | |
| 314 | if check_clause_all_true: |
| 315 | return True, model |
| 316 | |
| 317 | try: |
| 318 | pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) |
| 319 | except RecursionError: |
| 320 | print("raises a RecursionError and is") |
| 321 | return None, {} |
| 322 | p = None |
| 323 | if len(pure_symbols) > 0: |
| 324 | p, value = pure_symbols[0], assignment[pure_symbols[0]] |
| 325 | |
| 326 | if p: |
| 327 | tmp_model = model |
| 328 | tmp_model[p] = value |
| 329 | tmp_symbols = list(symbols) |
| 330 | if p in tmp_symbols: |
| 331 | tmp_symbols.remove(p) |
| 332 | return dpll_algorithm(clauses, tmp_symbols, tmp_model) |
| 333 | |
| 334 | unit_symbols, assignment = find_unit_clauses(clauses, model) |
| 335 | p = None |
| 336 | if len(unit_symbols) > 0: |
| 337 | p, value = unit_symbols[0], assignment[unit_symbols[0]] |
| 338 | if p: |
| 339 | tmp_model = model |
| 340 | tmp_model[p] = value |
| 341 | tmp_symbols = list(symbols) |
| 342 | if p in tmp_symbols: |
no test coverage detected