From 18c2bcb67393ae402a0627435ef83762e7e337b5 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 9 Dec 2025 10:26:15 -0500
Subject: [PATCH 01/10] Changed from model to matrix

---
 model.py     | 2 +-
 vsp.py       | 4 ++--
 vspursuer.py | 4 ++--
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/model.py b/model.py
index 429a26e..615e6ee 100644
--- a/model.py
+++ b/model.py
@@ -202,7 +202,7 @@ class Model:
 
     def __str__(self):
         result = ("=" * 25) + f"""
-Model Name: {self.name}
+Matrix Name: {self.name}
 Carrier Set: {set_to_str(self.carrier_set)}
 Designated Values: {set_to_str(self.designated_values)}
 """
diff --git a/vsp.py b/vsp.py
index 034005f..85d912e 100644
--- a/vsp.py
+++ b/vsp.py
@@ -21,8 +21,8 @@ class VSP_Result:
 
     def __str__(self):
         if not self.has_vsp:
-            return f"Model {self.model_name} does not have the variable sharing property."
-        return f"""Model {self.model_name} has the variable sharing property.
+            return f"Matrix {self.model_name} does not have the variable sharing property."
+        return f"""Matrix {self.model_name} has the variable sharing property.
 Subalgebra 1: {set_to_str(self.subalgebra1)}
 Subalgebra 2: {set_to_str(self.subalgebra2)}
 """
diff --git a/vspursuer.py b/vspursuer.py
index d9d9e53..5914a5f 100755
--- a/vspursuer.py
+++ b/vspursuer.py
@@ -168,7 +168,7 @@ def multi_process_runner(num_cpu: int, data_file_path: str, skip_to: Optional[st
         if vsp_result.has_vsp:
             num_has_vsp += 1
 
-    print_with_timestamp(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP")
+    print_with_timestamp(f"Tested {num_tested} matrices, {num_has_vsp} of which satisfy VSP")
 
 def single_process_runner(data_file_path: str, skip_to: Optional[str]):
     num_tested = 0
@@ -189,7 +189,7 @@ def single_process_runner(data_file_path: str, skip_to: Optional[str]):
         if vsp_result.has_vsp:
             num_has_vsp += 1
 
-    print_with_timestamp(f"Tested {num_tested} models, {num_has_vsp} of which satisfy VSP")
+    print_with_timestamp(f"Tested {num_tested} matrices, {num_has_vsp} of which satisfy VSP")
 
 
 if __name__ == "__main__":

From f799a1ff5dedb254aeac11e5d5b10ff25628f43f Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Fri, 12 Dec 2025 11:36:21 -0500
Subject: [PATCH 02/10] Skip model sizes 2-5 and 7 when conjunction,
 disjunction, and negation are defined

---
 utils/compare_vsp_results.py |  8 ++++----
 vsp.py                       |  6 +++++-
 vspursuer.py                 | 17 +++++++++--------
 3 files changed, 18 insertions(+), 13 deletions(-)

diff --git a/utils/compare_vsp_results.py b/utils/compare_vsp_results.py
index 82c587d..aa16aa5 100644
--- a/utils/compare_vsp_results.py
+++ b/utils/compare_vsp_results.py
@@ -56,9 +56,9 @@ if __name__ == "__main__":
     extra_models1 = 0
     extra_models2 = 0
 
-    for model, impfunction, negation_defined in solutions1:
+    for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions1:
         total_models1 += 1
-        vsp_result = has_vsp(model, impfunction, negation_defined)
+        vsp_result = has_vsp(model, impfunction, negation_defined, conjunction_disjunction_defined)
 
         if vsp_result.has_vsp:
             good_models1 += 1
@@ -83,9 +83,9 @@ if __name__ == "__main__":
 
 
     # Check through the remaining models in the second set
-    for model, impfunction, negation_defined in solutions2:
+    for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions2:
         total_models2 += 1
-        vsp_result = has_vsp(model, impfunction, negation_defined)
+        vsp_result = has_vsp(model, impfunction, negation_defined, conjunction_disjunction_defined)
 
         if not vsp_result.has_vsp:
             bad_models2 += 1
diff --git a/vsp.py b/vsp.py
index 85d912e..2d3575c 100644
--- a/vsp.py
+++ b/vsp.py
@@ -28,7 +28,7 @@ Subalgebra 2: {set_to_str(self.subalgebra2)}
 """
 
 def has_vsp(model: Model, impfunction: ModelFunction,
-            negation_defined: bool) -> VSP_Result:
+            negation_defined: bool, conjunction_disjunction_defined: bool) -> VSP_Result:
     """
     Checks whether a model has the variable
     sharing property.
@@ -38,6 +38,10 @@ def has_vsp(model: Model, impfunction: ModelFunction,
     if len(model.designated_values) == 1:
         return VSP_Result(False, model.name)
 
+    if len(model.carrier_set) in [2,3,4,5,7] \
+        and conjunction_disjunction_defined and negation_defined:
+        return VSP_Result(False, model.name)
+
     assert model.ordering is not None, "Expected ordering table in model"
 
     top = model.ordering.top()
diff --git a/vspursuer.py b/vspursuer.py
index 5914a5f..67e73fa 100755
--- a/vspursuer.py
+++ b/vspursuer.py
@@ -6,7 +6,7 @@ from queue import Empty as QueueEmpty
 import argparse
 import multiprocessing as mp
 
-from logic import Negation, Implication, Operation
+from logic import Conjunction, Disjunction, Implication, Negation, Operation
 from model import Model, ModelFunction
 from parse_magic import SourceFile, parse_matrices
 from vsp import has_vsp, VSP_Result
@@ -36,13 +36,14 @@ def restructure_solutions(solutions: Iterator[Tuple[Model, Dict[Operation, Model
         # NOTE: Implication must be defined, the rest may not
         impfunction = interpretation[Implication]
         negation_defined = Negation in interpretation
-        yield (model, impfunction, negation_defined)
+        conjunction_disjunction_defined = (Conjunction in interpretation) and (Disjunction in interpretation)
+        yield (model, impfunction, negation_defined, conjunction_disjunction_defined)
 
-def has_vsp_plus_model(model, impfunction, negation_defined) -> Tuple[Optional[Model], VSP_Result]:
+def has_vsp_plus_model(model, impfunction, negation_defined, conjunction_disjunction_defined) -> Tuple[Optional[Model], VSP_Result]:
     """
     Wrapper which also stores the models along with its vsp result
     """
-    vsp_result = has_vsp(model, impfunction, negation_defined)
+    vsp_result = has_vsp(model, impfunction, negation_defined, conjunction_disjunction_defined)
     # NOTE: Memory optimization - Don't return model if it doesn't have VSP
     model = model if vsp_result.has_vsp else None
     return (model, vsp_result)
@@ -61,8 +62,8 @@ def worker_vsp(task_queue: mp.Queue, result_queue: mp.Queue):
             # If sentinal value, break
             if task is None:
                 break
-            (model, impfunction, negation_defined) = task
-            result = has_vsp_plus_model(model, impfunction, negation_defined)
+            (model, impfunction, negation_defined, conjunction_disjunction_defined) = task
+            result = has_vsp_plus_model(model, impfunction, negation_defined, conjunction_disjunction_defined)
             result_queue.put(result)
     finally:
         # Either an exception occured or the worker finished
@@ -178,8 +179,8 @@ def single_process_runner(data_file_path: str, skip_to: Optional[str]):
     solutions = parse_matrices(SourceFile(data_file))
     solutions = restructure_solutions(solutions, skip_to)
 
-    for model, impfunction, negation_defined in solutions:
-        model, vsp_result = has_vsp_plus_model(model, impfunction, negation_defined)
+    for model, impfunction, negation_defined, conjunction_disjunction_defined in solutions:
+        model, vsp_result = has_vsp_plus_model(model, impfunction, negation_defined, conjunction_disjunction_defined)
         print_with_timestamp(vsp_result)
         num_tested += 1
 

From 51c26dd9fcab87f7da562c3419fa4e600b37e8c9 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Fri, 12 Dec 2025 14:49:32 -0500
Subject: [PATCH 03/10] Optimization in computing meets and joins

---
 model.py | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/model.py b/model.py
index 615e6ee..6272d48 100644
--- a/model.py
+++ b/model.py
@@ -129,6 +129,12 @@ class OrderTable:
 
         candidates = X.intersection(Y)
 
+        if not candidates:
+            return None
+
+        if len(candidates) == 1:
+            return next(iter(candidates))
+
         # Grab all elements greater than each of the candidates
         candidate_ge_maps = (self.ge_map[candidate] for candidate in candidates)
         common_ge_values = reduce(set.intersection, candidate_ge_maps)
@@ -147,6 +153,12 @@ class OrderTable:
 
         candidates = X.intersection(Y)
 
+        if not candidates:
+            return None
+
+        if len(candidates) == 1:
+            return next(iter(candidates))
+
         # Grab all elements smaller than each of the candidates
         candidate_le_maps = (self.le_map[candidate] for candidate in candidates)
         common_le_values = reduce(set.intersection, candidate_le_maps)

From f8eca388d4fe30359c73d2aa94342e7b7a7cdce9 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 27 Jan 2026 11:23:47 -0500
Subject: [PATCH 04/10] Some comment changes

---
 smt.py | 5 ++---
 vsp.py | 2 +-
 2 files changed, 3 insertions(+), 4 deletions(-)

diff --git a/smt.py b/smt.py
index 0be7af6..3946975 100644
--- a/smt.py
+++ b/smt.py
@@ -230,7 +230,7 @@ class SMTLogicEncoder:
             for smt_elem in self.smt_carrier_set
         }
 
-        # Exclude operation function mappings
+        # Iterate over all logical operations
         for model_func in model.logical_operations:
             operation = Operation(model_func.operation_name, model_func.arity)
             smt_func = self.operation_function_map[operation]
@@ -239,10 +239,9 @@ class SMTLogicEncoder:
                 smt_inputs = tuple(model_value_to_smt[inp] for inp in inputs)
                 smt_output = model_value_to_smt[output]
 
-                # For future models the input->output mapping may differ
+                # It may be the case that the output of f(input) differs
                 constraints.append(smt_func(*smt_inputs) != smt_output)
 
-        # Exclude designated value set
         for smt_elem in self.smt_carrier_set:
             model_val = ModelValue(str(smt_elem))
             is_designated_in_model = model_val in model.designated_values
diff --git a/vsp.py b/vsp.py
index 5ea2ae9..0de5b10 100644
--- a/vsp.py
+++ b/vsp.py
@@ -168,7 +168,7 @@ def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result:
                 )
             )
 
-    # x -> y is non-designated
+    # x -> y is non-designated for any x in K1 and y in K2
     smt_imp = encoder.model_function_map[impfn]
     for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set):
         encoder.solver.add(

From 6d877938034c102ebab7aed03ecd261c357341ae Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 27 Jan 2026 12:48:33 -0500
Subject: [PATCH 05/10] Updated driver file R.py to showcase SMT techinques
 Fixed minor bugs concerning lack of falsification rules and interfaces
 between VSP and SMT

---
 R.py              | 81 +++++++++++++++++++++++++++++++++++------------
 generate_model.py | 11 ++++---
 logic.py          |  2 +-
 smt.py            | 75 +++++++++++++++++++++++++------------------
 vsp.py            | 16 +++++-----
 5 files changed, 120 insertions(+), 65 deletions(-)

diff --git a/R.py b/R.py
index 4ce4b04..1b0fa39 100644
--- a/R.py
+++ b/R.py
@@ -12,7 +12,8 @@ from logic import (
 )
 from model import Model, ModelFunction, ModelValue, satisfiable
 from generate_model import generate_model
-# from vsp import has_vsp
+from vsp import has_vsp
+from smt import smt_is_loaded
 
 
 # ===================================================
@@ -56,12 +57,17 @@ disjunction_rules = {
     Rule({Conjunction(x, Disjunction(y, z)),}, Disjunction(Conjunction(x, y), Conjunction(x, z)))
 }
 
+falsification_rules = {
+    # At least one value is non-designated
+    Rule(set(), x)
+}
+
 
 logic_rules = implication_rules | negation_rules | conjunction_rules | disjunction_rules
 
 operations = {Negation, Conjunction, Disjunction, Implication}
 
-R_logic = Logic(operations, logic_rules, "R")
+R_logic = Logic(operations, logic_rules, falsification_rules, "R")
 
 # ===============================
 
@@ -69,36 +75,36 @@ R_logic = Logic(operations, logic_rules, "R")
 Example 2-Element Model of R
 """
 
