From 20ccacc1660497736bb179da04662c9369f85151 Mon Sep 17 00:00:00 2001 From: Brandon Rozek Date: Mon, 15 Apr 2024 00:08:00 -0400 Subject: [PATCH] Some optimizations --- R.py | 34 +++++++++--------- common.py | 4 +++ generate_model.py | 91 ++++++++++++++++++++++++++++++++++++++--------- logic.py | 31 +++++++++------- model.py | 29 ++++++++------- 5 files changed, 132 insertions(+), 57 deletions(-) create mode 100644 common.py diff --git a/R.py b/R.py index 1459066..4eea77b 100644 --- a/R.py +++ b/R.py @@ -23,38 +23,38 @@ x = PropositionalVariable("x") y = PropositionalVariable("y") z = PropositionalVariable("z") - implication_rules = { - Rule({}, Implication(x, x)), + Rule(set(), Implication(x, x)), Rule({Implication(x, y), Implication(y, z)}, Implication(x, z)), - Rule({}, Implication(Implication(x, Implication(x, y)), Implication(x, y))), - Rule({}, Implication(Implication(x, Implication(y, z)), Implication(y, Implication(x, z)))), - Rule({}, Implication(Implication(x, y), Implication(Implication(z, x), Implication(z, y)))), - Rule({}, Implication(Implication(x, y), Implication(Implication(y, z), Implication(x, z)))), + Rule({Implication(x, Implication(x, y)),}, Implication(x, y)), + Rule({Implication(x, Implication(y, z)),}, Implication(y, Implication(x, z))), + Rule({Implication(x, y),}, Implication(Implication(z, x), Implication(z, y))), + Rule({Implication(x, y),}, Implication(Implication(y, z), Implication(x, z))), Rule({Implication(x, y), x}, y) } negation_rules = { - Rule({}, Implication(Negation(Negation(x)), x)), - Rule({}, Implication(x, Negation(Negation(x)))), + Rule({Negation(Negation(x)),}, x), + Rule({x,}, Negation(Negation(x))), Rule({Implication(x, y)}, Implication(Negation(y), Negation(x))), - Rule({}, Implication(Implication(x, y), Implication(Negation(y), Negation(x)))) + Rule({Implication(x, y),}, Implication(Negation(y), Negation(x))) } conjunction_rules = { Rule({y, z}, Conjunction(y, z)), - Rule({}, Implication(Conjunction(x, y), x)), - Rule({}, Implication(Conjunction(x, y), y)), - Rule({}, Implication(Conjunction(Implication(x, y), Implication(x, z)), Implication(x, Conjunction(y, z)))) + Rule({Conjunction(x, y),}, x), + Rule({Conjunction(x, y),}, y), + Rule({Conjunction(Implication(x, y), Implication(x, z)),}, Implication(x, Conjunction(y, z))) } disjunction_rules = { - Rule({}, Implication(x, Disjunction(x, y))), - Rule({}, Implication(y, Disjunction(x, y))), - Rule({}, Implication(Conjunction(Implication(x, z), Implication(y, z)), Implication(Disjunction(x, y), z))), - Rule({}, Implication(Conjunction(x, Disjunction(y, z)), Disjunction(Conjunction(x, y), Conjunction(x, z)))) + Rule({x,}, Disjunction(x, y)), + Rule({y,}, Disjunction(x, y)), + Rule({Conjunction(Implication(x, z), Implication(y, z)),}, Implication(Disjunction(x, y), z)), + Rule({Conjunction(x, Disjunction(y, z)),}, Disjunction(Conjunction(x, y), Conjunction(x, z))) } + logic_rules = implication_rules | negation_rules | conjunction_rules | disjunction_rules operations = {Negation, Conjunction, Disjunction, Implication} @@ -118,7 +118,7 @@ interpretation = { # Generate models of R of a given size model_size = 2 -satisfiable_models = generate_model(R_logic, model_size) +satisfiable_models = generate_model(R_logic, model_size, print_model=True) print(f"There are {len(satisfiable_models)} satisfiable models of element length {model_size}") diff --git a/common.py b/common.py new file mode 100644 index 0000000..32e8e2d --- /dev/null +++ b/common.py @@ -0,0 +1,4 @@ +from typing import Set + +def set_to_str(x: Set) -> str: + return "{" + ", ".join((str(xi) for xi in x)) + "}" diff --git a/generate_model.py b/generate_model.py index f4c4b1a..e7aa93e 100644 --- a/generate_model.py +++ b/generate_model.py @@ -1,9 +1,11 @@ """ File which generates all the models """ -from logic import Logic +from common import set_to_str +from logic import Logic, Operation, Rule, get_operations_from_term, PropositionalVariable from model import ModelValue, Model, satisfiable, ModelFunction from itertools import combinations, chain, product +from typing import Set def possible_designations(iterable): """Powerset without the empty and complete set""" @@ -23,13 +25,59 @@ def possible_functions(operation, carrier_set): yield ModelFunction(new_function, operation.symbol) -def possible_interpretations(logic, carrier_set): + +def only_rules_with(rules: Set[Rule], operation: Operation) -> Set[Rule]: + result_rules = [] + for rule in rules: + is_valid = True + for t in (rule.premises | {rule.conclusion,}): + t_operations = get_operations_from_term(t) + if len(t_operations) > 1: + is_valid = False + break + if len(t_operations) == 0: + continue + t_operation = next(iter(t_operations)) + if t_operation != operation: + is_valid = False + break + if is_valid: + result_rules.append(rule) + return result_rules + + + +def possible_interpretations( + logic: Logic, carrier_set: Set[ModelValue], + designated_values: Set[ModelValue]): operations = [] model_functions = [] for operation in logic.operations: operations.append(operation) - model_functions.append(possible_functions(operation, carrier_set)) + candidate_functions = list(possible_functions(operation, carrier_set)) + passed_functions = [] + """ + Only consider functions that at least pass + in the rules with the operation by itself. + """ + restricted_rules = only_rules_with(logic.rules, operation) + if len(restricted_rules) > 0: + small_logic = Logic({operation,}, restricted_rules) + for f in candidate_functions: + small_model = Model(carrier_set, {f,}, designated_values) + interp = {operation: f} + if satisfiable(small_logic, small_model, interp): + passed_functions.append(f) + else: + passed_functions = candidate_functions + if len(passed_functions) == 0: + raise Exception("No interpretation satisfies the axioms for the operation " + str(operation)) + else: + print( + f"Operation {operation.symbol} has {len(passed_functions)} candidate functions" + ) + model_functions.append(passed_functions) functions_choice = product(*model_functions) for functions in functions_choice: @@ -39,25 +87,36 @@ def possible_interpretations(logic, carrier_set): interpretation[operation] = function yield interpretation -def generate_model(logic: Logic, number_elements: int): +def generate_model(logic: Logic, number_elements: int, num_solutions: int = -1, print_model=False): carrier_set = { ModelValue("a" + str(i)) for i in range(number_elements) } possible_designated_values = possible_designations(carrier_set) - possible_interps = possible_interpretations(logic, carrier_set) satisfied_models = [] - checked = 0 - for designated_values, interpretation in product(possible_designated_values, possible_interps): - checked += 1 + for designated_values in possible_designated_values: designated_values = set(designated_values) - - model = Model(carrier_set, set(interpretation.values()), designated_values) - if satisfiable(logic, model, interpretation): - satisfied_models.append(model) - print(model) - - print("Checked", checked) - + print("Considering models for designated values", set_to_str(designated_values)) + possible_interps = possible_interpretations(logic, carrier_set, designated_values) + + for interpretation in possible_interps: + is_valid = True + model = Model(carrier_set, set(interpretation.values()), designated_values) + # Iteratively test possible interpretations + # by adding one axiom at a time + for rule in logic.rules: + small_logic = Logic(logic.operations, {rule,}) + if not satisfiable(small_logic, model, interpretation): + is_valid = False + break + + if is_valid: + satisfied_models.append(model) + if print_model: + print(model, flush=True) + + if num_solutions >= 0 and len(satisfied_models) >= num_solutions: + return satisfied_models + return satisfied_models diff --git a/logic.py b/logic.py index 8c4980d..b38bbdd 100644 --- a/logic.py +++ b/logic.py @@ -1,4 +1,4 @@ -from typing import Any, Set +from typing import Any, Set, Tuple from functools import lru_cache class Operation: @@ -38,14 +38,10 @@ class PropositionalVariable(Term): def __hash__(self): return self.hashed_value - # def __setattr__(self, name: str, value: Any): - # raise Exception("Propositional variables are immutable") + def __str__(self): return self.name -# def PropTerm(Term): -# def __init__(self, v: PropositionalVariable): -# self.v = v class OpTerm(Term): def __init__(self, operation: Operation, arguments): @@ -65,12 +61,12 @@ class OpTerm(Term): arg_strs = [str(a) for a in self.arguments] return self.operation.symbol + "(" + ",".join(arg_strs) + ")" +# Standard operators Negation = Operation("¬", 1) Conjunction = Operation("∧", 2) Disjunction = Operation("∨", 2) Implication = Operation("→", 2) - class Inequation: def __init__(self, antecedant : Term, consequent: Term): self.antecedant = antecedant @@ -104,18 +100,19 @@ class Logic: self.rules = rules -def get_prop_var_from_term(t: Term): +def get_prop_var_from_term(t: Term) -> Set[PropositionalVariable]: if isinstance(t, PropositionalVariable): return {t,} - result = set() + result: Set[PropositionalVariable] = set() for arg in t.arguments: result |= get_prop_var_from_term(arg) return result -def get_propostional_variables(rules): - vars = set() +@lru_cache +def get_propostional_variables(rules: Tuple[Rule]) -> Set[PropositionalVariable]: + vars: Set[PropositionalVariable] = set() for rule in rules: # Get all vars in premises @@ -125,4 +122,14 @@ def get_propostional_variables(rules): # Get vars in conclusion vars |= get_prop_var_from_term(rule.conclusion) - return vars \ No newline at end of file + return vars + +def get_operations_from_term(t: Term) -> Set[Operation]: + if isinstance(t, PropositionalVariable): + return set() + + result: Set[Operation] = {t.operation,} + for arg in t.arguments: + result |= get_operations_from_term(arg) + + return result diff --git a/model.py b/model.py index efa4cf4..e5a325b 100644 --- a/model.py +++ b/model.py @@ -1,18 +1,18 @@ """ Defining what it means to be a model """ +from common import set_to_str from logic import ( PropositionalVariable, get_propostional_variables, Logic, Term, Operation ) -from typing import Set, List, Dict +from typing import Set, List, Dict, Tuple from itertools import product +from functools import lru_cache __all__ = ['ModelValue', 'ModelFunction', 'Model'] -def set_to_str(x): - return "{" + ", ".join((str(xi) for xi in x)) + "}" class ModelValue: def __init__(self, name): @@ -80,7 +80,7 @@ Designated Values: {set_to_str(self.designated_values)} return result -def evaluate_term(t: Term, f: Dict[PropositionalVariable, ModelValue], interpretation: Dict[Operation, ModelFunction]): +def evaluate_term(t: Term, f: Dict[PropositionalVariable, ModelValue], interpretation: Dict[Operation, ModelFunction]) -> ModelValue: if isinstance(t, PropositionalVariable): return f[t] @@ -93,24 +93,28 @@ def evaluate_term(t: Term, f: Dict[PropositionalVariable, ModelValue], interpret return model_function(*model_arguments) def all_model_valuations( - pvars: Set[PropositionalVariable], - mvalues: Set[ModelValue]): + pvars: Tuple[PropositionalVariable], + mvalues: Tuple[ModelValue]): - pvars = list(pvars) possible_valuations = [mvalues for _ in pvars] all_possible_values = product(*possible_valuations) for valuation in all_possible_values: - mapping = dict() + mapping: Dict[PropositionalVariable, ModelValue] = dict() assert len(pvars) == len(valuation) for pvar, value in zip(pvars, valuation): mapping[pvar] = value yield mapping - -def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, ModelFunction]): - pvars = get_propostional_variables(logic.rules) - mappings = all_model_valuations(pvars, model.carrier_set) +@lru_cache +def all_model_valuations_cached( + pvars: Tuple[PropositionalVariable], + mvalues: Tuple[ModelValue]): + return list(all_model_valuations(pvars, mvalues)) + +def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, ModelFunction]) -> bool: + pvars = tuple(get_propostional_variables(tuple(logic.rules))) + mappings = all_model_valuations_cached(pvars, tuple(model.carrier_set)) for mapping in mappings: for rule in logic.rules: @@ -120,6 +124,7 @@ def satisfiable(logic: Logic, model: Model, interpretation: Dict[Operation, Mode if t not in model.designated_values: premise_met = False break + if not premise_met: continue