diff --git a/other/davisb_putnamb_logemannb_loveland.py b/other/davisb_putnamb_logemannb_loveland.py index 00068930b89e..b703733593c2 100644 --- a/other/davisb_putnamb_logemannb_loveland.py +++ b/other/davisb_putnamb_logemannb_loveland.py @@ -77,15 +77,21 @@ def evaluate(self, model: dict[str, bool]) -> bool: 3. Return None(unable to complete evaluation) if a literal has no assignment. 4. Compute disjunction of all values assigned in clause. """ + + # 1. literal and complement in clause for literal in self.literals: symbol = literal.rstrip("'") if literal.endswith("'") else literal + "'" if symbol in self.literals: return True + # 2. Any literal is True and + # 3. Any literal is False self.assign(model) for value in self.literals.values(): if value in (True, None): return value + + # 4. disjunction return any(self.literals.values()) @@ -282,6 +288,7 @@ def dpll_algorithm( 2. If some clause in clauses is False, return False. 3. Find pure symbols. 4. Find unit symbols. + 5. recurse on symbol = True or symbol = False >>> formula = Formula([Clause(["A4", "A3", "A5'", "A1", "A3'"]), Clause(["A4"])]) >>> clauses, symbols = generate_parameters(formula) @@ -292,6 +299,9 @@ def dpll_algorithm( >>> model {'A4': True} """ + + # 2. Check any False + # 1. Check All True check_clause_all_true = True for clause in clauses: clause_check = clause.evaluate(model) @@ -304,40 +314,38 @@ def dpll_algorithm( if check_clause_all_true: return True, model - try: - pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) - except RecursionError: - print("raises a RecursionError and is") - return None, {} - P = None - if len(pure_symbols) > 0: + # 3. Pure symbols + pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) + if pure_symbols: P, value = pure_symbols[0], assignment[pure_symbols[0]] + model_true = model.copy() + model_true[P] = value + symbols_without_p = [i for i in symbols if i != P] + return dpll_algorithm(clauses, symbols_without_p, model_true) - if P: - tmp_model = model - tmp_model[P] = value - tmp_symbols = [i for i in symbols] - if P in tmp_symbols: - tmp_symbols.remove(P) - return dpll_algorithm(clauses, tmp_symbols, tmp_model) - + # 4. Unit symbols unit_symbols, assignment = find_unit_clauses(clauses, model) - P = None - if len(unit_symbols) > 0: + if unit_symbols: P, value = unit_symbols[0], assignment[unit_symbols[0]] - if P: - tmp_model = model - tmp_model[P] = value - tmp_symbols = [i for i in symbols] - if P in tmp_symbols: - tmp_symbols.remove(P) - return dpll_algorithm(clauses, tmp_symbols, tmp_model) + if P in symbols: + model_with_p = model.copy() + model_with_p[P] = value + symbols_without_p = [i for i in symbols if i != P] + return dpll_algorithm(clauses, symbols_without_p, model_with_p) + + # 5. recurse through next symbol True and False: P = symbols[0] rest = symbols[1:] - tmp1, tmp2 = model, model - tmp1[P], tmp2[P] = True, False - return dpll_algorithm(clauses, rest, tmp1) or dpll_algorithm(clauses, rest, tmp2) + # duplicate model for update, python passes objects by reference + model_true = model.copy() + model_true[P] = True + model_false = model.copy() + model_false[P] = False + + return dpll_algorithm(clauses, rest, model_true) or dpll_algorithm( + clauses, rest, model_false + ) if __name__ == "__main__": @@ -345,13 +353,38 @@ def dpll_algorithm( doctest.testmod() - formula = generate_formula() - print(f"The formula {formula} is", end=" ") - - clauses, symbols = generate_parameters(formula) - solution, model = dpll_algorithm(clauses, symbols, {}) - - if solution: - print(f"satisfiable with the assignment {model}.") - else: - print("not satisfiable.") + # recursion example: + # {A4} , {A3} , {A2' , A1' , A3 , A4} , {A2'} , {A1' , A1 , A5'} , {A3' , A1} + + # no recursion problem: + clauses_ok = [ + Clause(x) + for x in [ + ["A3'", "A1"], + ["A3"], + ["A4"], + ] + ] + clauses_recursion = [ + Clause(x) + for x in [ + ["A3'", "A1"], + ["A4"], + ["A3"], + ] + ] + + for formula in [ + Formula(clauses_ok), + Formula(clauses_recursion), + generate_formula(), + ]: + print(f"The formula {formula} is", end=" ") + clauses, symbols = generate_parameters(formula) + solution, model = dpll_algorithm(clauses, symbols, {}) + + if solution: + print(f"satisfiable with the assignment {model}.") + else: + print("not satisfiable.") + print()