[Optimization] Add exhausted knowledge threshold to avoid high memory…

… usage and False reduction (#30)

.flake8

@@ -1,5 +1,5 @@
 [flake8]
-ignore = E203, E266, E501, W503
+ignore = E203, E266, E501, W503, C901
 max-line-length = 80
 max-complexity = 18
 select = B,C,E,F,W,T4,B9

pylogic/propositional.py

@@ -381,7 +381,8 @@ def parse(self, clause: Clause) -> Set[CnfClause]:
         return cnf_clauses
 
 
-def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool:  # noqa: C901
+# noqa: C901
+def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000, threshold=10000) -> bool:
     parser = CnfParser()
     alpha_cnf = parser.parse(to_cnf(~alpha))
 
@@ -435,7 +436,7 @@ def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool:  # noqa:
                 interesting_clauses.add(clause)
                 added_knowledge = True
 
-        if not added_knowledge:
+        if not added_knowledge or len(interesting_clauses.clauses) >= threshold:
             return False
 
         it += 1

tests/test_propositional.py

@@ -120,3 +120,24 @@ def test_previous_bug_1():
     kb.add(list(r4))
     kb.add(list(r2))
     assert pl_resolution(kb, alpha) is False
+
+
+def test_debug():
+    parser = CnfParser()
+    result = to_cnf(
+        Variable("B13", True)
+        >> (Variable("P12", True) | Variable("P03", True) | Variable("P32", True))
+    )
+    r4 = parser.parse(result)
+
+    result = to_cnf(
+        Variable("P12", True) & Variable("P03", True) & Variable("B13", True)
+    )
+    r2 = parser.parse(result)
+
+    alpha = ~Variable("P32", True)
+
+    kb = PropLogicKB()
+    kb.add(list(r4))
+    kb.add(list(r2))
+    assert pl_resolution(kb, alpha) is False