Keywords

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Task planning is the problem of finding a sequence of abstract actions, described at the symbolic level as causal (temporal, spatial) relations in a state transition system, allowing to reach a desired goal state—see, e.g., [11] for a recent account on the subject. In the era of smart factories, i.e., responsive, adaptive, connective manufacturingFootnote 1, the achievements of task planning research undergo severe challenges when practical applications are in order. Consider a plant that can produce different items on demand. Once a new product request arrives, a robot would probably take the order, assemble it, pack it and prepare it for delivery. With an increasing number of orders, large teams of robots would be needed to keep the business running. Each robot in the team would have to come up with an efficient plan to deliver its order, all while considering what other robots do so as to avoid interferences. Optimality targets like minimizing overall energy consumption or time to delivery, must be taken into account as well.

Task planning in domains as the one just described is an intricate problem that requires reasoning about temporal and ordering constraints efficiently. Although the nature of the constraints involved may vary considerably, the problem remains challenging even in the simplest settings [12]. In order to enable practical application of planning algorithms, relatively fast planners have been developed which rely on heuristics to speed up computations. However, heuristics typically lack performance guarantees, which can be critical to maintain efficiency [3].

In order to study possible solutions to the above problems at a manageable scale, the RoboCup Logistics League (RCLL) [26] has been proposed as a simplified, yet realistic, testbed. Efficient heuristic approaches exist to solve the RCLL [14, 25]. However, these methods cannot provide guarantees on the quality of the solutions they produce. To account for this problem, we propose to cast the task planning problem in the framework of Optimization Modulo Theories (OMT): combining symbolic reachability techniques and optimization, OMT solvers [5, 32] can be leveraged to generate plans with formal performance guarantees by reasoning on expressive models that combine temporal and ordering constraints on tasks and robots.

In the following we discuss our experience using OMT decision procedures to synthesize optimal plans within the RoboCup Logistics League. Besides presenting our results, we discuss challenges and possible directions for future development of OMT planning.

2 Satisfiability Modulo Theories and Optimization

Satisfiability Modulo Theories (SMT) is the problem of deciding the satisfiability of a first-order formula with respect to some decidable theory \(\mathcal {T}\). In particular, SMT generalizes Boolean satisfiability (SAT) by adding background theories such as the theory of real numbers, integers, and the theories of data structures.

To decide the satisfiability of an input formula \(\varphi \) in CNF, SMT solvers such as [9, 10, 23] typically proceed as follows. First a Boolean abstraction \(\textit{abs}(\varphi )\) of \(\varphi \) is built by replacing each constraint by a fresh Boolean proposition. A SAT solver searches for a satisfying assignment S for \(\textit{abs}(\varphi )\). If no such assignment exists then the input formula \(\varphi \) is unsatisfiable. Otherwise, the consistency of the assignment in the underlying theory is checked by a theory solver. If the constraints are consistent then a satisfying solution (model) is found for \(\varphi \). Otherwise, the theory solver returns a theory lemma \(\varphi _E\) giving an explanation for the conflict, e.g., the negated conjunction of some inconsistent input constraints. The explanation is used to refine the Boolean abstraction \(\textit{abs}(\varphi )\) to \(\textit{abs}(\varphi )\wedge \textit{abs}(\varphi _E)\). These steps are iteratively executed until either a theory-consistent Boolean assignment is found, or no more Boolean satisfying assignments exist.

Standard decision procedures for SMT have been extended with optimization capabilities, leading to Optimization Modulo Theories (OMT). OMT extends SMT solving with optimization procedures to find a variable assignment that defines an optimal value for an objective function f (or a combination of multiple objective functions) under all models of a formula \(\varphi \). As noted in [31], OMT solvers such as [5, 32] typically implement a linear search scheme, which can be summarized as follows. Let \(\varphi _S\) be the conjunction of all theory constraints that are true under S and the negation of those that are false under S. A local optimum \(\mu \) for f is computedFootnote 2 under the side condition \(\varphi _S\) and \(\varphi \) is updated as

