Code optimizations. added get_level and evaluate methods

clause.py

@@ -2,17 +2,39 @@
 from bitarray import bitarray
 
 class Clause:
-    def __init__(self, str_signature: str) -> None:
-        if not str_signature or any(c not in ('0','1') for c in str_signature):
-            raise ValueError("Invalid signature!")
-        self.cardinality = len(str_signature)
-        self.signature = bitarray(str_signature)
+    def __init__(self, signature, size=None) -> None:
+        if not signature:
+            raise ValueError('Invalid signature!')
+        if isinstance(signature, str):
+            if any(c not in ('0','1') for c in signature) or \
+               (size and size != len(signature)):
+                raise ValueError('Invalid signature!')
+            self.cardinality = len(signature)
+            self.signature = bitarray(signature)
+        elif isinstance(signature, bitarray):
+            if size and size != len(signature):
+                raise ValueError('Invalid signature!')
+            self.cardinality = len(signature)
+            self.signature = signature.copy()
+        elif isinstance(signature, list):
+            if not size or not isinstance(size, int) or size < 1 or \
+            any((i < 1 or i > size) for i in signature):
+             raise ValueError('Invalid signature!')
+            self.cardinality = size
+            self.signature = bitarray('0' * size)
+            for i in signature:
+                self.signature[i - 1] = True
 
     def clone_add(self, lit: int) -> 'Clause':
-        c = Clause(self.signature.to01())
+        c = Clause(self.signature)
         c.signature[lit] = True
         return c
-
+
+    def clone_rm(self, lit: int) -> 'Clause':
+        c = Clause(self.signature)
+        c.signature[lit] = False
+        return c
+
     def get_size(self) -> int:
         return self.cardinality
 
@@ -22,82 +44,70 @@ def get_signature(self) -> bitarray:
     def get_order(self) -> int:
         return self.signature.count()
 
-    def has_some_literal(self, c: 'Clause') -> bool:
-        return any(self.signature[i] and c.signature[i] \
-                   for i in range(self.cardinality))
-
-    def missing_literals(self) -> list[int]:
+    def get_off_literals(self) -> list[int]:
         return [i for i in range(self.cardinality) if not self.signature[i]]
 
+    def get_on_literals(self) -> list[int]:
+        return [i for i in range(self.cardinality) if self.signature[i]]
+
     def __hash__(self) -> int:
         """ Hash function for Clause using the signature bit """
         return hash(self.signature.tobytes())
 
     def get_containing(self, sClauses: Set['Clause']) -> Set['Clause']:
-        containing = set()
-        for s in sClauses:
-            if self <= s:
-                containing.add(s)
-        return containing
+        return { s for s in sClauses if self <= s }
 
     def get_contained(self, sClauses: Set['Clause']) -> Set['Clause']:
-        contained = set()
-        for s in sClauses:
-            if s != self and s <= self:
-                contained.add(s)
-        return contained
-
+        return { s for s in sClauses if s < self }
+
     def __eq__(self, other) -> bool:
         return isinstance(other, Clause) and \
                 self.cardinality == other.cardinality and \
                 self.signature == other.signature
 
+    def __ne__(self, other) -> bool:
+        return not self == other
+
     def __ge__(self, c: 'Clause') -> bool:
         if self.cardinality != c.cardinality:
             raise ValueError("Clauses must have the same cardinality!")
         # with list comprehension
-        return all((self.signature[i] or not c.signature[i]) for i in range(self.cardinality))
+        return (~self.signature & c.signature).count() == 0
 
     def __gt__(self, c: 'Clause') -> bool:
         if self.cardinality != c.cardinality:
             raise ValueError("Clauses must have the same cardinality!")
-        return self >= c and not self == c
+        return self >= c and self != c
 
     def __le__(self, c: 'Clause') -> bool:
         if self.cardinality != c.cardinality:
             raise ValueError("Clauses must have the same cardinality!")
