Optimizing the Performance of Robot Fleets in Production Logistics Scenarios Using SMT Solving

cropped-logo_ths.png                  logo_kbsg-rwth


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

State of the art and own contribution

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.
The research group Theory of Hybrid Systems is developing the SMT solver  SMT-RAT with a special focus on solving quantifier-free non-linear real arithmetic (QF-NRA) problems. Latest improvements strengthened SMT-RAT’s functionality also for integer arithmetic.


Our goal is to significantly improve the current planning approach by employing SMT 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 SMT, 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.

Our aim in this project is to:

  • build formal models for movement, order schedules and deadlines, production processes, and rewards;
  • encode the scheduling problem as an optimization problem;
  • develop and improve optimization in SMT solving;
  • embed an SMT solver in the planning software;
  • evaluate the approach using an existing simulator for the RCLL.


This project is executed in cooperation between different research groups:

We are thankful for support by the ICT project house Foundations of a Digitized Industry, Economy, and Society of RWTH Aachen University.