Fixes recursion exception in davisb_putnamb_logemann_loveland

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,54 +314,77 @@ 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__":
  import doctest
 
  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()