Abstract
Task planning is a well-studied problem for which interesting applications exist in production logistics. Planning for such domains requires to take into account not only feasible plans, but also optimality targets, e.g., minimize time, costs or energy consumption. Although there exist several algorithms to compute optimal solutions with formal guarantees, heuristic approaches are typically preferred in practical applications, trading certified solutions for a reduced computational cost. Reverting this trend represents a standing challenge within the domain of task planning at large. In this paper we discuss our experience using Optimization Modulo Theories to synthesize optimal plans for multi-robot teams handling production processes within the RoboCup Logistics League. Besides presenting our results, we discuss challenges and possible directions for future development of OMT planning.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
- 2.
For instance, if f and \(\varphi _S\) are expressed in QF_LRA, this can be done with Simplex.
- 3.
References
EXplainable AI Planning (2018). http://icaps18.icaps-conference.org/xaip/
Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)
Bensalem, S., Havelund, K., Orlandini, A.: Verification and validation meet planning and scheduling. STTT 16(1), 1–12 (2014)
Bit-Monnot, A., Leofante, F., Pulina, L., Ábrahám, E., Tacchella, A.: SMarTplan: a task planner for smart factories. CoRR abs/1806.07135 (2018)
Bjørner, N., Phan, A.-D., Fleckenstein, L.: \(\nu \)z - An optimizing SMT solver. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 194–199. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46681-0_14
Cashmore, M., Fox, M., Long, D., Magazzeni, D.: A compilation of the full PDDL+ language into SMT. In: Proceedings of ICAPS 2016, pp. 79–87 (2016)
Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Invariant checking of NRA transition systems via incremental reduction to LRA with EUF. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 58–75. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54577-5_4
Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Satisfiability modulo transcendental functions via incremental linearization. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 95–113. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63046-5_7
Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The mathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93–107. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_7
Corzilius, F., Kremer, G., Junges, S., Schupp, S., Ábrahám, E.: SMT-RAT: an open source C++ toolbox for strategic and parallel SMT solving. In: Heule, M., Weaver, S. (eds.) SAT 2015. LNCS, vol. 9340, pp. 360–368. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24318-4_26
Ghallab, M., Nau, D.S., Traverso, P.: Automated Planning and Acting. Cambridge University Press, Cambridge (2016)
Gini, M.L.: Multi-robot allocation of tasks with temporal and ordering constraints. In: Proceedings of AAAI 2018, pp. 4863–4869 (2017)
Hamadi, Y., Wintersteiger, C.M.: Seven challenges in parallel SAT solving. AI Mag. 34(2), 99–106 (2013)
Hofmann, T., Niemueller, T., Claßen, J., Lakemeyer, G.: Continual planning in Golog. In: Proceeding of AAAI 2016, pp. 3346–3353 (2016)
Hyvärinen, A.E.J., Wintersteiger, C.M.: Parallel satisfiability modulo theories. In: Hamadi, Y., Sais, L. (eds.) Handbook of Parallel Constraint Reasoning, pp. 141–178. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-63516-3_5
Kautz, H.A., Selman, B.: Planning as satisfiability. In: ECAI, pp. 359–363 (1992)
Krizhevsky, A., Sutskever, I., Hinton, G.E.: Imagenet classification with deep convolutional neural networks. In: Proceedings of NIPS 2012, pp. 1097–1105 (2012)
LaValle, S.M.: Planning Algorithms. Cambridge University Press, Cambridge (2006)
Leofante, F.: Guaranteed plans for multi-robot systems via optimization modulo theories. In: Proceedings of AAAI 2018 (2018)
Leofante, F.: Optimal multi-robot task planning: from synthesis to execution (and back). In: Proceeding of IJCAI 2018 (2018, to appear)
Leofante, F., Ábrahám, E., Niemueller, T., Lakemeyer, G., Tacchella, A.: On the synthesis of guaranteed-quality plans for robot fleets in logistics scenarios via optimization modulo theories. In: Proceedings of IRI 2017, pp. 403–410 (2017)
Leofante, F., Ábrahám, E., Niemueller, T., Lakemeyer, G., Tacchella, A.: Integrated Synthesis and Execution of Optimal Plans for Multi-Robot Systems in Logistics. Information Systems Frontiers, pp. 1–21. Springer, New York (2018). https://doi.org/10.1007/s10796-018-9858-3
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Niemueller, T., Karpas, E., Vaquero, T., Timmons, E.: Planning competition for logistics robots in simulation. In: Proceeding of PlanRob@ICAPS 2016 (2016)
Niemueller, T., Lakemeyer, G., Ferrein, A.: Incremental task-level reasoning in a competitive factory automation scenario. In: AAAI Spring Symposium - Designing Intelligent Robots: Reintegrating AI (2013)
Niemueller, T., Lakemeyer, G., Ferrein, A.: The RoboCup Logistics League as a benchmark for planning in robotics. In: Proceeding of PlanRob@ICAPS 2015 (2015)
Niemueller, T., Lakemeyer, G., Leofante, F., Ábrahám, E.: Towards CLIPS-based task execution and monitoring with SMT-based decision optimization. In: Proceedings of PlanRob@ICAPS 2017 (2017)
Nunes, E., Manner, M.D., Mitiche, H., Gini, M.L.: A taxonomy for task allocation problems with temporal and ordering constraints. Robot. Auton. Syst. 90, 55–70 (2017)
Popplestone, R., Ambler, A., Bellos, I.: RAPT: a language for describing assemblies. Ind. Robot Int. J. 5(3), 131–137 (1978)
RCLL Technical Committee: RoboCup Logistics League – Rules and regulations 2017 (2017)
Sebastiani, R., Tomasi, S.: Optimization modulo theories with linear rational costs. ACM Trans. Comput. Log. 16(2), 12:1–12:43 (2015)
Sebastiani, R., Trentin, P.: OptiMathSAT: a tool for optimization modulo theories. In: Proceedings of CAV 2015, pp. 447–454 (2015)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Leofante, F., Ábrahám, E., Tacchella, A. (2018). Task Planning with OMT: An Application to Production Logistics. In: Furia, C., Winter, K. (eds) Integrated Formal Methods. IFM 2018. Lecture Notes in Computer Science(), vol 11023. Springer, Cham. https://doi.org/10.1007/978-3-319-98938-9_18
Download citation
DOI: https://doi.org/10.1007/978-3-319-98938-9_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-98937-2
Online ISBN: 978-3-319-98938-9
eBook Packages: Computer ScienceComputer Science (R0)