-a0 = ModelValue("a0")
-a1 = ModelValue("a1")
+a0 = ModelValue("0")
+a1 = ModelValue("1")
 
 carrier_set = {a0, a1}
 
 mnegation = ModelFunction(1, {
     a0: a1,
     a1: a0
-})
+}, "¬")
 
 mimplication = ModelFunction(2, {
     (a0, a0): a1,
     (a0, a1): a1,
     (a1, a0): a0,
     (a1, a1): a1
-})
+}, "→")
 
 mconjunction = ModelFunction(2, {
     (a0, a0): a0,
     (a0, a1): a0,
     (a1, a0): a0,
     (a1, a1): a1
-})
+}, "∧")
 
 mdisjunction = ModelFunction(2, {
     (a0, a0): a0,
     (a0, a1): a1,
     (a1, a0): a1,
     (a1, a1): a1
-})
+}, "∨")
 
 
 designated_values = {a1}
@@ -117,11 +123,18 @@ interpretation = {
 
 print(R_model_2)
 
+print(f"Does {R_model_2.name} satisfy the logic R?", satisfiable(R_logic, R_model_2, interpretation))
+
+if smt_is_loaded():
+    print(has_vsp(R_model_2, mimplication, True, True))
+else:
+    print("Z3 not setup, skipping VSP check...")
+
 
 # =================================
 
 """
-Generate models of R of a specified size
+Generate models of R of a specified size using the slow approach
 """
 
 print("*" * 30)
@@ -130,14 +143,20 @@ model_size = 2
 print("Generating models of Logic", R_logic.name, "of size", model_size)
 solutions = generate_model(R_logic, model_size, print_model=False)
 
-print(f"Found {len(solutions)} satisfiable models")
+if smt_is_loaded():
+    num_satisfies_vsp = 0
+    for model, interpretation in solutions:
+        negation_defined = Negation in interpretation
+        conj_disj_defined = Conjunction in interpretation and Disjunction in interpretation
+        if has_vsp(model, interpretation[Implication], negation_defined, conj_disj_defined).has_vsp:
+            num_satisfies_vsp += 1
+
+    print(f"Found {len(solutions)} satisfiable models of size {model_size}, {num_satisfies_vsp} of which satisfy VSP")
 
-# for model, interpretation in solutions:
-#     print(has_vsp(model, interpretation))
 
 print("*" * 30)
 
-######
+# =================================
 
 """
 Showing the smallest model for R that has the
@@ -146,12 +165,12 @@ variable sharing property.
 This model has 6 elements.
 """
 
-a0 = ModelValue("a0")
-a1 = ModelValue("a1")
-a2 = ModelValue("a2")
-a3 = ModelValue("a3")
-a4 = ModelValue("a4")
-a5 = ModelValue("a5")
+a0 = ModelValue("0")
+a1 = ModelValue("1")
+a2 = ModelValue("2")
+a3 = ModelValue("3")
+a4 = ModelValue("4")
+a5 = ModelValue("5")
 
 carrier_set = { a0, a1, a2, a3, a4, a5 }
 designated_values = {a1, a2, a3, a4, a5 }
@@ -312,4 +331,26 @@ interpretation = {
 
 print(R_model_6)
 print(f"Model {R_model_6.name} satisfies logic {R_logic.name}?", satisfiable(R_logic, R_model_6, interpretation))
-# print(has_vsp(R_model_6, interpretation))
+if smt_is_loaded():
+    print(has_vsp(R_model_6, mimplication, True, True))
+else:
+    print("Z3 not loaded, skipping VSP check...")
+
+"""
+Generate models of R of a specified size using the SMT approach
+"""
+
+from vsp import logic_has_vsp
+
+size = 7
+print(f"Searching for a model of size {size} which witness VSP...")
+if smt_is_loaded():
+    solution = logic_has_vsp(R_logic, size)
+    if solution is None:
+        print(f"No models found of size {size} which witness VSP")
+    else:
+        model, vsp_result = solution
+        print(vsp_result)
+        print(model)
+else:
+    print("Z3 not setup, skipping...")
\ No newline at end of file
diff --git a/generate_model.py b/generate_model.py
index 5a46efc..ceb9681 100644
--- a/generate_model.py
+++ b/generate_model.py
@@ -67,7 +67,7 @@ def only_rules_with(rules: Set[Rule], operation: Operation) -> List[Rule]:
 
 def possible_interpretations(
         logic: Logic, carrier_set: Set[ModelValue],
-        designated_values: Set[ModelValue]):
+        designated_values: Set[ModelValue], debug: bool):
     """
     Consider every possible interpretation of operations
     within the specified logic given the carrier set of
@@ -100,7 +100,7 @@ def possible_interpretations(
             passed_functions = candidate_functions
         if len(passed_functions) == 0:
             raise Exception("No interpretation satisfies the axioms for the operation " + str(operation))
-        else:
+        elif debug:
             print(
                   f"Operation {operation.symbol} has {len(passed_functions)} candidate functions"
             )
@@ -120,7 +120,7 @@ def possible_interpretations(
 
 def generate_model(
         logic: Logic, number_elements: int, num_solutions: int = -1,
-        print_model=False) -> List[Tuple[Model, Interpretation]]:
+        print_model=False, debug=False) -> List[Tuple[Model, Interpretation]]:
     """
     Generate the specified number of models that
     satisfy a logic of a certain size.
@@ -136,9 +136,10 @@ def generate_model(
 
     for designated_values in possible_designated_values:
         designated_values = set(designated_values)
-        print("Considering models for designated values", set_to_str(designated_values))
+        if debug:
+            print("Considering models for designated values", set_to_str(designated_values))
 
-        possible_interps = possible_interpretations(logic, carrier_set, designated_values)
+        possible_interps = possible_interpretations(logic, carrier_set, designated_values, debug)
         for interpretation in possible_interps:
             is_valid = True
             model = Model(carrier_set, set(interpretation.values()), designated_values)
diff --git a/logic.py b/logic.py
index 44c5c6b..1cb383e 100644
--- a/logic.py
+++ b/logic.py
@@ -85,7 +85,7 @@ class Logic:
             name: Optional[str] = None):
         self.operations = operations
         self.rules = rules
-        self.falsifies = falsifies
+        self.falsifies = falsifies if falsifies is not None else set()
         self.name = str(abs(hash((
             frozenset(operations),
             frozenset(rules)
diff --git a/smt.py b/smt.py
index 3946975..4394713 100644
--- a/smt.py
+++ b/smt.py
@@ -1,18 +1,26 @@
 from itertools import product
-from typing import Dict, Generator, Optional, Tuple
+from typing import Dict, Generator, Optional, Set, Tuple, TYPE_CHECKING
 
 from logic import Logic, Operation, Rule, PropositionalVariable, Term, OpTerm, get_prop_vars_from_rule
 from model import Model, ModelValue, ModelFunction
 
-from z3 import (
-    And, BoolSort, Context, EnumSort, Function, Implies, Or, sat, Solver, z3
-)
+SMT_LOADED = True
+try:
+    from z3 import (
+        And, BoolSort, Context, EnumSort, Function, Implies, Or, sat, Solver, z3
+    )
+except ImportError:
+    SMT_LOADED = False
+
+def smt_is_loaded() -> bool:
+    global SMT_LOADED
+    return SMT_LOADED
 
 def term_to_smt(
     t: Term,
-    op_mapping: Dict[Operation, z3.FuncDeclRef],
-    var_mapping: Dict[PropositionalVariable, z3.DatatypeRef]
-) -> z3.DatatypeRef:
+    op_mapping: Dict[Operation, "z3.FuncDeclRef"],
+    var_mapping: Dict[PropositionalVariable, "z3.DatatypeRef"]
+) -> "z3.DatatypeRef":
     """Convert a logic term to its SMT representation."""
     if isinstance(t, PropositionalVariable):
         return var_mapping[t]
@@ -26,10 +34,10 @@ def term_to_smt(
 
 def logic_rule_to_smt_constraints(
     rule: Rule,
-    IsDesignated: z3.FuncDeclRef,
+    IsDesignated: "z3.FuncDeclRef",
     smt_carrier_set,
-    op_mapping: Dict[Operation, z3.FuncDeclRef]
-) -> Generator[z3.BoolRef, None, None]:
+    op_mapping: Dict[Operation, "z3.FuncDeclRef"]
+) -> Generator["z3.BoolRef", None, None]:
     """
     Encode a logic rule as SMT constraints.
 
@@ -63,10 +71,10 @@ def logic_rule_to_smt_constraints(
 
 def logic_falsification_rule_to_smt_constraints(
     rule: Rule,
-    IsDesignated: z3.FuncDeclRef,
+    IsDesignated: "z3.FuncDeclRef",
     smt_carrier_set,
-    op_mapping: Dict[Operation, z3.FuncDeclRef]
-) -> z3.BoolRef:
+    op_mapping: Dict[Operation, "z3.FuncDeclRef"]
+) -> "z3.BoolRef":
     """
     Encode a falsification rule as an SMT constraint.
 
@@ -132,7 +140,7 @@ class SMTLogicEncoder:
         self.carrier_sort, self.smt_carrier_set = EnumSort("C", element_names, ctx=self.ctx)
 
         # Create operation functions
-        self.operation_function_map: Dict[Operation, z3.FuncDeclRef] = {}
+        self.operation_function_map: Dict[Operation, "z3.FuncDeclRef"] = {}
         for operation in logic.operations:
             self.operation_function_map[operation] = self.create_function(operation.symbol, operation.arity)
 
@@ -143,10 +151,10 @@ class SMTLogicEncoder:
         self._add_logic_constraints()
         self._add_designation_symmetry_constraints()
 
-    def create_predicate(self, name: str, arity: int) -> z3.FuncDeclRef:
+    def create_predicate(self, name: str, arity: int) -> "z3.FuncDeclRef":
         return Function(name, *(self.carrier_sort for _ in range(arity)), BoolSort(ctx=self.ctx))
 
-    def create_function(self, name: str, arity: int) -> z3.FuncDeclRef:
+    def create_function(self, name: str, arity: int) -> "z3.FuncDeclRef":
         return Function(name, *(self.carrier_sort for _ in range(arity + 1)))
 
     def _add_logic_constraints(self):
@@ -171,9 +179,9 @@ class SMTLogicEncoder:
             )
             self.solver.add(constraint)
 
-    def extract_model(self, smt_model) -> Model:
+    def extract_model(self, smt_model) -> Tuple[Model, Dict[Operation, ModelFunction]]:
         """
-        Extract a Model object from an SMT model.
+        Extract a Model object and interpretation from an SMT model.
         """
         carrier_set = {ModelValue(f"{i}") for i in range(self.size)}
 
@@ -185,7 +193,8 @@ class SMTLogicEncoder:
         designated_values = {ModelValue(str(x)) for x in smt_designated}
 
         # Extract operation functions
-        model_functions = set()
+        model_functions: Set[ModelFunction] = set()
+        interpretation: Dict[Operation, ModelFunction] = dict()
         for (operation, smt_function) in self.operation_function_map.items():
             mapping: Dict[Tuple[ModelValue], ModelValue] = {}
             for smt_inputs in product(self.smt_carrier_set, repeat=operation.arity):
@@ -193,9 +202,12 @@ class SMTLogicEncoder:
                 smt_output = smt_model.evaluate(smt_function(*smt_inputs))
                 model_output = ModelValue(str(smt_output))
                 mapping[model_inputs] = model_output
-            model_functions.add(ModelFunction(operation.arity, mapping, operation.symbol))
+            model_function = ModelFunction(operation.arity, mapping, operation.symbol)
+            model_functions.add(model_function)
+            interpretation[operation] = model_function
 
-        return Model(carrier_set, model_functions, designated_values)
+
+        return Model(carrier_set, model_functions, designated_values), interpretation
 
 
     def _add_designation_symmetry_constraints(self):
@@ -218,7 +230,7 @@ class SMTLogicEncoder:
                 )
             )
 
-    def create_exclusion_constraint(self, model: Model) -> z3.BoolRef:
+    def create_exclusion_constraint(self, model: Model) -> "z3.BoolRef":
         """
         Create a constraint that excludes the given model from future solutions.
         """
@@ -254,7 +266,7 @@ class SMTLogicEncoder:
 
         return Or(constraints)
 
-    def find_model(self) -> Optional[Model]:
+    def find_model(self) -> Optional[Tuple[Model, Dict[Operation, ModelFunction]]]:
         """
         Find a single model satisfying the logic constraints.
 
@@ -274,12 +286,12 @@ class SMTLogicEncoder:
             pass
 
 
-def find_model(logic: Logic, size: int) -> Optional[Model]:
+def find_model(logic: Logic, size: int) -> Optional[Tuple[Model, Dict[Operation, ModelFunction]]]:
     """Find a single model for the given logic and size."""
     encoder = SMTLogicEncoder(logic, size)
     return encoder.find_model()
 
-def find_all_models(logic: Logic, size: int) -> Generator[Model, None, None]:
+def find_all_models(logic: Logic, size: int) -> Generator[Tuple[Model, Dict[Operation, ModelFunction]], None, None]:
     """
     Find all models for the given logic and size.
 
@@ -294,13 +306,14 @@ def find_all_models(logic: Logic, size: int) -> Generator[Model, None, None]:
 
     while True:
         # Try to find a model
-        model = encoder.find_model()
-        if model is None:
+        solution = encoder.find_model()
+        if solution is None:
             break
 
-        yield model
+        yield solution
 
         # Add constraint to exclude this model from future solutions
+        model, _ = solution
         exclusion_constraint = encoder.create_exclusion_constraint(model)
         encoder.solver.add(exclusion_constraint)
 
@@ -346,13 +359,13 @@ class SMTModelEncoder:
             is_designated = model_value in model.designated_values
             self.solver.add(self.is_designated(self.model_value_to_smt[model_value]) == is_designated)
 
-    def create_predicate(self, name: str, arity: int) -> z3.FuncDeclRef:
+    def create_predicate(self, name: str, arity: int) -> "z3.FuncDeclRef":
         return Function(name, *(self.carrier_sort for _ in range(arity)), BoolSort(ctx=self.ctx))
 
-    def create_function(self, name: str, arity: int) -> z3.FuncDeclRef:
+    def create_function(self, name: str, arity: int) -> "z3.FuncDeclRef":
         return Function(name, *(self.carrier_sort for _ in range(arity + 1)))
 
-    def add_function_constraints_from_table(self, smt_fn: z3.FuncDeclRef, model_fn: ModelFunction):
+    def add_function_constraints_from_table(self, smt_fn: "z3.FuncDeclRef", model_fn: ModelFunction):
         for inputs, output in model_fn.mapping.items():
             smt_inputs = tuple(self.model_value_to_smt[inp] for inp in inputs)
             smt_output = self.model_value_to_smt[output]
diff --git a/vsp.py b/vsp.py
index 0de5b10..fe97ccb 100644
--- a/vsp.py
+++ b/vsp.py
@@ -10,12 +10,12 @@ from model import (
     Model, model_closure, ModelFunction, ModelValue
 )
 
-SMT_LOADED = True
+from smt import SMTModelEncoder, SMTLogicEncoder, smt_is_loaded
+
 try:
     from z3 import And, Or, Implies, sat
-    from smt import SMTModelEncoder, SMTLogicEncoder
 except ImportError:
-    SMT_LOADED = False
+    pass
 
 class VSP_Result:
     def __init__(
@@ -139,7 +139,7 @@ def has_vsp_smt(model: Model, impfn: ModelFunction) -> VSP_Result:
     Checks whether a given model satisfies the variable
     sharing property via SMT
     """
-    if not SMT_LOADED:
+    if not smt_is_loaded():
         raise Exception("Z3 is not property installed, cannot check via SMT")
 
     encoder = SMTModelEncoder(model)
@@ -198,7 +198,7 @@ def has_vsp(model: Model, impfunction: ModelFunction,
     if model.is_magical:
         return has_vsp_magical(model, impfunction, negation_defined, conjunction_disjunction_defined)
 
-    return has_vsp_smt(model)
+    return has_vsp_smt(model, impfunction)
 
 
 def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]]:
@@ -254,15 +254,15 @@ def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]]
             )
         )
 
-    model = encoder.find_model()
+    solution = encoder.find_model()
 
     # We failed to find a VSP witness
-    if model is None:
+    if solution is None:
         return None
 
     # Otherwise, a matrix model and correspoding
     # subalgebras exist.
-
+    model, _ = solution
     smt_model = encoder.solver.model()
     K1_smt = [x for x in encoder.smt_carrier_set if smt_model.evaluate(IsInK1(x))]
     K1 = {ModelValue(str(x)) for x in K1_smt}

From bf86bfd83ead5036ae5d2576e399a5a29ee5baf4 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 27 Jan 2026 14:11:41 -0500
Subject: [PATCH 06/10] Simplified satisfiable

---
 model.py | 87 +++++++++++++++++++++++---------------------------------
 1 file changed, 35 insertions(+), 52 deletions(-)

diff --git a/model.py b/model.py
index 41483f9..cd02e6e 100644
--- a/model.py
+++ b/model.py
@@ -5,7 +5,7 @@ a given logic.
 from common import set_to_str, immutable
 from logic import (
     get_propostional_variables, Logic,
-    Operation, PropositionalVariable, Term
+    Operation, PropositionalVariable, Rule, Term
 )
 from collections import defaultdict
 from functools import cached_property, lru_cache, reduce
@@ -277,67 +277,50 @@ def all_model_valuations_cached(
     return list(all_model_valuations(pvars, mvalues))
 
 
+def rule_satisfied(
+        rule: Rule, valuations: List[Dict[PropositionalVariable, ModelValue]],
+        interpretation: Dict[Operation, ModelFunction], designated_values: Set[ModelValue]) -> bool:
+    """
+    Checks whether a rule holds under all valuations listed in mapping.
+
+    If there is a mapping where the premise holds but the consequent does
+    not then this returns False.
+    """
+    for valuation in valuations:
+        premise_met = True
+        for premise in rule.premises:
+            premise_t = evaluate_term(premise, valuation, interpretation)
+            if premise_t not in designated_values:
+                premise_met = False
+                break
+
+        # If any of the premises doesn't hold, then this won't serve as a counterexample
+        if not premise_met:
+            continue
+
+        consequent_t = evaluate_term(rule.conclusion, valuation, interpretation)
+        if consequent_t not in designated_values:
+            # Counterexample found, return False
+            return False
+
+    # No mapping found which contradicts our rule
+    return True
+
+
 def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, ModelFunction]) -> bool:
     """
     Determine whether a model satisfies a logic
     given an interpretation.
     """
     pvars = tuple(get_propostional_variables(tuple(logic.rules)))
-    mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set))
+    valuations = all_model_valuations_cached(pvars, tuple(model.carrier_set))
 
     for rule in logic.rules:
-        # The rule most hold for all valuations
-        for mapping in mappings:
-            # The check only applies if the premises are designated
-            premise_met = True
-            premise_ts: Set[ModelValue] = set()
-
-            for premise in rule.premises:
-                premise_t = evaluate_term(premise, mapping, interpretation)
-                # As soon as one premise is not designated,
-                # move to the next rule.
-                if premise_t not in model.designated_values:
-                    premise_met = False
-                    break
-                # If designated, keep track of the evaluated term
-                premise_ts.add(premise_t)
-
-            if not premise_met:
-                continue
-
-            # With the premises designated, make sure the consequent is designated
-            consequent_t = evaluate_term(rule.conclusion, mapping, interpretation)
-            if consequent_t not in model.designated_values:
-                return False
+        if not rule_satisfied(rule, valuations, interpretation, model.designated_values):
+            return False
 
     for rule in logic.falsifies:
-        # We must find one mapping where this does not hold
-        counterexample_found = False
-        for mapping in mappings:
-            # The check only applies if the premises are designated
-            premise_met = True
-            premise_ts: Set[ModelValue] = set()
-
-            for premise in rule.premises:
-                premise_t = evaluate_term(premise, mapping, interpretation)
-                # As soon as one premise is not designated,
-                # move to the next rule.
-                if premise_t not in model.designated_values:
-                    premise_met = False
-                    break
-                # If designated, keep track of the evaluated term
-                premise_ts.add(premise_t)
-
-            if not premise_met:
-                continue
-
-            # With the premises designated, make sure the consequent is not designated
-            consequent_t = evaluate_term(rule.conclusion, mapping, interpretation)
-            if consequent_t not in model.designated_values:
-                counterexample_found = True
-                break
-
-        if not counterexample_found:
+        if rule_satisfied(rule, valuations, interpretation, model.designated_values):
             return False
 
     return True

From 51f8adcd441d67a57200ff503d2dab631876d969 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 27 Jan 2026 14:13:19 -0500
Subject: [PATCH 07/10] Small comment change

---
 model.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/model.py b/model.py
index cd02e6e..79cff8f 100644
--- a/model.py
+++ b/model.py
@@ -281,7 +281,7 @@ def rule_satisfied(
         rule: Rule, valuations: List[Dict[PropositionalVariable, ModelValue]],
         interpretation: Dict[Operation, ModelFunction], designated_values: Set[ModelValue]) -> bool:
     """
-    Checks whether a rule holds under all valuations listed in mapping.
+    Checks whether a rule holds under all valuations.
 
     If there is a mapping where the premise holds but the consequent does
     not then this returns False.

From 85ef364a5743dc8982410aa1d32ac7983fc5b0c7 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 27 Jan 2026 14:13:54 -0500
Subject: [PATCH 08/10] Small comment change

---
 model.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/model.py b/model.py
index 79cff8f..855b320 100644
--- a/model.py
+++ b/model.py
@@ -303,7 +303,7 @@ def rule_satisfied(
             # Counterexample found, return False
             return False
 
-    # No mapping found which contradicts our rule
+    # No valuation found which contradicts our rule
     return True
 
 

From 06cca7d32ecd3c69d36fbb3a50f2f4b7ebe4ddf3 Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 27 Jan 2026 15:22:47 -0500
Subject: [PATCH 09/10] Refactored out valuation generation code in SMT

---
 model.py |  4 ++--
 smt.py   | 64 ++++++++++++++++++++++++++++++++++++--------------------
 2 files changed, 43 insertions(+), 25 deletions(-)

diff --git a/model.py b/model.py
index 855b320..05a1a1d 100644
--- a/model.py
+++ b/model.py
@@ -13,7 +13,7 @@ from itertools import (
     chain, combinations_with_replacement,
     permutations, product
 )
-from typing import Dict, List, Optional, Set, Tuple
+from typing import Any, Dict, Generator, List, Optional, Set, Tuple
 
 
 __all__ = ['ModelValue', 'ModelFunction', 'Model', 'Interpretation']
@@ -255,7 +255,7 @@ def evaluate_term(
 
 def all_model_valuations(
         pvars: Tuple[PropositionalVariable],
-        mvalues: Tuple[ModelValue]):
+        mvalues: Tuple[ModelValue]) -> Generator[Dict[PropositionalVariable, ModelValue], Any, None]:
     """
     Given propositional variables and model values,
     produce every possible mapping between the two.
diff --git a/smt.py b/smt.py
index 4394713..9dbee99 100644
--- a/smt.py
+++ b/smt.py
@@ -1,5 +1,6 @@
+from functools import lru_cache
 from itertools import product
-from typing import Dict, Generator, Optional, Set, Tuple, TYPE_CHECKING
+from typing import Dict, Generator, Optional, Set, Tuple
 
 from logic import Logic, Operation, Rule, PropositionalVariable, Term, OpTerm, get_prop_vars_from_rule
 from model import Model, ModelValue, ModelFunction
@@ -27,11 +28,32 @@ def term_to_smt(
 
     assert isinstance(t, OpTerm)
 
+    # Recursively convert all arguments to SMT
     arguments = [term_to_smt(arg, op_mapping, var_mapping) for arg in t.arguments]
     fn = op_mapping[t.operation]
 
     return fn(*arguments)
 
+def all_smt_valuations(pvars: Tuple[PropositionalVariable], smtvalues):
+    """
+    Generator which maps all the propositional variable to
+    smt variables representing the carrier set.
+
+    Exhaust the generator to get all such mappings.
+    """
+    all_possible_values = product(smtvalues, repeat=len(pvars))
+    for valuation in all_possible_values:
+        mapping = dict()
+        assert len(pvars) == len(valuation)
+        for pvar, value in zip(pvars, valuation):
+            mapping[pvar] = value
+        yield mapping
+
+
+@lru_cache
+def all_smt_valuations_cached(pvars: Tuple[PropositionalVariable], smtvalues):
+    return list(all_smt_valuations(pvars, smtvalues))
+
 def logic_rule_to_smt_constraints(
     rule: Rule,
     IsDesignated: "z3.FuncDeclRef",
@@ -43,32 +65,30 @@ def logic_rule_to_smt_constraints(
 
     For all valuations: if premises are designated, then conclusion is designated.
     """
-    prop_vars = get_prop_vars_from_rule(rule)
-
-    # Requires that the rule holds under all valuations
-    for smt_vars in product(smt_carrier_set, repeat=len(prop_vars)):
-        assert len(prop_vars) == len(smt_vars)
-
-        var_mapping = {
-            prop_var: smt_var
-            for (prop_var, smt_var) in zip(prop_vars, smt_vars)
-        }
+    prop_vars = tuple(get_prop_vars_from_rule(rule))
+    valuations = all_smt_valuations_cached(prop_vars, tuple(smt_carrier_set))
 
+    for valuation in valuations:
         premises = [
-            IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True
+            IsDesignated(term_to_smt(premise, op_mapping, valuation)) == True
             for premise in rule.premises
         ]
-        conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, var_mapping)) == True
+        conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, valuation)) == True
 
         if len(premises) == 0:
