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