$$\begin{aligned} \varphi := \varphi \wedge (f \bowtie \mu ) \wedge \lnot \bigwedge \varphi _S,\quad \bowtie \in \{<, >\} \end{aligned}$$

Repeating this procedure until the formula becomes unsatisfiable will lead to an assignment minimizing f under all models of \(\varphi \).

3 Planning for Autonomous Robots in Smart Factories

In this section we report our experience using OMT to solve planning problems optimally in the RCLL domain. After introducing the domain, we highlight some of the main challenges it presents. In doing so, we wish to distinguish between (i) challenges that appear in the RCLL irrespective of the approach used for planning and (ii) challenges that planning for the RCLL poses to OMT solvers. Finally, we briefly discuss the solution we proposed for OMT planning.

3.1 The RoboCup Logistics League

The RoboCup Logistics League provides a simplified smart factory scenario where two teams of three autonomous robots each compete to handle the logistics of materials to accommodate orders known only at run-time. Competitions take place yearly using a real robotic setup. However, for our experiments we made use of the simulated environment (Fig. 1) developed for the Planning and Execution Competition for Logistics Robots in SimulationFootnote 3 [24].

Fig. 1.
figure 1

Simulated RCLL factory environment [24].

Full size image

Products to be assembled have different complexities and usually require a base, mounting 0 to 3 rings, and a cap as a finishing touch. Bases are available in three different colors, four colors are admissible for rings and two for caps, leading to about 250 different possible combinations. Each order defines which colors are to be used, together with an ordering. An example of a possible configuration is shown in Fig. 2.

Several machines are scattered around the factory shop floor (random placement in each game, positions are announced to the robots). Each of them completes a particular production step such as providing bases, mounting colored rings or caps. There are four types of machines:

  • Base Station (BS): acts as dispenser of base elements (one per team).

  • Cap Station (CS): mounts a cap as the final step in production on an intermediate product. The CS stores at most one cap at a time (empty initially). To prefill the CS, a base element with a cap must be taken from a shelf in the arena and fed to the machine; the cap is then unmounted and buffered. The cap can then be mounted on the next intermediate product taken to the machine (two CS per team).

  • Ring Station (RS): mounts one colored ring (of specific color) onto an intermediate product. Some ring colors require additional tokens: robots will have to feed a RS with a specified number of bases before the required color can be mounted (two RS per team).

  • Delivery Station (DS): accepts finished products (one per team).

The objective for autonomous robots is then to transport intermediate products between processing machines and optimize a multistage production cycle of different product variants until delivery of final products.

Orders that denote the products which must be assembled are posted at run-time by an automated referee box and come with a delivery time window, introducing a temporal component that requires quick planning and scheduling.

Fig. 2.
figure 2

Example of order configuration for the competition [26, 30]. (Color figure online)

Full size image

3.2 RCLL Challenges for Task Planning

Task Planning with Time Windows. Production processes in the RCLL require reasoning over tasks that are subject to temporal constraints often expressed as time windows, e.g., delivery must happen between minutes 2 and 3. Time windows increase the complexity of the planning and scheduling problem as they require to reason on both temporal and spatial relations between robots (and tasks). Furthermore, one might even want to specify additional optimization requirements, such as, perform delivery taking the least time possible. The nature of these constraints introduces three strictly related subproblems [28], i.e., (i) find an assignment of tasks to robots that optimizes the given objective function, (ii) compute a feasible ordering of tasks that results in optimal assignments, and (iii) assign times to tasks in a way that optimizes the objective.

Domain Representation. The domain presented by the RCLL is a fairly complex one and efficient reasoning on it can be hard for model-based approaches. To get a feeling of this, consider the variety of product configurations that are allowed in the competition: about 250 configurations are possible! This can clearly represent a problem for state-based approaches, since models explicitly encoding all product variants can quickly become intractable.