+            # If there are no premises, then the conclusion must always be designated
             yield conclusion
         else:
+            # Otherwise, combine all the premises with and
+            # and have that if the premises are designated
+            # then the conclusion is designated
             premise = premises[0]
             for p in premises[1:]:
                 premise = And(premise, p)
 
             yield Implies(premise, conclusion)
 
+
 def logic_falsification_rule_to_smt_constraints(
     rule: Rule,
     IsDesignated: "z3.FuncDeclRef",
@@ -81,24 +101,22 @@ def logic_falsification_rule_to_smt_constraints(
     There exists at least one valuation where premises are designated
     but conclusion is not designated.
     """
-    prop_vars = get_prop_vars_from_rule(rule)
+    prop_vars = tuple(get_prop_vars_from_rule(rule))
+    valuations = all_smt_valuations_cached(prop_vars, tuple(smt_carrier_set))
 
     # Collect all possible counter-examples (valuations that falsify the rule)
     counter_examples = []
 
-    for smt_vars in product(smt_carrier_set, repeat=len(prop_vars)):
-        assert len(prop_vars) == len(smt_vars)
-
-        var_mapping = {
-            prop_var: smt_var
-            for (prop_var, smt_var) in zip(prop_vars, smt_vars)
-        }
+    for valuation in valuations:
+        # The rule is falsified when all of our premises
+        # are designated but our conclusion is not designated
 
         premises = [
-            IsDesignated(term_to_smt(premise, op_mapping, var_mapping)) == True
+            IsDesignated(term_to_smt(premise, op_mapping, valuation)) == True
             for premise in rule.premises
         ]
-        conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, var_mapping)) == False
+
+        conclusion = IsDesignated(term_to_smt(rule.conclusion, op_mapping, valuation)) == False
 
         if len(premises) == 0:
             counter_examples.append(conclusion)

From 51bf1a44d9985ac5406938bc0e1b56ca21aed29b Mon Sep 17 00:00:00 2001
From: Brandon Rozek <brozek@brandonrozek.com>
Date: Tue, 27 Jan 2026 15:26:16 -0500
Subject: [PATCH 10/10] Small comment change

---
 vsp.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/vsp.py b/vsp.py
index fe97ccb..c4fd398 100644
--- a/vsp.py
+++ b/vsp.py
@@ -244,7 +244,7 @@ def logic_has_vsp(logic: Logic, size: int) -> Optional[Tuple[Model, VSP_Result]]
                 )
             )
 
-    # x -> y is non-designated
+    # x -> y is non-designated for any x in k1 and y in k2
     Impfn = encoder.operation_function_map[Implication]
     for (x, y) in product(encoder.smt_carrier_set, encoder.smt_carrier_set):
         encoder.solver.add(