Optimizing the Performance of Robot Fleets in Production Logistics Scenarios Using SMTKBSG
Manufacturing industries are on the brink of widely accepting a new paradigm for organizing
production by introducing perceiving, active, context-aware, and autonomous systems. This is
often referred to as Industry~4.0, a move from static process chains towards more automation and
autonomy. The corner stones for this paradigm shift are smart factories, which is a context-aware
facility in which manufacturing steps are considered as services that can be combined efficiently
and flexibly, allowing for the production of various product types and variants in small lot sizes.
In particular, managing and optimizing the in-factory supply chain carried out by a fleet of robots
becomes a crucial factor, yet to date this problem remains largely unsolved. The RoboCup Logistics
League (RCLL) provides a realistic testbed to study this problem at a comprehensible and manageable
scale, where groups of robots need to maintain and optimize the material flow according to dynamic
orders in a simplified factory environment. Though there are successful symbolic reasoning methods
towards solving the underlying scheduling problem, a disadvantage of these methods is that they
provides no guarantees about the quality of the solution.
A promising approach to solve this problem is offered by the recently emerging field of
satisfiability modulo theories (SMT) solving. SMT solving aims at checking logical formulas for
satisfiability, whereas latest developments also incorporate extensions towards functionalities for
optimization. However, current approaches do not yet exploit the potential of applying SMT solving
to achieve guaranteed-quality solutions for the above problem. This project aims at combining the
techniques from these two fields to arrive at optimized schedules, with RCLL scenarios serving as
benchmarks for the evaluation.