-        return c >= self
+        return (~c.signature & self.signature).count() == 0
 
     def __lt__(self, c: 'Clause') -> bool:
         if self.cardinality != c.cardinality:
             raise ValueError("Clauses must have the same cardinality!")
-        return c > self
+        return self <= c and self != c
 
     def is_independent(self, c: 'Clause') -> bool:
         if self.cardinality != c.cardinality:
             raise ValueError("Clauses must have the same cardinality!")
         return not self>=c and not self<=c
 
     def get_subsets(self) -> Set['Clause']:
-        subsets = set()
-        for i in range(self.cardinality):
-            if self.signature[i]:
-                c = Clause(self.signature.to01())
-                c.signature[i] = False
-                subsets.add(c)
-        return subsets
-
+        return { self.clone_rm(l) for l in self.get_on_literals() }
+
     def get_supersets(self) -> Set['Clause']:
-        supersets = set()
-        for i in range(self.cardinality):
-            if not self.signature[i]:
-                c = Clause(self.signature.to01())
-                c.signature[i] = True
-                supersets.add(c)
-        return supersets
-
+        return { self.clone_add(l) for l in self.get_off_literals() }
+
     def __str__(self) -> str:
         return "{" + ",".join(str(i + 1) for i in range(self.cardinality) if self.signature[i]) + "}"
 
     def __repr__(self) -> str:
         return str(self)
+
+    def evaluate(self, signs: bitarray, values: bitarray) -> bool:
+        # (signs XAND values) AND clause
+        # number of 1's must be equal to the number of literals in clause
+        return ((~(signs ^ values)) & self.signature).count() == self.signature.count()
+

function.py

@@ -50,14 +50,10 @@ def is_consistent(self) -> bool:
         return self.consistent
 
     def update_consistency(self) -> None:
-        self.consistent = self.has_independent_clauses() and self.is_cover()
+        self.consistent = self.is_independent() and self.is_cover()
 
-    def has_independent_clauses(self) -> bool:
-        for c1 in self.clauses:
-            for c2 in self.clauses:
-                if c1 != c2 and not c1.is_independent(c2):
-                    return False
-        return True
+    def is_independent(self) -> bool:
+        return all(c1.is_independent(c2) for c1 in self.clauses for c2 in self.clauses if c1 != c2)
 
     def is_cover(self) -> bool:
         bcover = bitarray('0'*self.nvars)
@@ -82,3 +78,23 @@ def __str__(self) -> str:
 
     def __repr__(self) -> str:
         return str(self)
+
+    def evaluate(self, signs: bitarray, values: bitarray) -> bool:
+        return any(c.evaluate(signs, values) for c in self.clauses)
+
+    def get_level(self) -> list[int]:
+        return sorted([(self.nvars - c.get_order()) for c in self.clauses], reverse=True)
+
+    def level_cmp(self, other: 'Function') -> int:
+        lself, lother = self.get_level(), other.get_level()
+        szself, szother = len(lself), len(lother)
+
+        # Compare element by element
+        for i in range(min(szself, szother)):
+            if   lself[i] > lother[i]: return 1
+            elif lself[i] < lother[i]: return -1
+
+        if   szself  < szother: return -1
+        elif szself == szother: return  0
+        else:                   return  1
+

hassediagram.py

@@ -5,16 +5,16 @@
 
 class HasseDiagram:
     # Dedeking number: number of monotone Boolean functions of n variables:
-    #   https://oeis.org/A000372
+    #  https://oeis.org/A000372
     # Number of monotone non-degenerate Boolean functions of n variables:
