×

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.

MSC:

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

References:

[1] Armando, A.; Castellini, C.; Giunchiglia, E.; Giunchiglia, F.; Tacchella, A., SAT-based decision procedures for automated reasoning: A unifying perspective, (Lecture Notes in Computer Science, vol. 2605 (2003)) · 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, (Proceedings of the International Conference of Automated Deduction. Proceedings of the International Conference of Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 2392 (2002)), 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, (Proceedings of the International Conference on Computer Aided Verification (CAV-04) (2004)), 515-518 · Zbl 1103.68605
[6] Bayardo, R.; Schrag, R., Using CSP Look-back techniques to solve real-world SAT instances, (Proceedings of the 14th National Conference on Artificial Intelligence (AAAI-97), Providence, RI (1997)), 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; 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); 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, (Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI-01), Seattle, WA (2001)), 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: Morgan Kaufmann San Fransisco, CA
[13] Davis, E., Axiomatizing qualitative process theory, (Proceedings of the 3rd International Conference on Principles of Knowledge Representation and Reasoning (KR-92) (1992)), 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, (Proceedings of the 8th Conference on Principle and Practice on Constraint Programming (CP-02) (2002)), 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, (Proceedings of Conference on Theory and Applications of Satisfiability Testing (SAT-03) (2003)), 502-518 · Zbl 1204.68191
[21] Ernst, M.; Millstein, T.; Weld, D., Automatic SAT-compilation of planning problems, (Proceedings of the 15th International Joint Conference on Artificial Intelligence (IJCAI-97), Nagoya, Japan (1997)), 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, (Proceedings of the 15th National Conference of Artificial Intelligence (AAAI-98), St. Paul, MN (1998)), 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, (Proceedings of the 15th National Conference on Artificial Intelligence (AAAI-98), St. Paul, MN (1998)), 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, (Proceedings of the 11th Annual Symposium on Logic in Computer Science (1996)), 278-292 · Zbl 0959.68073
[31] Hooker, J., Logic-Based Methods for Optimization (2000), Wiley: Wiley New York · Zbl 0974.90001
[32] Kautz, H.; Selman, B., Planning as satisfiability, (Proceedings of the 10th European Conference on Artificial Intelligence (ECAI-92) (1992)), 359-363
[33] Kautz, H.; McAllester, D.; Selman, B., Encoding plans in propositional logic, (Proceedings of the 5th International Conference on Principles of Knowledge Representation and Reasoning (KR-96) (1996)), 374-384
[34] Kautz, H.; Selman, B., Pushing the envelope: Planning, propositional logic and stochastic search, (Proceedings of the 13th National Conference on Artificial Intelligence (AAAI-96), Portland, OR (1996)), 1194-1201
[35] Kautz, H.; Selman, B., Unifying SAT-based and graph-based planning, (Proceedings of the 17th International Joint Conference on Artificial Intelligence (IJCAI-99), Stockholm, Sweden (1999)), 318-325
[36] Kichkaylo, K.; Ivan, A.; Karamcheti, V., Constrained component deployment in wide-area networks using AI planning techniques, (Proceedings of the International Parallel and Distributed Symposium (IPDPS-03) (2003)), 3-8
[37] Long, D.; Fox, M.; Sebastia, I.; Coddington, A., An examination of resources in planning, (Proceedings of UK Planning and Scheduling SIG Workshop (2000))
[38] Long, D.; Fox, M., Exploiting a Graphplan framework in temporal planning, (Proceedings of International Conference on Automated Planning and Scheduling (ICAPS-03) (2003)), 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, (Proceedings of IEEE International Conference on Tools with Artificial Intelligence (2002)), 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, (Proceedings of Workshop on PDDL at International Conference on Automated Planning Scheduling (2003))
[43] McDermott, D., Reasoning about autonomous processes in an estimated-regression planner, (Proceedings of the International Conference on Automated Planning and Scheduling (ICAPS-03) (2003)), 143-152
[44] J. Penberthy, Planning with continuous change, Ph.D. Dissertation, Department of Computer Science and Engineering, University of Washington, WA, USA, 1993; 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, (Proceedings of the 12th National Conference on Artificial Intelligence (AAAI-94), Seattle, WA (1994)), 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; 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, (Proceedings of the 22th National Conference on Artificial Intelligence (AAAI-04), San Jase, CA (2004)), 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; 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, (Proceedings of the 16th International Joint Conference of Artificial Intelligence (IJCAI-99), Stockholm, Sweden (1999)), 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, (Proceedings of the 16th International Joint Conference of Artificial Intelligence (IJCAI-99), Stockholm, Sweden (1999)), 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, (Proceedings of the International Conference on Computer Aided Verification (CAV-02) (2002)), 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.