×

zbMATH — the first resource for mathematics

Using satisfiability for non-optimal temporal planning. (English) Zbl 1361.68205
Fariñas del Cerro, Luis (ed.) et al., Logics in artificial intelligence. 13th European conference, JELIA 2012, Toulouse, France, September 26–28, 2012. Proceeding. Berlin: Springer (ISBN 978-3-642-33352-1/pbk). Lecture Notes in Computer Science 7519. Lecture Notes in Artificial Intelligence, 176-188 (2012).
Summary: AI planning is one of the research fields that has benefited from employing satisfiability checking methods. These methods have been proved to be very effective in finding optimal plans for both classical and temporal planning. It is also known that by using planning-based heuristic information in solving SAT formulae, one can develop SAT-based planners that are competitive with state-of-the-art non-optimal planners in classical planning domains. However, using satisfiability for non-optimal temporal planning has not been investigated so far. The main difficulty in using satisfiability in temporal planning is the representation of time, which is a continuous concept. Previously introduced SAT-based temporal planners employed an explicit representation of time in the SAT formulation, which made the formulation too large for even very small problems. To overcome this problem, we introduce a novel method for converting temporal problems into a SAT encoding. We show how the size of the encoding can be reduced by abstracting out durations of planning actions. We also show that the new formulation is powerful enough to encode fully concurrent plans. We first use an off-the-shelf SAT solver to extract an abstract initial plan out of the new encoding. We then add the durations of actions to a relaxed version of the initial plan and verify the resulting temporally constrained plan by testing consistency of a certain related simple temporal problem (STP). In the case of an inconsistency, a negative cycle within the corresponding simple temporal network (STN) is detected and encoded into the SAT formulation to prevent the SAT solver from reproducing plans with similar cycles. This process is repeated until a valid temporal plan will be achieved. Our empirical results show that the new approach, while not using a planning-based heuristic function of any kind, is competitive with POPF, which is the state-of-the-art of expressively temporal heuristic planners.
For the entire collection see [Zbl 1246.68063].
MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Kautz, H., Selman, B.: Planning as Satisfiability. In: Proceedings of 10th European Conference on Artificial Intelligence, pp. 359–363. IOS Press (1992)
[2] Blum, A., Furst, M.: Fast Planning Through Planning Graph Analysis. Artificial Intelligence 90(1-2), 281–300 (1997) · Zbl 1017.68533
[3] Kautz, H., Selman, B.: Unifying SAT-based and Graph-based Planning. In: Proceedings of 16th International Joint Conference on Artificial Intelligence, pp. 318–325. AAAI Press (1999)
[4] Robinson, N., Gretton, C., Pham, D.N., Sattar, A.: SAT-Based Parallel Planning Using a Split Representation of Actions. In: Proceedings of 19th International Conference on Automated Planning and Scheduling. AAAI Press (2009)
[5] Rintanen, J., Heljanko, K., Niemelä, I.: Parallel Encodings of Classical Planning as Satisfiability. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol. 3229, pp. 307–319. Springer, Heidelberg (2004) · Zbl 1111.68660
[6] Rintanen, J.: Planning with Specialized SAT Solvers. In: Proceedings of 25th AAAI Conference on Artificial Intelligence. AAAI Press (2011)
[7] Younes, H.L.S., Simmons, R.G.: VHPOP: Versatile Heuristic Partial Order Planner. Journal of Artificial Intelligence Research 20, 405–430 (2003) · Zbl 1036.68107
[8] Vidal, V., Geffner, H.: Branching and pruning: An optimal temporal POCL planner based on constraint programming. Artificial Intelligence 170(3), 298–335 (2006) · Zbl 1131.68528
[9] Smith, D.E., Weld, D.S.: Temporal planning with mutual exclusion reasoning. In: Proceedings of 16th International Joint Conference on Artificial Intelligence, pp. 326–337. AAAI Press (1999)
[10] Garrido, A., Fox, M., Long, D.: A temporal planning system for durative actions of PDDL2.1. In: Proceedings of 15th European Conference on Artificial Intelligence, pp. 586–590. IOS Press (2002)
[11] Gerevini, A., Serina, I.: LPG: a Planner based on Local Search for Planning Graphs. In: Proceedings of 6th International Conference on Artificial Intelligence Planning Systems, pp. 13–22. AAAI Press (2002)
[12] Eyerich, P., Mattmuller, R., Roger, G.: Unifying Context-Enhanced Additive Heuristic for Temporal and Numeric Planning. In: Proceedings of 19th International Conference on Automated Planning and Scheduling. AAAI Press (2009)
[13] Huang, R., Chen, Y., Zhang, W.: An optimal temporally expressive planner: Initial results and application to P2P network optimization. In: Proceedings of 19th International Conference on Automated Planning and Scheduling. AAAI Press (2009)
[14] Mali, A.D., Liu, Y.: T-SATPLAN: A SAT-based Temporal Planner. International Journal of Artificial Intelligence Tools 15(5), 779–802 (2006) · Zbl 05421518
[15] Cushing, W., Kambhampati, S., Weld, D.S.: When is temporal planning really temporal? In: Proceedings of 20th International Joint Conference on Artificial Intelligence, pp. 1852–1859. AAAI Press (2007)
[16] Halsey, K., Long, D., Fox, M.: Managing Concurrency in Planning Using Planner-Scheduler interaction. Artificial Intelligence 173(1), 1–44 (2009) · Zbl 1180.68245
[17] Coles, A.J., Coles, A., Fox, M., Long, D.: Forward-Chaining Partial-Order Planning. In: Proceedings of 20th International Conference on Automated Planning and Scheduling, pp. 42–49. AAAI Press (2010)
[18] Hoffmann, J., Nebel, B.: The FF Planning System: Fast Plan Generation Through Heuristic Search. Journal of Artificial Intelligence Research 14, 253–302 (2001) · Zbl 0970.68044
[19] Dechter, R., Meiri, I., Pearl, J.: Temporal Constraint Networks. Artificial Intelligence 49(1-3), 61–95 (1991) · Zbl 0737.68070
[20] Fox, M., Long, D.: PDDL2.1: An Extension to PDDL for Expressing Temporal Planning Domains. Journal of Artificial Intelligence Research 20, 61–124 (2003) · Zbl 1036.68093
[21] Kautz, H., Selman, B., Hoffmann, J.: SatPlan: Planning as Satisfiability. IPC (2006)
[22] Eén, N., Sörensson, N.: An Extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502–518. Springer, Heidelberg (2004) · Zbl 1204.68191
[23] Strathclyde Planning Group, http://planning.cis.strath.ac.uk
[24] Coles, A., Coles, A., Olaya, A.G., Jiménez, S., López, C.L., Sanner, S., Yoon, S.: A Survey of the Seventh International Planning Competition. AI Magazine 33(1) (2012)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.