From f799a1ff5dedb254aeac11e5d5b10ff25628f43f Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 12 Dec 2025 11:36:21 -0500 Subject: [PATCH] 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