-    # n=2 ->                                                       2 functions
-    # n=3 ->                                                       9 functions
-    # n=4 ->                                                     114 functions
-    # n=5 ->                                                   6 894 functions
-    # n=6 ->                                               7 785 062 functions
-    # n=7 ->                                       2 414 627 396 434 functions
-    # n=8 ->                          56 130 437 209 370 320 359 966 functions
-    # n=9 -> 286 386 577 668 298 410 623 295 216 696 338 374 471 993 functions
+    #  n=2 ->                                                       2 functions
+    #  n=3 ->                                                       9 functions
+    #  n=4 ->                                                     114 functions
+    #  n=5 ->                                                   6 894 functions
+    #  n=6 ->                                               7 785 062 functions
+    #  n=7 ->                                       2 414 627 396 434 functions
+    #  n=8 ->                          56 130 437 209 370 320 359 966 functions
+    #  n=9 -> 286 386 577 668 298 410 623 295 216 696 338 374 471 993 functions
 
     def __init__(self, nvars: int) -> None:
         self.nvars = nvars
@@ -42,10 +42,7 @@ def get_f_parents(self, f: 'Function') -> Tuple[Set['Function'], Set['Function']
         sC = self.powerset.get_maximal(self.powerset.get_independent(f.clauses))
 
         # Add all parents from the 1st rule
-        for c in sC:
-            fp = f.clone_rm_add(set(), {c})
-            s1Parents.add(fp)
-            #print('fp:',fp, 'R1')
+        s1Parents = { f.clone_rm_add(set(), { c }) for c in sC }
 
         # Get maximal dominated clauses
         lD = [d for d in self.powerset.get_maximal( \
@@ -90,7 +87,7 @@ def get_f_children(self, f: 'Function') -> Tuple[Set['Function'], Set['Function'
             bToMerge, bExtendable = False, False
             # Child function to be extended with: s \cup {l_i}
             fs = f.clone_rm_add({s},set())
-            for l in s.missing_literals():
+            for l in s.get_off_literals():
                 sl = s.clone_add(l)
                 sAbsorbed = sl.get_contained(f.clauses)
                 if len(sAbsorbed) == 1:
@@ -116,7 +113,7 @@ def get_f_children(self, f: 'Function') -> Tuple[Set['Function'], Set['Function'
             while lmergeable:
                 c = lmergeable[-1]
                 fMergeable = Function(f.get_size(), set(lmergeable))
-                for l in c.missing_literals():
+                for l in c.get_off_literals():
                     cl = c.clone_add(l)
                     sAbsorbed = cl.get_contained(fMergeable.clauses)
                     if len(sAbsorbed) == 2:

powerset.py

@@ -46,7 +46,7 @@ def get_dominant_directly(self, s_clauses: Set['Clause']) -> Set['Clause']:
         return s_dominant
 
     def get_dominated_recursively(self, c: 'Clause', s_seen: Set['Clause']) -> Set['Clause']:
-        for c_subset in self.subset_clauses.get(c):
+        for c_subset in self.subset_clauses.get(c, set()):
             if c_subset not in s_seen:
                 s_seen.add(c_subset)
                 s_seen.update(self.get_dominated_recursively(c_subset, s_seen))
@@ -70,26 +70,10 @@ def get_independent(self, clauses: Set['Clause']) -> Set['Clause']:
         return s_diff
 
     def get_minimal(self, s_clauses: Set['Clause']) -> Set['Clause']:
-        l_clauses = list(s_clauses)
-        s_minimal = set()
-        for i in range(len(l_clauses)):
-            dominates = False
-            for j in range(len(l_clauses)):
-                if i != j and l_clauses[i] >= l_clauses[j]:
-                    dominates = True
-                    break
-            if not dominates:
-                s_minimal.add(l_clauses[i])
-        return s_minimal
+        return { s1 for s1 in s_clauses if not any( s1 != s2 and s2 <= s1 for s2 in s_clauses) }
 
     def get_maximal(self, s_clauses: Set['Clause']) -> Set['Clause']:
-        l_clauses = list(s_clauses)
-        s_maximal = set()
-        for i in range(len(s_clauses)):
-            if any([i != j and l_clauses[j]>=l_clauses[i] for j in range(len(s_clauses))]):
-                continue
-            s_maximal.add(l_clauses[i])
-        return s_maximal
+        return { s1 for s1 in s_clauses if not any( s1 != s2 and s2 >= s1 for s2 in s_clauses) }
 
     def __str__(self) -> str:
         s = ""