Abstract
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Kautz, H., Selman, B.: Planning as Satisfiability. In: Proceedings of 10th European Conference on Artificial Intelligence, pp. 359–363. IOS Press (1992)
Blum, A., Furst, M.: Fast Planning Through Planning Graph Analysis. Artificial Intelligence 90(1-2), 281–300 (1997)
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)
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)
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)
Rintanen, J.: Planning with Specialized SAT Solvers. In: Proceedings of 25th AAAI Conference on Artificial Intelligence. AAAI Press (2011)
Younes, H.L.S., Simmons, R.G.: VHPOP: Versatile Heuristic Partial Order Planner. Journal of Artificial Intelligence Research 20, 405–430 (2003)
Vidal, V., Geffner, H.: Branching and pruning: An optimal temporal POCL planner based on constraint programming. Artificial Intelligence 170(3), 298–335 (2006)
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)
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)
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)
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)
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)
Mali, A.D., Liu, Y.: T-SATPLAN: A SAT-based Temporal Planner. International Journal of Artificial Intelligence Tools 15(5), 779–802 (2006)
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)
Halsey, K., Long, D., Fox, M.: Managing Concurrency in Planning Using Planner-Scheduler interaction. Artificial Intelligence 173(1), 1–44 (2009)
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)
Hoffmann, J., Nebel, B.: The FF Planning System: Fast Plan Generation Through Heuristic Search. Journal of Artificial Intelligence Research 14, 253–302 (2001)
Dechter, R., Meiri, I., Pearl, J.: Temporal Constraint Networks. Artificial Intelligence 49(1-3), 61–95 (1991)
Fox, M., Long, D.: PDDL2.1: An Extension to PDDL for Expressing Temporal Planning Domains. Journal of Artificial Intelligence Research 20, 61–124 (2003)
Kautz, H., Selman, B., Hoffmann, J.: SatPlan: Planning as Satisfiability. IPC (2006)
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)
Strathclyde Planning Group, http://planning.cis.strath.ac.uk
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rankooh, M.F., Mahjoob, A., Ghassem-Sani, G. (2012). Using Satisfiability for Non-optimal Temporal Planning. In: del Cerro, L.F., Herzig, A., Mengin, J. (eds) Logics in Artificial Intelligence. JELIA 2012. Lecture Notes in Computer Science(), vol 7519. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33353-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-642-33353-8_14
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33352-1
Online ISBN: 978-3-642-33353-8
eBook Packages: Computer ScienceComputer Science (R0)