Online Execution. Automated production processes like the one proposed by the RCLL are, by their own nature, highly dynamic and subject to unforeseeable changes. The latter are often due to, e.g., temporary robot/machine failures, changes in task definitions or online arrival of new tasks. As all these aspects are modeled in the RCLL, one can easily realize that the execution of plans represents an interesting challenge too. To cater for these aspects, the dynamics that occur during execution must be considered, making integrated approaches essential to maintain efficiency.

3.3 Specific Challenges for OMT Solvers

Combinatorial Optimization. Computing optimal task plans with OMT requires the solver to (i) search over a finite set of actions so as to (ii) optimize an objective function over the arithmetic domain. This means that, although the problem seems to require optimization in the arithmetic domain, it mostly requires efficient combinatorial optimization capabilities. However, solvers do not recognize this and invoke arithmetic optimization resulting in prohibiting runtimes.

Scalability. As the complexity of products required during a game in the RCLL increases, formula encodings can grow rapidly. If large encodings can already become inefficient to solve in SMT, this becomes even more critical in OMT. Abstractions are therefore needed to tame solving complexity, however, currently there are no procedures that can handle iterative abstraction refinement internally to the solver. Cimatti et al. started to address the problem in the context of SMT [7, 8], however no similar work exists for OMT.

3.4 Our Solution

In a recent series of papers [4, 19,20,21,22, 27] we proposed OMT as an approach to deliver task plans that can meet production requirements (optimally) and withstand deployment in the RCLL. While the approach described in those papers is specifically tailored for the RCLL, we expect that our solution can carry over to domains with similar structure and features, thus providing the basis for general, yet efficient, synthesis of optimal task plans based on OMT.

To generate optimal plans, we extended standard Planning as Satisfiability [16] to enable optimization over reward structures expressed in first-order arithmetic theories in OMT – see [19] for a brief overview of our approach. This idea was applied to solve multi-robot planning problems arising in the RCLL, such as factory shop-floor exploration [21] and planning for production [22].

To cater for the dynamics that occur when plans are executed on concrete systems, we also presented a system that integrates our planning approach into an online execution agent based on CLIPS [25], currently used by the RCLL world champion. A prototypical implementation of this system was presented in [27] and later extended in [22].

4 Further Challenges

Modern solvers achieve impressive performances in several domains and offer a powerful support for planning. Nevertheless, there are several challenges still to be addressed in order to ease the applicability of OMT in planning. In this section we discuss some of these challenges.

Parallelization. Practical efficiency is probably one of the main limitations of current OMT algorithms and tools. Beyond theoretical worst-case complexity results, research on SAT and SMT has shown that problem instances arising from application domains can be tackled successfully in many cases of interest. The research on OMT is currently less mature than its SMT counterpart, therefore improving on this aspect is still an open challenge. We believe that parallelization may offer an interesting path towards attaining practical efficiency in OMT. While parallel SAT solving has been the subject of research in the past [13], the development of parallel SMT solvers is still in its infancy [15], and, to the best of our knowledge, paradigms for parallel OMT have not been considered yet. Carrying over the results obtained in SAT to SMT/OMT is nontrivial, because the role of SAT solver inside SMT/OMT procedure is to enumerate assignments and not just to search a satisfying one. However, once enumeration of assignments can be successfully parallelized, at least to some extent, also checking their theory consistency and, possibly, finding optimal solutions, can be distributed on several processors. Besides modern multi-core architectures, parallelization could also take advantage of hybrid CPU-GPU architectures, where the GPU part can substantially speed up numerical computations as it happens in other AI fields like training of deep neural networks—see, e.g., [17].

