mirror of
https://github.com/Brandon-Rozek/matmod.git
synced 2025-07-29 20:52:01 +00:00
Transformed subalgebra generation from exponential to linear
This commit is contained in:
parent
214e9ba658
commit
7b652f36eb
1 changed files with 41 additions and 112 deletions
153
vsp.py
153
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:
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue