Single-shot solving benchmarks implementation

benchmarks/singleshot/README.md

@@ -0,0 +1,17 @@
+# Singleshot benchmarking for OOASP
+
+In this directory is a collection of `.lp` files defining ooasp for the purposes of singleshot benchmarking, automated python script for running them and resulting outputs of the script.
+
+## Automated Script
+
+The benchmarking is meant to be run using the automated script `autorun.py`, which is to be run from the `singleshot_bench` directory.
+The script works by automatically rewriting the `assumptions.lp` file and then using the Clingo python API to run solving and log the times.
+
+### Domain sizes
+
+The minimal domain sizes are calculated using a python script provided to team members. For now these should be considered the minimal solvable domain sizes.
+
+### Logging
+
+The script currently creates logs of found models in `results/models` and times per iteration in `results/times`.
+Outdated `assumptions.lp` files are not logged by default, but this logging can be switch on by changing the `save` flag in `build_assumptions` function to `True`.

benchmarks/singleshot/autorun.py

@@ -0,0 +1,144 @@
+# Copyright (c) 2022-2024 Siemens AG Oesterreich
+# SPDX-License-Identifier: MIT
+
+import os
+import datetime
+
+from typing import List, Annotated
+
+from clingo import Control
+
+ELEMENT_NAMES = 'ABCD'
+ELEMENT_TYPES = len(ELEMENT_NAMES)
+
+domain_sizes: Annotated[List[int], "Currently known minimal domain sizes calculated by count.py script"] = [
+ 19, 33, 51, 65, 84, 98, 116, 130, 149, 163, 181, 195, 214, 228, 246, 260, 279, 293, 311, 325
+ ]
+
+instances: Annotated[List[int], "Iteration identifications."] = [x+1 for x in range(20)]
+
+
+def generate_ids(n: int) -> List[str]:
+ """
+ Generates combinations of element definitions
+ with suitable IDs.
+ :param n: int, number of elements of each type (e.g. for iteration 4, n=4)
+ :return: list of fact representations strings 
+ """
+
+ ids = [id+1 for id in range(ELEMENT_TYPES*n)]
+ assigned = [ids[i*n:i*n+n] for i in range(ELEMENT_TYPES)]
+ partial_config_facts = []
+
+ for element_index, object_ids in enumerate(assigned):
+ for id in object_ids:
+ partial_config_facts.append(f"user(ooasp_isa(element{ELEMENT_NAMES[element_index]},{id})).")
+
+ return partial_config_facts
+
+
+def rewrite_assumptions(content: List[str], save: bool = True) -> None:
+ """
+ Rewrites the assumptions.lp file to the list of content passed.
+ If save is set to true, creates a legacy directory and saves a copy of existing assumptions to it.
+ :param content: list of configuration facts
+ :param save: if active, saves all the generated files iin the outdated instances directory 
+ """
+
+ if os.path.isfile('instances/assumptions.lp'):
+ if save:
+ os.makedirs('instances/outdated', exist_ok=True)
+ new_file = f"instances/outdated/assumptions{len(content)}{str(datetime.datetime.now()).replace(' ', '_').replace('.', '-').replace(':', '-')}.lp"
+ os.rename('instances/assumptions.lp', new_file)
+ os.makedirs('instances', exist_ok=True)
+ with open('instances/assumptions.lp', 'w') as file:
+ print(" >>Rewriting assumptions.")
+ for t in content:
+ file.write(t+'\n')
+
+
+def add_domain(size: int) -> None:
+ """
+ Adds domain size constraints to the assumption file
+ :param size: size of the domain
+ """
+ with open('instances/assumptions.lp', 'a') as file:
+ t = f'ooasp_domain(object,1..{size}).'
+ file.write(t)
+
+
+def build_assumptions(n: int, save: bool = False) -> None:
+ """
+ Builds the new assumptions file in its entirety.
+ :param n: number of iteration
+ :param save: flag to save old assumption files before rewriting them
+ """
+ partial_config_facts = generate_ids(n)
+ rewrite_assumptions(partial_config_facts, save=save)
+ add_domain(domain_sizes[n-1] if len(domain_sizes) >= n else 100) # 100 is a placeholder value to avoid potential errors
+
+
+def reset_solving() -> Control:
+ """
+ Reinitialises the clingo control.
+ Returns the set up instance.
+ """
+ ctl = Control(["--opt-mode=ignore",
+ "--warn=none"])
+ ctl.load("singleshot.lp")
+ ctl.ground([("base", [])])
+ return ctl
+
+
+def log_model(model, out: bool=False) -> None:
+ """
+ Creates a model directory (if it does not exist)
+ And logs resulting models into files
+ :param model: representation of the model
+ :param out: flag to turn on stdout prints of the model
+ """
+ os.makedirs('results/models', exist_ok=True)
+
+ global timestr
+ new_file = f"results/models/M{iteration}{timestr}.txt"
+ with open(new_file, 'w') as mfile:
+ mfile.write(str(model))
+ if out:
+ print('MODEL:')
+ print(model)
+
+
+def log_results(stats: str, iteration: int, out: bool = False) -> None:
+ """
+ Creates a results directory (if it does not exist)
+ And logs times and results into text files.
+ :param stats: statistics to write into the file
+ :param iteration: identificator of the iteration
+ :param out: flag to activate stdout prints of the results
+ """
+ os.makedirs('results/times', exist_ok=True)
+ global timestr
+ new_file = f"results/times/R{iteration}{timestr}.txt"
+ with open(new_file, 'w') as mfile:
+ mfile.write(stats)
+ if out:
+ print('RESULTS:')
+ print(stats)
+
+
+def on_model(m):
+ """
+ Helper function to control resulting model
+ """
+ log_model(m)
+
+
+if __name__ == "__main__":
+ global timestr
+ timestr = str(datetime.datetime.now()).replace(' ', '_').replace('.', '-').replace(':', '-')
+ for iteration in instances:
+ print(f">>Solving for:{iteration}")
+ build_assumptions(iteration)
+ ctl = reset_solving()
+ ctl.solve(on_model=on_model)
+ log_results(str(ctl.statistics['summary']['times']), iteration, out=True)

