Processes and continuous change in a SAT-based planner. (English) Zbl 1132.68711

Summary: The TM-LPSAT planner can construct plans in domains containing atomic actions and durative actions; events and processes; discrete, real-valued, and interval-valued fluents; reusable resources, both numeric and interval-valued; and continuous linear change to quantities. It works in three stages. In the first stage, a representation of the domain and problem in an extended version of PDDL+ is compiled into a system of Boolean combinations of propositional atoms and linear constraints over numeric variables. In the second stage, a SAT-based arithmetic constraint solver, such as LPSAT or MathSAT, is used to find a solution to the system of constraints. In the third stage, a correct plan is extracted from this solution. We discuss the structure of the planner and show how planning with time and metric quantities is compiled into a system of constraints. The proofs of soundness and completeness over a substantial subset of our extended version of PDDL+ are presented.


68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Full Text: DOI


[1] Armando, A.; Castellini, C.; Giunchiglia, E.; Giunchiglia, F.; Tacchella, A., SAT-based decision procedures for automated reasoning: A unifying perspective, () · Zbl 1098.68693
[2] Allen, J.F., Maintaining knowledge about temporal intervals, Comm. ACM, 26, 11, 832-843, (1983) · Zbl 0519.68079
[3] Audemard, G.; Bertoli, P.; Cimatti, A.; Kornilowicz, R.; Sebastiani, R., A SAT based approach for solving formulas over Boolean and linear mathematical propositions, (), 193-208
[4] Audemard, G.; Bozzano, M.; Cimatti, A.; Sebastiani, R., Verifying industrial hybrid systems with mathsat, Electronic notes theoret. comput. sci., 89, 4, (2004) · Zbl 1272.68220
[5] Barrett, C.; Berezin, S., CVC lite: A new implementation of the cooperating validity checker, (), 515-518 · Zbl 1103.68605
[6] Bayardo, R.; Schrag, R., Using CSP look-back techniques to solve real-world SAT instances, (), 203-208
[7] Blum, A.; Furst, M., Fast planning through planning graph analysis, Artificial intelligence, 90, 281-300, (1997) · Zbl 1017.68533
[8] A. Borning, G. Badros, The cassowary linear arithmetic constraint solving algorithm: Interface and implementation, Technical Report UW-CSE-98-06-04, University of Washington, WA, 1998
[9] M. Bozzano, R. Bruttomesso, A. Cimatti, T. Junttila, P. Rossum, S. Schults, R. Sebastiani, MATHSAT: Tight integration of SAT and mathematical decision procedures, J. Automat. Reason. (Special Issue on SAT) (2005) · Zbl 1109.68101
[10] Brafman, R., A simplifier for propositional formulas with many binary clauses, (), 515-522
[11] Chapman, D., Planning for conjunctive goals, Artificial intelligence, 32, 3, 333-377, (1987) · Zbl 0642.68171
[12] Davis, E., Representations of common sense knowledge, (1990), Morgan Kaufmann San Fransisco, CA
[13] Davis, E., Axiomatizing qualitative process theory, (), 177-188
[14] Davis, M.; Logemann, G.; Loveland, D., A machine program for theorem proving, Comm. ACM, 5, 394-397, (1962) · Zbl 0217.54002
[15] Dean, T.; Firby, J.; Miller, D., Hierarchical planning involving deadlines, travel times and resources, Comput. intelligence, 4, 4, 381-398, (1988)
[16] Dimopoulos, Y.; Gerevini, A., Temporal planning through mixed integer programming: A preliminary report, (), 47-62
[17] Do, M.B.; Kambhampati, S., Sapa: A scalable multi-objective metric temporal planner, J. artificial intelligence res., 20, 155-194, (2003) · Zbl 1036.68091
[18] Drabble, B., EXCALIBUR: A program for planning and reasoning with processes, Artificial intelligence, 62, 1-40, (1993)
[19] Edelkamp, S.; Hoffman, J., PDDL2.2: the languages for the classical part of the 4th international planning competition, 2004
[20] Een, N.; Sorensson, N., An extensible SAT-solver, (), 502-518 · Zbl 1204.68191
[21] Ernst, M.; Millstein, T.; Weld, D., Automatic SAT-compilation of planning problems, (), 1169-1176
[22] Forbus, K., Qualitative process theory, Artificial intelligence, 24, 85-168, (1984)
[23] Fox, M.; Long, D., The automatic inference of state invariants in TIM, J. artificial intelligence res., 9, 367-421, (1998) · Zbl 0910.68199
[24] Fox, M.; Long, D., PDDL+ level 5: an extension to PDDL2.1 for modelling planning domains continuous time-dependent effects, 2001
[25] Fox, M.; Long, D., PDDL2.1: an extension to PDDL for expressing temporal planning domains, J. artificial intelligence res., 20, 61-124, (2003) · Zbl 1036.68093
[26] Gerevini, A.; Schubert, L., Inferring state constraints for domain independent planning, (), 905-912
[27] Gerevini, A.; Saetti, A.; Serina, I., Planning through stochastic local search and temporal action, J. artificial intelligence res., 20, 239-290, (2003) · Zbl 1058.68103
[28] Giunchiglia, E.; Massarotto, A.; Sebastiani, R., Act and the rest will follow: exploiting determinism in planning as satisfiability, (), 948-953
[29] Hendrix, G., Modeling simultaneous actions and continuous changes, Artificial intelligence, 4, 145-180, (1973)
[30] Henzinger, T., The theory of hybrid automata, (), 278-292 · Zbl 0959.68073
[31] Hooker, J., Logic-based methods for optimization, (2000), Wiley New York · Zbl 0974.90001
[32] Kautz, H.; Selman, B., Planning as satisfiability, (), 359-363
[33] Kautz, H.; McAllester, D.; Selman, B., Encoding plans in propositional logic, (), 374-384
[34] Kautz, H.; Selman, B., Pushing the envelope: planning, propositional logic and stochastic search, (), 1194-1201
[35] Kautz, H.; Selman, B., Unifying SAT-based and graph-based planning, (), 318-325
[36] Kichkaylo, K.; Ivan, A.; Karamcheti, V., Constrained component deployment in wide-area networks using AI planning techniques, (), 3-8
[37] Long, D.; Fox, M.; Sebastia, I.; Coddington, A., An examination of resources in planning, ()
[38] Long, D.; Fox, M., Exploiting a graphplan framework in temporal planning, (), 51-62
[39] Long, D.; Fox, M., The 3rd international planning competition: results and analysis, J. artificial intelligence res., 20, 1-59, (2003) · Zbl 1036.68097
[40] Mali, A., Encoding temporal planning as CSP, (), 75-92
[41] McDermott, D., The AIPS-98 planning competition committee, PDDL—the planning domain definition language, version 1.2, 1998
[42] McDermott, D., The formal semantics of processes in PDDL, ()
[43] McDermott, D., Reasoning about autonomous processes in an estimated-regression planner, (), 143-152
[44] J. Penberthy, Planning with continuous change, Ph.D. Dissertation, Department of Computer Science and Engineering, University of Washington, WA, USA, 1993
[45] Penberthy, J.; Weld, D., Temporal planning with continuous change, (), 1010-1015
[46] J. Shin, TM-LPSAT: Encoding temporal metric planning in continuous time, Ph.D. Dissertation, Department of Computer Science, New York University, NY, USA, 2004
[47] Shin, J.; Davis, E., Continuous time in a SAT-based planner, (), 531-536
[48] R. Simmons, Combining associational and causal reasoning to solve interpretation and planning problems, Technical Report AI-TR-1048, MIT AI Lab, MA, USA, 1988
[49] Smith, D.; Frank, J.; Jonsson, A., Bridging the gap between planning and scheduling, Knowledge engrg. rev., 15, 1, 61-94, (2000)
[50] Smith, D.; Weld, D., Temporal planning with mutual exclusion reasoning, (), 326-333
[51] Vere, S., Planning in time: windows and durations for activities and goals, Pattern anal. machine intelligence, 5, 246-267, (1983)
[52] Wilkins, D., Can AI planners solve practical problems?, Comput. intelligence, 6, 4, 232-246, (1990)
[53] Wolfman, S.; Weld, D., The LPSAT engine and its application to resource planning, (), 310-316
[54] Wolfman, S.; Weld, D., Combining linear programming and satisfiability solving for resource planning, Knowledge engrg. rev., 16, 1, 85-99, (2000) · Zbl 1060.91510
[55] Zhang, L.; Malik, S., The quest for efficient Boolean satisfiability solvers, (), 17-36 · Zbl 1010.68530
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.