Searching for Optimal Computations with Explanations

A wide range of tasks in computer science, including formal verification, the design of electronic circuits and computer chips as well as artificial intelligence, can be described with the help of logical expressions and constraints. These expressions can be solved by computers automatically using so-called solvers (programs that implement solution procedures). Solvers are commonly used to address questions in planning and optimisation, which also play an important role in many practical problems. In the health sector, for example, when patients suffer from several chronic diseases at the same time, the question is which combination of drugs and treatments is optimal for an individual patient respecting their personal preferences, so that the best possible effect is achieved and at the same time the risk of undesirable adverse drug reactions or side effects is minimised. The underlying logical expressions and constraints can be very complex and involve many (hundreds) of variables. They can be computed in different ways with existing computer- aided solving methods, depending on whether they are expressions with purely logical conditions or also conditions with numerical parameters. In this project, a general-purpose formal approach based on such existing automated solution procedures will be developed to guide the search for optimal solutions with respect to different criteria (time, completeness, effectiveness, cost, e nergy consumption, etc.). However, the approach should not only calculate optimal solutions, but also make the solution path comprehensible and thus the solutions explainable. Explainability is an important property, because it allows the user to compare different solutions, understand their differences, and guide them in selecting the optimal solution or the optimal calculation approach for the respective application. In this project, logic serves as a unifying tool for modelling, reasoning, searching and explaining optimal computations. The project is led by Dr Juliana Küster Filipe Bowles at the Software Competence Center Hagenberg (SCCH). At SCCH, she will collaborate with researchers from the fields of Software Science and Data Science, making it possible to incorporate and apply project results directly to various practical and industrial applications (e.g. robot control, medical technology, energy supply).