Develop New Encodings. Our experiments with different encodings of planning problems into OMT indicate that considerable progress can be made by considering novel kinds of encodings and relaxations. Beyond computational concerns, new relaxations can be of great interest from a representational standpoint. One key challenge relates to finding encodings which generalize well to several problem domains. While the improvements that we obtained working on the RCLL domain are mostly specific and tailored to a specific scenario, some choices, e.g., state-based vs. action-based encoding, should be weighted across several domains to understand their effectiveness at large. Currently, to the extent of our knowledge, the proposal of OMT-based planning has been tried and tested successfully in our work only, whereas general-purpose SMT-based planners have been proposed already—see, e.g., [6]. In both cases, the main issue is to deal effectively with the combinatorial aspects of the domain which could force the SAT engine underlying the SMT/OMT solver to perform “brute-force search” in the space of possible assignments without a clue. In order to reduce this phenomenon, some domain knowledge must be incorporated in the encoding so as to allow the SAT solver to learn suitable propositional constrains by interacting with the theory solver. In addition to this, specialized SAT heuristics could be devised to minimize the chance of exploring parts of the propositional search space which are trivially unfruitful once the underlying theory is taken into account.

Accounting for Uncertainty. Planning for dynamic environments such as smart factories often requires to include some degree of uncertainty in the models used. While practically efficient techniques to reason about uncertain models have been proposed in task planning—see, e.g., Part V of [11]—and formal verification—see, e.g., [2]—the question remains how to encode uncertainty efficiently in SMT/OMT, or to extend existing decision procedures to incorporate uncertainty. The issue is nontrivial because many of the above mentioned probabilistic techniques and tools rely on state-based representations which quickly become intractable in realistic production logistics domains. A symbolic approach, wherein the specification of states and transitions is left implicit like in probabilistic programs, would be suitable for realistically-sized domains as well. SMT solvers have been successfully used both in planning and formal verification as engines in symbolic planners and model checkers, but this is not the case of OMT solvers and, to the best of our knowledge, there is no provision for optimization in current state-of-the-art tools.

Integrated Task and Motion Planning. Task planning tries to answer the question of what can be done to achieve a given objective. In the RCLL, this would correspond to, e.g., what actions do robots need to perform to deliver the requested product? However, as highlighted in Sect. 3, planning for robotics requires more than just saying what needs to be done. In such domains, planning needs to be integrated with other deliberation functions such as how to perform actions (and monitor their progress). In our previous work, we decoupled this problem by relying on an execution and monitoring agent external to the planning process. This however may lead to plan failures if, e.g., a robot tries to move toward a target location to perform a task but its kinematics does not allow such motion. A tighter integration between task constraints and motion constraints is needed in most relevant robotics applications where any planning is needed, and such need has been recognized for a long time—see, e.g., [29]. However, it was not until recent times that research in motion planning achieved efficient algorithms and tools—see, e.g., [18]—that can be combined over a wide spectrum of methods and implementations in task planning. Harvesting motion planning techniques and incorporating them into SMT/OMT based approaches requires matching, mostly discrete, specifications of task planning domains with the, mostly continuous, specification of motion planning constraints. A suitable semantic “bridge” must be found between the two sides, one that is akin to hybdrid systems models where discrete control modes are endowed with continuous dynamics.

Explainable Planning. The problem of generating explanations for decisions taken by autonomous systems is very pressing, with many initiative being launched to foster research in this field [1]. The need for explanations is even amplified when AI technologies are employed in safety-critical scenarios involving, e.g., the interplay of human and robotic workers. In [22] we started looking into this problem, as we believe OMT-based synthesis builds on techniques that have the potential to ease explaining, e.g., by generating unsat cores. However, presenting solver outputs in a human-readable way that could facilitate understanding of the underlying decision process remains an open challenge.

5 Conclusion

In this paper we briefly reported on our experiences using Optimization Modulo Theories to solve task planning problems in logistics. Given the broad nature of the topic, we focused our effort on problems stemming from the RoboCup Logistics League, a well-known benchmark in planning and robotics. Despite highly encouraging results, efforts are still needed to increase applicability and scalability of OMT technologies in planning. With this work we hope to increase the visibility of OMT techniques and tools in planning so as to intensify the developments in this relevant research area.