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)]