From 92e83cf7204703fa2af8fe10557116b521927684 Mon Sep 17 00:00:00 2001 From: Andrew Grangaard Date: Thu, 28 Oct 2021 11:22:36 -0700 Subject: [PATCH 1/6] dpll: add example case for recursion bug The formula {{A3' , A1} , {A3} , {A4}} is satisfiable with the assignment {'A1': True, 'A4': True, 'A3': True}. The formula {{A3' , A1} , {A4} , {A3}} is raises a RecursionError and is not satisfiable. The formula {{A2' , A3} , {A2 , A3 , A5' , A1} , {A3} , {A5 , A1'}} is raises a RecursionError and is not satisfiable. --- other/davisb_putnamb_logemannb_loveland.py | 45 +++++++++++++++++----- 1 file changed, 35 insertions(+), 10 deletions(-) diff --git a/other/davisb_putnamb_logemannb_loveland.py b/other/davisb_putnamb_logemannb_loveland.py index 00068930b89e..d231c77db52d 100644 --- a/other/davisb_putnamb_logemannb_loveland.py +++ b/other/davisb_putnamb_logemannb_loveland.py @@ -345,13 +345,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() From 809ec7c61b89413059f1e6a17f9602a80a661b48 Mon Sep 17 00:00:00 2001 From: Andrew Grangaard Date: Thu, 28 Oct 2021 11:29:59 -0700 Subject: [PATCH 2/6] dpll: add comment for each step --- other/davisb_putnamb_logemannb_loveland.py | 13 +++++++++++++ 1 file changed, 13 insertions(+) diff --git a/other/davisb_putnamb_logemannb_loveland.py b/other/davisb_putnamb_logemannb_loveland.py index d231c77db52d..4bda268c16ec 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()) @@ -292,6 +298,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,6 +313,7 @@ def dpll_algorithm( if check_clause_all_true: return True, model + # 3. Pure symbols try: pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) except RecursionError: @@ -321,6 +331,7 @@ def dpll_algorithm( 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: @@ -332,6 +343,8 @@ def dpll_algorithm( if P in tmp_symbols: tmp_symbols.remove(P) return dpll_algorithm(clauses, tmp_symbols, tmp_model) + + # 5. recurse through next symbol True and False: P = symbols[0] rest = symbols[1:] tmp1, tmp2 = model, model From a6ab187baa9f4df53b8b69e10c0aa144e3f3beee Mon Sep 17 00:00:00 2001 From: Andrew Grangaard Date: Thu, 28 Oct 2021 11:33:15 -0700 Subject: [PATCH 3/6] dpll: python check on array length --- other/davisb_putnamb_logemannb_loveland.py | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) diff --git a/other/davisb_putnamb_logemannb_loveland.py b/other/davisb_putnamb_logemannb_loveland.py index 4bda268c16ec..f4f1bb261c2b 100644 --- a/other/davisb_putnamb_logemannb_loveland.py +++ b/other/davisb_putnamb_logemannb_loveland.py @@ -319,11 +319,9 @@ def dpll_algorithm( except RecursionError: print("raises a RecursionError and is") return None, {} - P = None - if len(pure_symbols) > 0: - P, value = pure_symbols[0], assignment[pure_symbols[0]] - if P: + if pure_symbols: + P, value = pure_symbols[0], assignment[pure_symbols[0]] tmp_model = model tmp_model[P] = value tmp_symbols = [i for i in symbols] @@ -333,10 +331,8 @@ def dpll_algorithm( # 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] From fe86ce05d904932d822efb7fb5c23da5a49197e0 Mon Sep 17 00:00:00 2001 From: Andrew Grangaard Date: Thu, 28 Oct 2021 11:44:25 -0700 Subject: [PATCH 4/6] dpll: fixes algo bug, recursion both went down False arm + copies model to allow independent mutation. + python assigns by reference. both tmp models mutated the original model and the second over wrote the first. Recursion was going down the same branch each time. --- other/davisb_putnamb_logemannb_loveland.py | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/other/davisb_putnamb_logemannb_loveland.py b/other/davisb_putnamb_logemannb_loveland.py index f4f1bb261c2b..58451eb3c736 100644 --- a/other/davisb_putnamb_logemannb_loveland.py +++ b/other/davisb_putnamb_logemannb_loveland.py @@ -288,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) @@ -343,7 +344,7 @@ def dpll_algorithm( # 5. recurse through next symbol True and False: P = symbols[0] rest = symbols[1:] - tmp1, tmp2 = model, model + tmp1, tmp2 = model.copy(), model.copy() tmp1[P], tmp2[P] = True, False return dpll_algorithm(clauses, rest, tmp1) or dpll_algorithm(clauses, rest, tmp2) From 6197fc7ab0bf764abb72607ccfbeeac8eefefd47 Mon Sep 17 00:00:00 2001 From: Andrew Grangaard Date: Thu, 28 Oct 2021 11:35:47 -0700 Subject: [PATCH 5/6] dpll: Fixes recursion problem by checking if unit_symbol remains in unevaluated symbols --- other/davisb_putnamb_logemannb_loveland.py | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/other/davisb_putnamb_logemannb_loveland.py b/other/davisb_putnamb_logemannb_loveland.py index 58451eb3c736..e5b3a5fcc700 100644 --- a/other/davisb_putnamb_logemannb_loveland.py +++ b/other/davisb_putnamb_logemannb_loveland.py @@ -315,15 +315,10 @@ def dpll_algorithm( return True, model # 3. Pure symbols - try: - pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) - except RecursionError: - print("raises a RecursionError and is") - return None, {} - + pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) if pure_symbols: P, value = pure_symbols[0], assignment[pure_symbols[0]] - tmp_model = model + tmp_model = model.copy() tmp_model[P] = value tmp_symbols = [i for i in symbols] if P in tmp_symbols: @@ -334,12 +329,13 @@ def dpll_algorithm( unit_symbols, assignment = find_unit_clauses(clauses, model) if unit_symbols: P, value = unit_symbols[0], assignment[unit_symbols[0]] - 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: + 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) # 5. recurse through next symbol True and False: P = symbols[0] From a42c6a41cee4187805769a90a71956ce031efd8a Mon Sep 17 00:00:00 2001 From: Andrew Grangaard Date: Thu, 28 Oct 2021 12:04:10 -0700 Subject: [PATCH 6/6] dpll: uses descriptive var names to show intent. pythonic copy + filter out P during the copy rather than removing after the copy is both clearer and marginally more efficient. 1.5n -> n --- other/davisb_putnamb_logemannb_loveland.py | 32 ++++++++++++---------- 1 file changed, 17 insertions(+), 15 deletions(-) diff --git a/other/davisb_putnamb_logemannb_loveland.py b/other/davisb_putnamb_logemannb_loveland.py index e5b3a5fcc700..b703733593c2 100644 --- a/other/davisb_putnamb_logemannb_loveland.py +++ b/other/davisb_putnamb_logemannb_loveland.py @@ -318,32 +318,34 @@ def dpll_algorithm( pure_symbols, assignment = find_pure_symbols(clauses, symbols, model) if pure_symbols: P, value = pure_symbols[0], assignment[pure_symbols[0]] - tmp_model = model.copy() - 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) + 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) # 4. Unit symbols unit_symbols, assignment = find_unit_clauses(clauses, model) if unit_symbols: P, value = unit_symbols[0], assignment[unit_symbols[0]] if P in symbols: - 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) + 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.copy(), model.copy() - 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__":