From 4b907281a55e3c71de66e81b4e98b425381b8757 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Fri, 31 Jan 2025 17:16:25 -0500 Subject: [PATCH 1/2] Implementing optimization #14 Discard subalgebras which are order-dependent --- model.py | 16 ++++++++++++++++ parse_magic.py | 15 ++++++++++----- vsp.py | 18 +++++++++++++++++- 3 files changed, 43 insertions(+), 6 deletions(-) diff --git a/model.py b/model.py index 2fff5ac..0451cfc 100644 --- a/model.py +++ b/model.py @@ -103,18 +103,34 @@ def binary_function_str(f: ModelFunction) -> str: Interpretation = Dict[Operation, ModelFunction] +class OrderTable: + def __init__(self): + self.ordering = set() + + def add(self, x, y): + """ + Add x <= y + """ + self.ordering.add((x, y)) + + def is_lt(self, x, y): + return (x, y) in self.ordering + + class Model: def __init__( self, carrier_set: Set[ModelValue], logical_operations: Set[ModelFunction], designated_values: Set[ModelValue], + ordering: Optional[OrderTable] = None, name: Optional[str] = None ): assert designated_values <= carrier_set self.carrier_set = carrier_set self.logical_operations = logical_operations self.designated_values = designated_values + self.ordering = ordering self.name = str(abs(hash(( frozenset(carrier_set), frozenset(logical_operations), diff --git a/parse_magic.py b/parse_magic.py index bab221a..78ca826 100644 --- a/parse_magic.py +++ b/parse_magic.py @@ -6,7 +6,7 @@ Assumes the base logic is R with no extra connectives import re from typing import TextIO, List, Optional, Tuple, Set, Dict -from model import Model, ModelValue, ModelFunction +from model import Model, ModelValue, ModelFunction, OrderTable from logic import ( Implication, Conjunction, @@ -65,6 +65,7 @@ class ModelBuilder: self.size : int = 0 self.carrier_set : Set[ModelValue] = set() self.mnegation: Optional[ModelFunction] = None + self.ordering: Optional[OrderTable] = None self.mconjunction: Optional[ModelFunction] = None self.mdisjunction: Optional[ModelFunction] = None self.designated_values: Set[ModelValue] = set() @@ -278,7 +279,8 @@ def process_orders(infile: SourceFile, current_model_parts: ModelBuilder) -> boo if result is None: return False - mconjunction, mdisjunction = result + ordering, mconjunction, mdisjunction = result + current_model_parts.ordering = ordering current_model_parts.mconjunction = mconjunction current_model_parts.mdisjunction = mdisjunction @@ -334,7 +336,7 @@ def process_model(model_name: str, mp: ModelBuilder, solutions: List[Tuple[Mode assert mp.mimplication is not None logical_operations = { mp.mimplication } - model = Model(mp.carrier_set, logical_operations, mp.designated_values, name=model_name) + model = Model(mp.carrier_set, logical_operations, mp.designated_values, ordering=mp.ordering, name=model_name) interpretation = { Implication: mp.mimplication } @@ -466,7 +468,7 @@ def determine_dresult(size: int, ordering: Dict[ModelValue, ModelValue], a: Mode if not invalid: return c -def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFunction, ModelFunction]]: +def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[OrderTable, ModelFunction, ModelFunction]]: """ Parse the line representing the ordering table """ @@ -478,6 +480,7 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun assert len(table) == (size + 1)**2, f"Order table doesn't match expected size at line {infile.current_line}" + ordering = OrderTable() omapping = {} table_i = 0 @@ -486,6 +489,8 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun for j in range(size + 1): y = mvalue_from_index(j) omapping[(x, y)] = table[table_i] == '1' + if table[table_i] == '1': + ordering.add(x, y) table_i += 1 cmapping = {} @@ -514,7 +519,7 @@ def parse_single_order(infile: SourceFile, size: int) -> Optional[Tuple[ModelFun mconjunction = ModelFunction(2, cmapping, "∧") mdisjunction = ModelFunction(2, dmapping, "∨") - return mconjunction, mdisjunction + return ordering, mconjunction, mdisjunction def parse_single_designated(infile: SourceFile, size: int) -> Optional[Set[ModelValue]]: """ diff --git a/vsp.py b/vsp.py index ad2849b..df18341 100644 --- a/vsp.py +++ b/vsp.py @@ -6,7 +6,7 @@ from itertools import chain, combinations, product from typing import Dict, List, Optional, Set, Tuple from common import set_to_str from model import ( - Model, model_closure, ModelFunction, ModelValue + Model, model_closure, ModelFunction, ModelValue, OrderTable ) from logic import Conjunction, Disjunction, Implication, Operation @@ -79,6 +79,15 @@ def find_bottom(algebra: Set[ModelValue], mconjunction: Optional[ModelFunction], print("[Warning] Failed to find the bottom of the lattice") 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__( @@ -111,6 +120,8 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod if len(model.designated_values) == 1: return VSP_Result(False, model.name) + assert model.ordering is not None, "Expected ordering table in model" + # Compute I the set of tuples (x, y) where # x -> y does not take a designiated value I: Set[Tuple[ModelValue, ModelValue]] = set() @@ -158,6 +169,11 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod if bottom is not None and bottom in xs: continue + # NOTE: Optimization + # If the subalgebras are order-dependent, skip this pair + if order_dependent(xs, ys, model.ordering): + continue + # Compute the closure of all operations # with just the xs carrier_set_left: Set[ModelValue] = model_closure(xs, model.logical_operations, bottom) From d431030b418edd5971e22a850428f5d6b1d11022 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Sun, 9 Feb 2025 11:28:09 -0500 Subject: [PATCH 2/2] Added case for when negation is defined --- vsp.py | 7 ++++++- vspursuer.py | 11 ++++++----- 2 files changed, 12 insertions(+), 6 deletions(-) diff --git a/vsp.py b/vsp.py index df18341..26d9d28 100644 --- a/vsp.py +++ b/vsp.py @@ -107,7 +107,10 @@ Subalgebra 1: {set_to_str(self.subalgebra1)} Subalgebra 2: {set_to_str(self.subalgebra2)} """ -def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[ModelFunction] = None, mdisjunction: Optional[ModelFunction] = None) -> VSP_Result: +def has_vsp(model: Model, impfunction: ModelFunction, + mconjunction: Optional[ModelFunction] = None, + mdisjunction: Optional[ModelFunction] = None, + mnegation: Optional[ModelFunction] = None) -> VSP_Result: """ Checks whether a model has the variable sharing property. @@ -173,6 +176,8 @@ def has_vsp(model: Model, impfunction: ModelFunction, mconjunction: Optional[Mod # If the subalgebras are order-dependent, skip this pair if order_dependent(xs, ys, model.ordering): continue + if mnegation is not None and order_dependent(ys, xs, model.ordering): + continue # Compute the closure of all operations # with just the xs diff --git a/vspursuer.py b/vspursuer.py index 66716a3..72b4615 100755 --- a/vspursuer.py +++ b/vspursuer.py @@ -3,7 +3,7 @@ from os import cpu_count import argparse import multiprocessing as mp -from logic import Conjunction, Disjunction, Implication +from logic import Conjunction, Disjunction, Negation, Implication from parse_magic import SourceFile, parse_matrices from vsp import has_vsp, VSP_Result @@ -24,19 +24,20 @@ if __name__ == "__main__": # NOTE: When subprocess gets spawned, the logical operations will # have a different memory address than what's expected in interpretation. - # This will make it so that we can pass the model functions directly instead. + # Therefore, we need to pass the model functions directly instead. solutions_expanded = [] for model, interpretation in solutions: impfunction = interpretation[Implication] mconjunction = interpretation.get(Conjunction) mdisjunction = interpretation.get(Disjunction) - solutions_expanded.append((model, impfunction, mconjunction, mdisjunction)) + mnegation = interpretation.get(Negation) + solutions_expanded.append((model, impfunction, mconjunction, mdisjunction, mnegation)) num_has_vsp = 0 with mp.Pool(processes=max(cpu_count() - 2, 1)) as pool: results = [ - pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction,)) - for model, impfunction, mconjunction, mdisjunction in solutions_expanded + pool.apply_async(has_vsp, (model, impfunction, mconjunction, mdisjunction, mnegation)) + for model, impfunction, mconjunction, mdisjunction, mnegation in solutions_expanded ] for i, result in enumerate(results):