From 872e54ec5ea3eeba419dbe52357a29f0d2dab2a1 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 24 Nov 2025 16:52:04 -0500 Subject: [PATCH 1/3] Revised algorithm to cache closures --- vsp.py | 103 +++++++++++++++++++-------------------------------------- 1 file changed, 34 insertions(+), 69 deletions(-) diff --git a/vsp.py b/vsp.py index 034005f..82baa4a 100644 --- a/vsp.py +++ b/vsp.py @@ -3,7 +3,7 @@ Check to see if the model has the variable sharing property. """ from itertools import product -from typing import List, Optional, Set, Tuple +from typing import Dict, List, Optional, Set, Tuple from common import set_to_str from model import ( Model, model_closure, ModelFunction, ModelValue @@ -43,81 +43,46 @@ def has_vsp(model: Model, impfunction: ModelFunction, top = model.ordering.top() bottom = model.ordering.bottom() - # Compute I the set of tuples (x, y) where - # x -> y does not take a designiated value - I: List[Tuple[ModelValue, ModelValue]] = [] + C: Dict[ModelValue, Set[ModelValue]] = {} + U: Dict[ModelValue, Set[ModelValue]] = {} - for (x, y) in product(model.designated_values, model.designated_values): - if impfunction(x, y) not in model.designated_values: - I.append((x, y)) - - # Find the subalgebras which falsify implication - for xys in I: - - xi = xys[0] + for d in model.designated_values: + C[d] = model_closure({d,}, model.logical_operations, None) + U[d] = {y for y in model.designated_values if impfunction(d, y) in model.designated_values} + for x in model.designated_values: + Xs = C[x] + # Discard ({⊥} ∪ A', B) subalgebras - if bottom is not None and xi == bottom: + if bottom is not None and bottom in Xs: continue - + # Discard ({⊤} ∪ A', B) subalgebras when negation is defined - if top is not None and negation_defined and xi == top: + if top is not None and negation_defined and top in Xs: continue - yi = xys[1] + Ux = U[x] + for y in model.designated_values - Xs - Ux: + Ys = C[y] - # Discard (A, {⊤} ∪ B') subalgebras - if top is not None and yi == top: - continue - - # Discard (A, {⊥} ∪ B') subalgebras when negation is defined - if bottom is not None and negation_defined and yi == bottom: - continue - - # Discard ({a} ∪ A', {b} ∪ B') subalgebras when a <= b - if model.ordering.is_lt(xi, yi): - continue - - # Discard ({a} ∪ A', {b} ∪ B') subalgebras when b <= a and negation is defined - if negation_defined and model.ordering.is_lt(yi, xi): - continue - - # Compute the left closure of the set containing xi under all the operations - carrier_set_left: Set[ModelValue] = model_closure({xi,}, model.logical_operations, bottom) - - # Discard ({⊥} ∪ A', B) subalgebras - if bottom is not None and bottom in carrier_set_left: - continue - - # Discard ({⊤} ∪ A', B) subalgebras when negation is defined - if top is not None and negation_defined and top in carrier_set_left: - continue - - # Compute the closure of all operations - # with just the ys - carrier_set_right: Set[ModelValue] = model_closure({yi,}, model.logical_operations, top) - - # Discard (A, {⊤} ∪ B') subalgebras - if top is not None and top in carrier_set_right: - continue - - # Discard (A, {⊥} ∪ B') subalgebras when negation is defined - if bottom is not None and negation_defined and bottom in carrier_set_right: - continue - - # Discard subalgebras that intersect - if not carrier_set_left.isdisjoint(carrier_set_right): - continue - - # Check whether for all pairs in the subalgebra, - # that implication is falsified. - falsified = True - for (x2, y2) in product(carrier_set_left, carrier_set_right): - if impfunction(x2, y2) in model.designated_values: - falsified = False - break - - if falsified: - return VSP_Result(True, model.name, carrier_set_left, carrier_set_right) + # Discard (A, {⊤} ∪ B') subalgebras + if top is not None and top in Ys: + continue + + # Discard (A, {⊥} ∪ B') subalgebras when negation is defined + if bottom is not None and negation_defined and bottom in Ys: + continue + + if not Xs.isdisjoint(Ys): + continue + falsified = True + for (xi, yi) in product(Xs, Ys): + if impfunction(xi, yi) in model.designated_values: + falsified = False + break + + if falsified: + return VSP_Result(True, model.name, Xs, Ys) + return VSP_Result(False, model.name) From 0a894388a08527af0a6ea2fa34cb1100b2861435 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 24 Nov 2025 17:29:43 -0500 Subject: [PATCH 2/3] Futile attempts at improving average runtime --- vsp.py | 50 +++++++++++++++++++++++++++++++++++++------------- 1 file changed, 37 insertions(+), 13 deletions(-) diff --git a/vsp.py b/vsp.py index 82baa4a..8383a89 100644 --- a/vsp.py +++ b/vsp.py @@ -44,35 +44,59 @@ def has_vsp(model: Model, impfunction: ModelFunction, bottom = model.ordering.bottom() C: Dict[ModelValue, Set[ModelValue]] = {} - U: Dict[ModelValue, Set[ModelValue]] = {} - - for d in model.designated_values: - C[d] = model_closure({d,}, model.logical_operations, None) - U[d] = {y for y in model.designated_values if impfunction(d, y) in model.designated_values} for x in model.designated_values: + + # Discard ({⊥} ∪ A', B) subalgebras + if bottom is not None and x == bottom: + continue + + # Discard ({⊤} ∪ A', B) subalgebras when negation is defined + if top is not None and negation_defined and x == top: + continue + + if x not in C: + C[x] = model_closure({x,}, model.logical_operations, None) Xs = C[x] - + # Discard ({⊥} ∪ A', B) subalgebras if bottom is not None and bottom in Xs: continue - + # Discard ({⊤} ∪ A', B) subalgebras when negation is defined if top is not None and negation_defined and top in Xs: continue - Ux = U[x] - for y in model.designated_values - Xs - Ux: + for y in model.designated_values - Xs: + + # Discard (A, {⊤} ∪ B') subalgebras + if top is not None and y == top: + continue + + # Discard (A, {⊥} ∪ B') subalgebras when negation is defined + if bottom is not None and negation_defined and y == bottom: + continue + + # Discard ({a} ∪ A', {b} ∪ B') subalgebras when a <= b + if model.ordering.is_lt(x, y): + continue + + # Discard ({a} ∪ A', {b} ∪ B') subalgebras when b <= a and negation is defined + if negation_defined and model.ordering.is_lt(y, x): + continue + + if y not in C: + C[y] = model_closure({y,}, model.logical_operations, None) Ys = C[y] # Discard (A, {⊤} ∪ B') subalgebras if top is not None and top in Ys: continue - + # Discard (A, {⊥} ∪ B') subalgebras when negation is defined if bottom is not None and negation_defined and bottom in Ys: continue - + if not Xs.isdisjoint(Ys): continue @@ -81,8 +105,8 @@ def has_vsp(model: Model, impfunction: ModelFunction, if impfunction(xi, yi) in model.designated_values: falsified = False break - + if falsified: return VSP_Result(True, model.name, Xs, Ys) - + return VSP_Result(False, model.name) From 7e4a57040732f3e20e2444237b8ec6aa7f7df83d Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 25 Nov 2025 10:03:55 -0500 Subject: [PATCH 3/3] Another attempt --- vsp.py | 54 ++++++++++++++++++++++++++++++------------------------ 1 file changed, 30 insertions(+), 24 deletions(-) diff --git a/vsp.py b/vsp.py index 8383a89..4aca288 100644 --- a/vsp.py +++ b/vsp.py @@ -43,10 +43,10 @@ def has_vsp(model: Model, impfunction: ModelFunction, top = model.ordering.top() bottom = model.ordering.bottom() + # Cache of closures C: Dict[ModelValue, Set[ModelValue]] = {} for x in model.designated_values: - # Discard ({⊥} ∪ A', B) subalgebras if bottom is not None and x == bottom: continue @@ -55,19 +55,31 @@ def has_vsp(model: Model, impfunction: ModelFunction, if top is not None and negation_defined and x == top: continue - if x not in C: - C[x] = model_closure({x,}, model.logical_operations, None) - Xs = C[x] + candidate_ys = [y for y in model.designated_values if impfunction(x, y) not in model.designated_values] + + if len(candidate_ys) == 0: + continue + + carrier_set_left: Set[ModelValue] = model_closure(C.get(x, {x,}), model.logical_operations, bottom) + C[x] = carrier_set_left # Discard ({⊥} ∪ A', B) subalgebras - if bottom is not None and bottom in Xs: + if bottom is not None and bottom in carrier_set_left: continue # Discard ({⊤} ∪ A', B) subalgebras when negation is defined - if top is not None and negation_defined and top in Xs: + if top is not None and negation_defined and top in carrier_set_left: continue + + for y in candidate_ys: + # Discard ({a} ∪ A', {b} ∪ B') subalgebras when a <= b + if model.ordering.is_lt(x, y): + continue + + # Discard ({a} ∪ A', {b} ∪ B') subalgebras when b <= a and negation is defined + if negation_defined and model.ordering.is_lt(y, x): + continue - for y in model.designated_values - Xs: # Discard (A, {⊤} ∪ B') subalgebras if top is not None and y == top: @@ -77,36 +89,30 @@ def has_vsp(model: Model, impfunction: ModelFunction, if bottom is not None and negation_defined and y == bottom: continue - # Discard ({a} ∪ A', {b} ∪ B') subalgebras when a <= b - if model.ordering.is_lt(x, y): - continue - - # Discard ({a} ∪ A', {b} ∪ B') subalgebras when b <= a and negation is defined - if negation_defined and model.ordering.is_lt(y, x): - continue - - if y not in C: - C[y] = model_closure({y,}, model.logical_operations, None) - Ys = C[y] + carrier_set_right: Set[ModelValue] = model_closure(C.get(y, {y,}), model.logical_operations, top) + C[y] = carrier_set_right # Discard (A, {⊤} ∪ B') subalgebras - if top is not None and top in Ys: + if top is not None and top in carrier_set_right: continue # Discard (A, {⊥} ∪ B') subalgebras when negation is defined - if bottom is not None and negation_defined and bottom in Ys: + if bottom is not None and negation_defined and bottom in carrier_set_right: continue - if not Xs.isdisjoint(Ys): + # Discard subalgebras that intersect + if not carrier_set_left.isdisjoint(carrier_set_right): continue + # Check whether for all pairs in the subalgebra, + # that implication is falsified. falsified = True - for (xi, yi) in product(Xs, Ys): - if impfunction(xi, yi) in model.designated_values: + for (x2, y2) in product(carrier_set_left, carrier_set_right): + if impfunction(x2, y2) in model.designated_values: falsified = False break if falsified: - return VSP_Result(True, model.name, Xs, Ys) + return VSP_Result(True, model.name, carrier_set_left, carrier_set_right) return VSP_Result(False, model.name)