Discarding Order-Dependent Subalgebras (#14)

model.py

@@ -103,18 +103,34 @@ def binary_function_str(f: ModelFunction) -> str:
 
 Interpretation = Dict[Operation, ModelFunction]
 
+class OrderTable:
+    def __init__(self):
+        self.ordering = set()
+
+    def add(self, x, y):
+        """
+        Add x <= y
+        """
+        self.ordering.add((x, y))
+
+    def is_lt(self, x, y):
+        return (x, y) in self.ordering
+
+
 class Model:
     def __init__(
             self,
             carrier_set: Set[ModelValue],
             logical_operations: Set[ModelFunction],
             designated_values: Set[ModelValue],
+            ordering: Optional[OrderTable] = None,
             name: Optional[str] = None
     ):
         assert designated_values <= carrier_set
         self.carrier_set = carrier_set
         self.logical_operations = logical_operations
         self.designated_values = designated_values
+        self.ordering = ordering
         self.name = str(abs(hash((
             frozenset(carrier_set),
             frozenset(logical_operations),

parse_magic.py

@@ -6,7 +6,7 @@ Assumes the base logic is R with no extra connectives
 import re
 from typing import TextIO, List, Optional, Tuple, Set, Dict
 
-from model import Model, ModelValue, ModelFunction
+from model import Model, ModelValue, ModelFunction, OrderTable
 from logic import (
     Implication,
     Conjunction,
@@ -65,6 +65,7 @@ class ModelBuilder:
         self.size : int = 0
         self.carrier_set : Set[ModelValue] = set()
         self.mnegation: Optional[ModelFunction] = None
+        self.ordering: Optional[OrderTable] = None
         self.mconjunction: Optional[ModelFunction] = None
         self.mdisjunction: Optional[ModelFunction] = None
         self.designated_values: Set[ModelValue] = set()
@@ -278,7 +279,8 @@ def process_orders(infile: SourceFile, current_model_parts: ModelBuilder) -> boo
     if result is None:
         return False
 
-    mconjunction, mdisjunction = result
+    ordering, mconjunction, mdisjunction = result
+    current_model_parts.ordering = ordering
     current_model_parts.mconjunction = mconjunction
     current_model_parts.mdisjunction = mdisjunction
 
@@ -334,7 +336,7 @@ def process_model(model_name: str, mp: ModelBuilder,  solutions: List[Tuple[Mode
     assert mp.mimplication is not None
 
     logical_operations = { mp.mimplication }
-    model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name)
+    model = Model(mp.carrier_set, logical_operations, mp.designated_values, ordering=mp.ordering, name=model_name)
     interpretation = {
         Implication: mp.mimplication
     }
@@ -466,7 +468,7 @@ def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: Mode
         if not invalid:
             return c
 
-def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]:
+def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[OrderTable, ModelFunction, ModelFunction]]:
     """
     Parse the line representing the ordering table
     """
@@ -478,6 +480,7 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun
 
     assert len(table) == (size + 1)**2, f"Order table doesn't match expected size at line {infile.current_line}"
 
+    ordering = OrderTable()
     omapping = {}
     table_i = 0
 
@@ -486,6 +489,8 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun
         for j in range(size + 1):
             y = mvalue_from_index(j)
             omapping[(x, y)] = table[table_i] == '1'
+            if table[table_i] == '1':
+                ordering.add(x, y)
             table_i += 1
 
     cmapping = {}
@@ -514,7 +519,7 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun
     mconjunction = ModelFunction(2, cmapping, "∧")
     mdisjunction = ModelFunction(2, dmapping, "∨")
 
-    return mconjunction, mdisjunction
+    return ordering, mconjunction, mdisjunction
 
 def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[ModelValue]]:
     """

vsp.py

@@ -6,7 +6,7 @@ from itertools import chain, combinations, product
 from typing import List, Optional, Set, Tuple
 from common import set_to_str
 from model import (
-    Model, model_closure, ModelFunction, ModelValue
+    Model, model_closure, ModelFunction, ModelValue, OrderTable
 )
 
 def preseed(
@@ -78,6 +78,15 @@ def find_bottom(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction],
     print("[Warning] Failed to find the bottom of the lattice")
     return None
 
+def order_dependent(subalgebra1: Set[ModelValue], subalegbra2: Set[ModelValue], ordering: OrderTable):
+    """
+    Returns true if there exists a value in subalgebra1 that's less than a value in subalgebra2
+    """
+    for x in subalgebra1:
+        for y in subalegbra2:
+            if ordering.is_lt(x, y):
+                return True
+    return False
 
 class VSP_Result:
     def __init__(
@@ -97,7 +106,10 @@ Subalgebra 1: {set_to_str(self.subalgebra1)}
 Subalgebra 2: {set_to_str(self.subalgebra2)}
 """
 
-def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[ModelFunction] = None, mdisjunction: Optional[ModelFunction] = None) -> VSP_Result:
+def has_vsp(model: Model, impfunction: ModelFunction,
+            mconjunction: Optional[ModelFunction] = None,
+            mdisjunction: Optional[ModelFunction] = None,
+            mnegation: Optional[ModelFunction] = None) -> VSP_Result:
     """
     Checks whether a model has the variable
     sharing property.
@@ -110,6 +122,8 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod
     if len(model.designated_values) == 1:
         return VSP_Result(False, model.name)
 
+    assert model.ordering is not None, "Expected ordering table in model"
+
     # Compute I the set of tuples (x, y) where
     # x -> y does not take a designiated value
     I: Set[Tuple[ModelValue, ModelValue]] = set()
@@ -167,6 +181,13 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod
         if bottom is not None and bottom in xs:
             continue
 
+        # NOTE: Optimization
+        # If the subalgebras are order-dependent, skip this pair
+        if order_dependent(xs, ys, model.ordering):
+            continue
+        if mnegation is not None and order_dependent(ys, xs, model.ordering):
+            continue
+
         # Compute the closure of all operations
         # with just the xs
         carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, bottom)

vspursuer.py

@@ -3,7 +3,7 @@ from os import cpu_count
 import argparse
 import multiprocessing as mp
 
-from logic import Conjunction, Disjunction, Implication
+from logic import Conjunction, Disjunction, Negation, Implication
 from parse_magic import SourceFile, parse_matrices
 from vsp import has_vsp, VSP_Result
 
@@ -28,7 +28,7 @@ if __name__ == "__main__":
 
     # NOTE: When subprocess gets spawned, the logical operations will
     # have a different memory address than what's expected in interpretation.
-    # This will make it so that we can pass the model functions directly instead.
+    # Therefore, we need to pass the model functions directly instead.
     solutions_expanded = []
     for model, interpretation in solutions:
         # If skip_to is defined, then don't process models
@@ -40,14 +40,15 @@ if __name__ == "__main__":
         impfunction = interpretation[Implication]
         mconjunction = interpretation.get(Conjunction)
         mdisjunction = interpretation.get(Disjunction)
-        solutions_expanded.append((model, impfunction, mconjunction, mdisjunction))
+        mnegation = interpretation.get(Negation)
+        solutions_expanded.append((model, impfunction, mconjunction, mdisjunction, mnegation))
 
     num_has_vsp = 0
     num_cpu = args.get("c", max(cpu_count() - 2, 1))
     with mp.Pool(processes=num_cpu) as pool:
         results = [
-            pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction,))
-            for model, impfunction, mconjunction, mdisjunction in solutions_expanded
+            pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction, mnegation))
+            for model, impfunction, mconjunction, mdisjunction, mnegation in solutions_expanded
         ]
 
         for i, result in enumerate(results):