benchmarks/singleshot/ooasp.lp

@@ -0,0 +1,28 @@
+% Copyright (c) 2022 Siemens AG Oesterreich
+% SPDX-License-Identifier: MIT
+
+% External Substitutes
+guess.
+check_potential_cv.
+check_permanent_cv.
+% ------------ Base programs
+#const config_name = default_config_name.
+#const kb_name = default_kb_name.
+ooasp_configuration(kb_name,config_name).
+#include "ooasp_aux_kb.lp". % Auxiliary predicates for the KB
+
+
+% ------------ Incremental programs
+%#include "ooasp_user_input.lp". % User input with externals
+#include "ooasp_aux_config.lp". % Auxiliay predicates fot the config
+#include "ooasp_guess.lp". % Guess section
+%#include "ooasp_guess_fclingo.lp". % Guess section
+#include "ooasp_check.lp". % Check section
+%#include "ooasp_check_fclingo.lp". % Check section
+%#include "ooasp_check_user.lp". % Check section
+%#include "ooasp_cautious_opt.lp". % Optimizations used for cautious reasoning
+
+%#include "ooasp_symmetry.lp". % Symmetry breaking constraints THIS BREAKS IT...for now (in original it is not replaced by the variable)
+
+:- user(ooasp_isa(C,new_object)),
+not ooasp_isa(C,new_object).

benchmarks/singleshot/ooasp_aux_config.lp

@@ -0,0 +1,70 @@
+% Copyright (c) 2022-2024 Siemens AG Oesterreich
+% SPDX-License-Identifier: MIT
+
+% Transitive closure when a leaf class is selected via choice
+ooasp_isa(LEAFCLASS,OBJECT) :-
+ ooasp_isa_leaf(LEAFCLASS,OBJECT).
+
+% Transitive closure
+ooasp_isa(SUPER,OBJECT) :-
+ ooasp_isa(SUB,OBJECT),
+ ooasp_subclass(SUB,SUPER).
+
+% Generation of leafs
+ooasp_isa_leaf(C,OBJECT) :-
+ ooasp_isa(C,OBJECT),
+ ooasp_leafclass(C).
+
+ooasp_isa_smallest(SUPER,OBJECT) :-
+ ooasp_isa(SUPER,OBJECT),
+ not ooasp_isa(SUB,OBJECT) :ooasp_subclass(SUB,SUPER).
+
+ooasp_assoc_gen(ASSOC,1,ID1,OBJECT) :-
+ ooasp_associated(ASSOC,ID1,OBJECT).
+
+ooasp_assoc_gen(ASSOC,1,OBJECT,ID2) :-
+ ooasp_associated(ASSOC,OBJECT,ID2).
+
+ooasp_assoc_gen(ASSOC,2,OBJECT,ID1) :-
+ ooasp_associated(ASSOC,ID1,OBJECT).
+
+ooasp_assoc_gen(ASSOC,2,ID2,OBJECT) :-
+ ooasp_associated(ASSOC,OBJECT,ID2).
+
+% Association specialization
+ooasp_associated(ASSOC,OBJECT,ID2) :-
+ ooasp_associated(ASSOC_S,OBJECT,ID2),
+ ooasp_assoc_specialization(ASSOC_S,ASSOC),
+ ooasp_assoc(ASSOC,C1,_,_,C2,_,_),
+ ooasp_isa(C1,OBJECT),
+ ooasp_isa(C2,ID2).
+
+ooasp_associated(ASSOC,ID1,OBJECT) :-
+ ooasp_associated(ASSOC_S,ID1,OBJECT),
+ ooasp_assoc_specialization(ASSOC_S,ASSOC),
+ ooasp_assoc(ASSOC,C1,_,_,C2,_,_),
+ ooasp_isa(C1,ID1),
+ ooasp_isa(C2,OBJECT).
+
+ooasp_associated(ASSOC_S,OBJECT,ID2) :-
+ ooasp_associated(ASSOC,OBJECT,ID2),
+ ooasp_assoc_specialization(ASSOC_S,ASSOC),
+ ooasp_assoc(ASSOC_S,C1,_,_,C2,_,_),
+ ooasp_isa(C1,OBJECT),
+ ooasp_isa(C2,ID2).
+
+ooasp_associated(ASSOC_S,ID1,OBJECT) :-
+ ooasp_associated(ASSOC,ID1,OBJECT),
+ ooasp_assoc_specialization(ASSOC_S,ASSOC),
+ ooasp_assoc(ASSOC_S,C1,_,_,C2,_,_),
+ ooasp_isa(C1,ID1),
+ ooasp_isa(C2,OBJECT).
+
+
+% Int attributes
+
+ooasp_attr_int(OBJECT, A, MIN, MAX):-
+ ooasp_isa(C,OBJECT),
+ ooasp_attr_minInclusive(C,A,MIN),
+ ooasp_attr_maxInclusive(C,A,MAX),
+ ooasp_attr(C,A,int).

benchmarks/singleshot/ooasp_aux_kb.lp

@@ -0,0 +1,52 @@
+% Copyright (c) 2022-2024 Siemens AG Oesterreich
+% SPDX-License-Identifier: MIT
+
+#program base.
+
+#const use_dl = false.
+
+% transitive closure
+ooasp_subclass(SUB,SUPER2) :-
+ ooasp_subclass(SUB,SUPER1),
+ ooasp_subclass(SUPER1,SUPER2).
+
+ooasp_subclass_ref(C1,C2):-ooasp_subclass(C1,C2).
+ooasp_subclass_ref(C,C):-ooasp_class(C).
+
+
+% derive domain for boolean attributes
+ooasp_attr_enum(C,N,"true") :-
+ ooasp_attr(C,N,"boolean").
+ooasp_attr_enum(C,N,"false") :-
+ ooasp_attr(C,N,"boolean").
+
+% true, if attribute has domain
+ooasp_attr_hasdomain(C,N) :-
+ ooasp_attr_enum(C,N,D).
+
+ooasp_attr_enum(C,N,MIN..MAX) :-
+ ooasp_attr(C,N,enumint),
+ ooasp_attr_minInclusive(C,N,MIN),
+ ooasp_attr_maxInclusive(C,N,MAX).
+
+ooasp_attr_fdom(C,N,MIN..MAX) :-
+ ooasp_attr(C,N,int),
+ ooasp_attr_minInclusive(C,N,MIN),
+ ooasp_attr_maxInclusive(C,N,MAX).
+
+% leafclasses are classes without subclasses
+ooasp_leafclass(C) :-
+ ooasp_class(C),
+ not ooasp_subclass(_,C).
+
+ooasp_assoc_limit(ASSOC,min,1,C1,C2MIN,C2):-
+ ooasp_assoc(ASSOC,C1,C1MIN,C1MAX,C2,C2MIN,C2MAX).
+
+ooasp_assoc_limit(ASSOC,max,1,C1,C2MAX,C2):-
+ ooasp_assoc(ASSOC,C1,C1MIN,C1MAX,C2,C2MIN,C2MAX).
+
+ooasp_assoc_limit(ASSOC,min,2,C2,C1MIN,C1):-
+ ooasp_assoc(ASSOC,C1,C1MIN,C1MAX,C2,C2MIN,C2MAX).
+
+ooasp_assoc_limit(ASSOC,max,2,C2,C1MAX,C1):-
+ ooasp_assoc(ASSOC,C1,C1MIN,C1MAX,C2,C2MIN,C2MAX).

benchmarks/singleshot/ooasp_cautious.opt.lp

@@ -0,0 +1,5 @@
+% Copyright (c) 2022-2024 Siemens AG Oesterreich
+% SPDX-License-Identifier: MIT
+
+% Used when getting inferences to minimize on lowerbound errors
+:~ ooasp_cv(lowerbound,ID,_,(ASSOC,CMIN,N,C,OPT,OBJECT)). [CMIN-N@3,(ASSOC,ID)]