Single-shot solving benchmarks implementation

singleshot_bench/README.md

@@ -0,0 +1,17 @@
+# Singleshot benchmarking for OOASP
+
+In this directory is collection of `.lp` files defining ooasp for 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 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 times.
+
+### Domain sizes
+
+As of now, the domain sizes (which need to be specified for singleshot) are only roughly approximated by formula: `n*19`, as the smallest configuration given one element of each type is 19. *Better approximation is to be further developed*.
+
+### 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`.

singleshot_bench/autorun.py

@@ -0,0 +1,129 @@
+# Copyright (c) 2022-2024 Siemens AG Oesterreich
+# SPDX-License-Identifier: MIT
+
+import os
+import datetime
+
+from typing import List
+
+from clingo import Control
+
+ELEMENT_TYPES = 4
+ELEMENT_NAMES = 'ABCD'
+
+domain_sizes = [19, 33, 51, 65, 84, 98, 116, 130, 149, 163, 181, 195, 214, 228, 246, 260, 279, 293, 311, 325]
+o_instances = [x+1 for x in range(20)]
+
+
+def generate_ids(n: int) -> List:
+    """
+    Generates combinations of element definitions
+    with suitable IDs.
+    """
+
+    ids = [id+1 for id in range(ELEMENT_TYPES*n)]
+    assigned = [ids[i*n:i*n+n] for i in range(ELEMENT_TYPES)]
+    terms = []
+
+    for letter, category in enumerate(assigned):
+        for id in category:
+            terms.append(f"ooasp_isa(element{ELEMENT_NAMES[letter]},{id}).")
+
+    return terms
+
+
+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.
+    """
+
+    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(n: int) -> None:
+    """
+    Adds domain size constraints to the assumption file
+    """
+    with open('instances/assumptions.lp', 'a') as file:
+        t = f'ooasp_domain(object,1..{n}).'
+        file.write(t)
+
+
+def build_assumptions(n: int, save: bool = False) -> None:
+    """
+    Builds the new assumptions file in its entirety.
+    """
+    ts = generate_ids(n)
+    rewrite_assumptions(ts, save=save)
+    add_domain(domain_sizes[n-1] if len(domain_sizes) >= n else 100)
+
+
+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=False):
+    """
+    Creates a model directory (if it does not exist)
+    And logs resulting models into files
+    """
+    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):
+    """
+    Creates a results directory (if it does not exist)
+    And logs times and results into text files.
+    """
+    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 model
+    model = None
+    global timestr
+    timestr = str(datetime.datetime.now()).replace(' ', '_').replace('.', '-').replace(':', '-')
+    for iteration in o_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)

singleshot_bench/ooasp.lp

@@ -0,0 +1,31 @@
+% 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
+%#external guess. % The guessing part is active
+%#external check_potential_cv. % Checks for potential constraints apply
+%#external check_permanent_cv. % Checks for permanent constraints apply
+
+
+% ------------ 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).

singleshot_bench/ooasp_aux_config.lp

@@ -0,0 +1,80 @@
+% Copyright (c) 2022 Siemens AG Oesterreich
+% SPDX-License-Identifier: MIT
+
+%#program domain(new_object, cls).
+
+%#external active(OBJECT). % Active id for arity constraints
+%ooasp_domain(cls,OBJECT).
+
+% 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).
+
+% Auxiliary predicate to avoid duplicated rules
+% ooasp_assoc_gen(ASSOC,POS,ID1,ID2)
+%    Object ID1 apearing in position POS of association ASSOC is associated to object ID2
+%    Example: ooasp_assoc_gen(c1,ass,2,23,10): : object 23 of the second class of association ass is associated with object 10
+
+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).

singleshot_bench/ooasp_aux_kb.lp

@@ -0,0 +1,56 @@
+% Copyright (c) 2022 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)
+% The association ASSOC must be from a C1 object to at least C2MIN objects of class C2
+
+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).

singleshot_bench/ooasp_cautious.opt.lp

@@ -0,0 +1,23 @@
+% Copyright (c) 2022 Siemens AG Oesterreich
+% SPDX-License-Identifier: MIT
+
+
+%#program domain(OBJECT, cls).
+
+% Used when getting inferences to minimize on lowerbound errors
+:~ ooasp_cv(lowerbound,ID,_,(ASSOC,CMIN,N,C,OPT,OBJECT)). [CMIN-N@3,(ASSOC,ID)]
+
+% % Penalize the bigger associations
+
+% :~ ooasp_isa_leaf(C1,ID3), % Instanciates ID3
+%       ooasp_isa_leaf(C2,ID1),
+%       not user(ooasp_associated(A, ID3, ID1)),
+%       not ooasp_assoc_specialization(A, _), % Only count the super
+%       ooasp_associated(A, ID3, ID1). [ID1@2,(A,ID3)]
+
+
+% :~ ooasp_isa_leaf(C1,ID3), % Instanciates ID3
+%       ooasp_isa_leaf(C2,ID1),
+%       not user(ooasp_associated(A, ID1, ID3)),
+%       not ooasp_assoc_specialization(A, _), % Only count the super
+%       ooasp_associated(A, ID1, ID3). [ID1@1,(A,ID3)]