Motivation and research question
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 optimization modulo theories (OMT) solving. While satisfiability modulo theories solving (SMT) solving aims at checking logical formulas for satisfiability, OMT solving also incorporates extensions with optimization capabilities. However, current approaches do not yet exploit the potential of applying OMT 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 plans, with RCLL scenarios serving as benchmarks for the evaluation.
Current results in RCLL
For a robot to fulfill a certain task, a component is necessary that composes basic skills or actions to form a coherent behavior — this is the task-level executive. Typical approaches can be roughly divided in three categories: state-machine-based controllers, reasoning systems from procedural reasoning systems or rule-based agents to more formal approaches like Golog, and finally planning systems with varying complexity and modeling requirements. Hybrid systems may integrate aspects of more categories, e.g. PDDL-based planning and Golog. The approaches can be further characterized as local (plan for single robot) or global (plan for fleet), centralized (one central planner) or distributed (planning is done on all robots and is coordinated), and can produce incremental or full plans. Particular challenges are on-line planning capabilities and flexible plan execution and monitoring systems.
The currently most successful approach is a rule-based, incremental, local reasoning system developed in the research group Knowledge-based Systems, part of the current world champion team in RCLL. Whenever the robot is idle, this approach chooses the best next task according to prioritized situations encoded as a rule-base. Coordination is then performed to avoid multiple robots choosing the same task. This approach relies on a shared world model synchronized over the network.
Our Approach
Our goal is to significantly improve the current planning approach by employing OMT solving to compute optimal strategies, thereby taking also future events and actions of other agents into account, and providing quality guarantees. To do so, we plan to encode the scheduling problem as a linear (mixed-) integer problem which can be solved and optimized by SMT-RAT as well as other solvers like Z3. Note that this problem can not be handled by traditional linear optimization tools, as it includes Boolean combinations of constraints.
The rule-based agent can determine multiple situations to be applicable at run-time during evaluation. This introduces a conflict of competing possible courses of action. Currently, this is resolved by an explicit prioritization of all possible tasks. With the introduction of OMT, this conflict could be resolved more intelligently by looking several steps in the future using an optimization theory to allow for a more informed choice.
Benchmarks
Our collection of SMT-LIB benchmarks for the RoboCup Logistics League can be found here.
Team
This project is carried out in cooperation between different research groups:
RWTH Aachen University, Germany
Erika Abraham
Gerhard Lakemeyer
Francesco Leofante
Tim Niemueller
University of Genoa, Italy