[Optimization] Trying to fix inconsistencies with my previous impleme…

…ntation (#30)

pylogic/propositional.py

@@ -1,6 +1,6 @@
 from enum import Enum
 from abc import ABC, abstractmethod
-from typing import List, Optional, Set, Tuple
+from typing import DefaultDict, List, Optional, Set, Tuple
 from functools import singledispatchmethod
 from collections import defaultdict
 
@@ -294,6 +294,13 @@ def __hash__(self) -> int:
     def __len__(self) -> int:
         return len(self._literals)
 
+    def issubset(self, other) -> bool:
+        subset = True
+        for literal in self.literals:
+            if literal not in other.literals:
+                subset = False
+        return subset
+
 
 class PropLogicKB:
     def __init__(self, clauses: Optional[Set[CnfClause]] = None):
@@ -387,7 +394,7 @@ def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool:  # noqa:
 
     it = 1
     while it <= maxit:
-        literal_clause_map = defaultdict(list)  # type: ignore
+        literal_clause_map: DefaultDict[Variable, List[CnfClause]] = defaultdict(list)
         for clause in interesting_clauses.clauses:
             for literal in clause.literals:
                 literal_clause_map[literal].append(clause)  # type: ignore
@@ -407,7 +414,7 @@ def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool:  # noqa:
             try:
                 res = ci.resolve(cj, literal)
             except UselessCnfClauseException:
-                continue
+                pass
             if res.is_empty_clause():
                 return True
             else:
@@ -417,11 +424,11 @@ def pl_resolution(kb: PropLogicKB, alpha: Clause, maxit=1000) -> bool:  # noqa:
         for clause in new_knowledge.clauses:
             any_subset = False
             for old_clause in interesting_clauses.clauses:
-                if set(old_clause.literals).issubset(set(clause.literals)):
+                if old_clause.issubset(clause):
                     any_subset = True
 
             for old_clause in kb.clauses:
-                if set(old_clause.literals).issubset(set(clause.literals)):
+                if old_clause.issubset(clause):
                     any_subset = True
 
             if not any_subset:

tests/test_propositional.py

@@ -102,3 +102,21 @@ def test_pl_resolution():
     clauses = parser.parse(cnf)
     kb = PropLogicKB(clauses)
     assert pl_resolution(kb, Variable("P12", False))
+
+
+def test_previous_bug_1():
+    parser = CnfParser()
+    result = to_cnf(
+        Variable("B21", True) >> (Variable("P22", True) | Variable("P31", True))
+    )
+    r4 = parser.parse(result)
+
+    result = to_cnf(~Variable("B11", True))
+    r2 = parser.parse(result)
+
+    alpha = ~Variable("P12", True)
+
+    kb = PropLogicKB()
+    kb.add(list(r4))
+    kb.add(list(r2))
+    assert pl_resolution(kb, alpha) is False