From 7b652f36eb753830b857e3d94da258e3b75f7860 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Tue, 13 May 2025 13:22:28 -0400 Subject: [PATCH] Transformed subalgebra generation from exponential to linear --- vsp.py | 153 ++++++++++++++++----------------------------------------- 1 file changed, 41 insertions(+), 112 deletions(-) diff --git a/vsp.py b/vsp.py index e5a715b..1a861f7 100644 --- a/vsp.py +++ b/vsp.py @@ -2,54 +2,13 @@ Check to see if the model has the variable sharing property. """ -from collections import defaultdict -from itertools import chain, combinations, product +from itertools import product from typing import List, Optional, Set, Tuple from common import set_to_str from model import ( - Model, model_closure, ModelFunction, ModelValue, OrderTable + Model, model_closure, ModelFunction, ModelValue ) -class Cache: - def __init__(self): - # input size -> cached (inputs, outputs) - self.c = defaultdict(list) - - def add(self, i: Set[ModelValue], o: Set[ModelValue]): - self.c[len(i)].append((i, o)) - - def get_closest(self, initial_set: Set[ModelValue]) -> Optional[Tuple[Set[ModelValue], bool]]: - """ - Iterate through our cache starting with the cached - inputs closest in size to the initial_set and - find the one that's a subset of initial_set. - - Returns cached_output, and whether the initial_set is the same - as the cached_input. - """ - initial_set_size = len(initial_set) - sizes = range(initial_set_size, 0, -1) - - for size in sizes: - if size not in self.c: - continue - - for cached_input, cached_output in self.c[size]: - if cached_input <= initial_set: - return cached_output, size == initial_set_size - - 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__( self, has_vsp: bool, model_name: Optional[str] = None, @@ -68,38 +27,6 @@ Subalgebra 1: {set_to_str(self.subalgebra1)} Subalgebra 2: {set_to_str(self.subalgebra2)} """ -def quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined) -> bool: - """ - Return True if VSP cannot be satisfied - through some incomplete checks. - """ - # If the left subalgebra contains bottom - # or the right subalgebra contains top - # skip this pair - if top is not None and top in ys: - return True - if negation_defined and bottom is not None and bottom in ys: - return True - if bottom is not None and bottom in xs: - return True - if negation_defined and top is not None and top in xs: - return True - - # If the two subalgebras intersect, move - # onto the next pair. - if not xs.isdisjoint(ys): - return True - - # If the subalgebras are order-dependent, skip this pair - if order_dependent(xs, ys, model.ordering): - return True - if negation_defined and order_dependent(ys, xs, model.ordering): - return True - - # We can't immediately rule out that these - # subalgebras don't exhibit VSP - return False - def has_vsp(model: Model, impfunction: ModelFunction, negation_defined: bool) -> VSP_Result: """ @@ -124,64 +51,66 @@ def has_vsp(model: Model, impfunction: ModelFunction, if impfunction(x, y) not in model.designated_values: I.append((x, y)) - # Construct the powerset of I without the empty set - I_power = chain.from_iterable(combinations(I, r) for r in range(1, len(I) + 1)) - # ((x1, y1)), ((x1, y1), (x2, y2)), ... - - closure_cache = Cache() - # Find the subalgebras which falsify implication - for xys in I_power: + for xys in I: - xs = { xy[0] for xy in xys } - ys = { xy[1] for xy in xys } + xi = xys[0] - if quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined): + # Discard ({⊥} ∪ A', B) subalgebras + if bottom is not None and xi == bottom: continue - orig_xs = xs - cached_xs = closure_cache.get_closest(xs) - if cached_xs is not None: - xs |= cached_xs[0] - - orig_ys = ys - cached_ys = closure_cache.get_closest(ys) - if cached_ys is not None: - ys |= cached_ys[0] - - xs_ys_updated = cached_xs is not None or cached_ys is not None - if xs_ys_updated and quick_vsp_unsat_incomplete(xs, ys, model, top, bottom, negation_defined): + # Discard ({⊤} ∪ A', B) subalgebras when negation is defined + if top is not None and negation_defined and xi == top: continue - # Compute the closure of all operations - # with just the xs - carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, bottom) + yi = xys[1] - # Save to cache - if cached_xs is None or (cached_xs is not None and not cached_xs[1]): - closure_cache.add(orig_xs, carrier_set_left) + # 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(ys, model.logical_operations, top) - - # Save to cache - if cached_ys is None or (cached_ys is not None and not cached_ys[1]): - closure_cache.add(orig_ys, carrier_set_right) + 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 - # If the carrier set intersects, then move on to the next - # subalgebra + # 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 - # See if for all pairs in the subalgebras, that - # implication is falsified + # 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: