From 3b535fdfa52a88732e97a65bb355f03246deec79 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Thu, 3 Oct 2024 21:38:15 -0400 Subject: [PATCH 1/3] Optimization: Discard subalgebras with bottom/top Currently this doesn't work since it discards the subalgebras {a3} and {a2} which show VSP for R using Model 5.2.1.1.3 --- vsp.py | 41 ++++++++++++++++++++++++++++++++++++++--- 1 file changed, 38 insertions(+), 3 deletions(-) diff --git a/vsp.py b/vsp.py index 23d6beb..52d9f43 100644 --- a/vsp.py +++ b/vsp.py @@ -8,7 +8,7 @@ from common import set_to_str from model import ( Model, model_closure, ModelFunction, ModelValue ) -from logic import Implication, Operation +from logic import Conjunction, Disjunction, Implication, Operation def preseed( initial_set: Set[ModelValue], @@ -38,6 +38,33 @@ def preseed( same_set = candidate_preseed[1] == 0 return candidate_preseed[0], same_set +def has_top_bottom(subalgebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]): + """ + Checks the subalgebra to see whether it + contains a top or bottom element. + + Note: This does not compute the closure. + + By definition, + The top element is any element x where x || x = x + The bottom element is any element x where x && x = x + """ + if mconjunction is None or mdisjunction is None: + return False + + for x in subalgebra: + if mconjunction(x, x) == x: + # print("Bottom Element Found") + return True + + if mdisjunction(x, x) == x: + # print("Top Element Found") + return True + + return False + + + class VSP_Result: def __init__( self, has_vsp: bool, model_name: Optional[str] = None, @@ -62,6 +89,8 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP sharing property. """ impfunction = interpretation[Implication] + mconjunction = interpretation.get(Conjunction) + mdisjunction = interpretation.get(Disjunction) # Compute I the set of tuples (x, y) where # x -> y does not take a designiated value @@ -96,11 +125,17 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP # NOTE: Optimziation before model_closure - # If the carrier set intersects, then move on to the next - # subalgebra + # If the two subalgebras intersect, move + # onto the next pair if len(xs & ys) > 0: continue + # NOTE: Optimization + # if either subalgebra contains top or bottom, move + # onto the next pair + if has_top_bottom(xs, mconjunction, mdisjunction) or has_top_bottom(ys, mconjunction, mdisjunction): + continue + # Compute the closure of all operations # with just the xs carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations) From bed3d09f4abcb9c4c98784af3df757dfeed9912c Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Thu, 24 Oct 2024 21:38:36 -0400 Subject: [PATCH 2/3] Check for top and bottom within subalgebra --- vsp.py | 49 ++++++++++++++++++++++++++++++------------------- 1 file changed, 30 insertions(+), 19 deletions(-) diff --git a/vsp.py b/vsp.py index 52d9f43..27994c0 100644 --- a/vsp.py +++ b/vsp.py @@ -38,31 +38,38 @@ def preseed( same_set = candidate_preseed[1] == 0 return candidate_preseed[0], same_set -def has_top_bottom(subalgebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]): + +def find_top(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]) -> Optional[ModelValue]: """ - Checks the subalgebra to see whether it - contains a top or bottom element. - - Note: This does not compute the closure. - - By definition, - The top element is any element x where x || x = x - The bottom element is any element x where x && x = x + Find the top of the order lattice. + T || a = T, T && a = a for all a in the carrier set """ if mconjunction is None or mdisjunction is None: - return False + return None - for x in subalgebra: - if mconjunction(x, x) == x: - # print("Bottom Element Found") - return True + for x in algebra: + for y in algebra: + if mdisjunction(x, y) == x and mconjunction(x, y) == y: + return x - if mdisjunction(x, x) == x: - # print("Top Element Found") - return True + print("[Warning] Failed to find the top of the lattice") + return None - return False +def find_bottom(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction], mdisjunction: Optional[ModelFunction]) -> Optional[ModelValue]: + """ + Find the bottom of the order lattice + F || a = a, F && a = F for all a in the carrier set + """ + if mconjunction is None or mdisjunction is None: + return None + for x in algebra: + for y in algebra: + if mdisjunction(x, y) == y and mconjunction(x, y) == x: + return x + + print("[Warning] Failed to find the bottom of the lattice") + return None class VSP_Result: @@ -91,6 +98,8 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP impfunction = interpretation[Implication] mconjunction = interpretation.get(Conjunction) mdisjunction = interpretation.get(Disjunction) + top = find_top(model.carrier_set, mconjunction, mdisjunction) + bottom = find_bottom(model.carrier_set, mconjunction, mdisjunction) # Compute I the set of tuples (x, y) where # x -> y does not take a designiated value @@ -133,7 +142,9 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP # NOTE: Optimization # if either subalgebra contains top or bottom, move # onto the next pair - if has_top_bottom(xs, mconjunction, mdisjunction) or has_top_bottom(ys, mconjunction, mdisjunction): + if top is not None and (top in xs or top in ys): + continue + if bottom is not None and (bottom in xs or bottom in ys): continue # Compute the closure of all operations From af81342a7421f006f7da73af3c0ded50aa55c9e2 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Wed, 30 Oct 2024 16:11:03 -0400 Subject: [PATCH 3/3] Break out of saturation computation early when top/bottom are found --- model.py | 36 +++++++++++++++++++++++++++++++++++- vsp.py | 13 +++++++++++-- 2 files changed, 46 insertions(+), 3 deletions(-) diff --git a/model.py b/model.py index 46406b5..d15d094 100644 --- a/model.py +++ b/model.py @@ -219,15 +219,18 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode -def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]): +def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction], top: Optional[ModelValue], bottom: Optional[ModelValue]) -> Set[ModelValue]: """ Given an initial set of model values and a set of model functions, compute the complete set of model values that are closed under the operations. + + If top or bottom is encountered, then we end the saturation procedure early. """ closure_set: Set[ModelValue] = initial_set last_new: Set[ModelValue] = initial_set changed: bool = True + topbottom_found = False while changed: changed = False @@ -251,6 +254,18 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]): if element not in closure_set: new_elements.add(element) + # Optimization: Break out of computation + # early when top or bottom element is foun + if top is not None and element == top: + topbottom_found = True + if bottom is not None and element == bottom: + topbottom_found = True + if topbottom_found: + break + + if topbottom_found: + break + # We don't need to compute the arguments # thanks to the cache, so move onto the # next function. @@ -274,8 +289,27 @@ def model_closure(initial_set: Set[ModelValue], mfunctions: Set[ModelFunction]): if element not in closure_set: new_elements.add(element) + # Optimization: Break out of computation + # early when top or bottom element is foun + if top is not None and element == top: + topbottom_found = True + if bottom is not None and element == bottom: + topbottom_found = True + if topbottom_found: + break + + if topbottom_found: + break + + if topbottom_found: + break + + closure_set.update(new_elements) changed = len(new_elements) > 0 last_new = new_elements + if topbottom_found: + break + return closure_set diff --git a/vsp.py b/vsp.py index 27994c0..6982c16 100644 --- a/vsp.py +++ b/vsp.py @@ -149,21 +149,30 @@ def has_vsp(model: Model, interpretation: Dict[Operation, ModelFunction]) -> VSP # Compute the closure of all operations # with just the xs - carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations) + carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, top, bottom) # Save to cache if cached_xs[0] is not None and not cached_ys[1]: closure_cache.append((orig_xs, carrier_set_left)) + if top is not None and top in carrier_set_left: + continue + if bottom is not None and bottom 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) + carrier_set_right: Set[ModelValue] = model_closure(ys, model.logical_operations, top, bottom) # Save to cache if cached_ys[0] is not None and not cached_ys[1]: closure_cache.append((orig_ys, carrier_set_right)) + if top is not None and top in carrier_set_right: + continue + if bottom is not None and bottom in carrier_set_right: + continue # If the carrier set intersects, then move on to the next # subalgebra