Planning as satisfiability: a non-clausal approach

• Razer Montaño UFPR
• Fabiano Silva UFPR
• Marcos Castilho UFPR
• Luis Künzle UFPR

Abstract

The proposed approach consists in resolve a planning problem as reachability in Petri nets. Initially, the problem is translated in an acyclic Petri net. A non-clausal SAT formula is obtained from mutex among actions, explicited in the net structure. The SAT formula resolution is made with Tableaux KE and corresponds to decide all mutex in the net. Finally, to resolve reachability in this acyclic conflict-free Petri net is polinomial.

References

D’Agostino, M. and Mondadori, M. (1994). The taming of the cut: Classical refutations with analytic cut. Journal of Logic and Computation, 4(3):285–319.

Darwiche, A. (1998). Model-based diagnosis using structured system descriptions. Journal of Artificial Intelligence Research, 8:165–222.

Darwiche, A. and Marquis, P. (2002). A Knowledge Compilation Map. Journal of Artificial Intelligence Research, 17:229–264.

Esparza, J. (1996). Decidability and complexity of petri net problems an introduction. In Petri Nets, pages 374–428.

Kautz, H. and Selman, B. (1999). Unifying SAT-based and graph-based planning. In Minker, J., editor, Workshop on Logic-Based Artificial Intelligence, Washington, DC, June 14–16, 1999, College Park, Maryland. Computer Science Department, University of Maryland.

Massacci, F. (1998). Simplification: A general constraint propagation technique for propositional and modal tableaux. Lecture Notes in Computer Science, 1397:217–231.

Montaño, R. (2006). Aplicação de Fórmulas Não-Clausais em Planejamento com Redes de Petri. Master’s thesis, Universidade Federal do Paraná, Curitiba PR, Brasil.

Murata, T. (1989). Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580.

Palacios, H., Bonet, B., Darwiche, A., and Geffner, H. (2005). Pruning conformant plans by counting models on compiled d-DNNF representations. In ICAPS, pages 141–150.

R. Hähnle and N. Murray and E. Rosenthal (2005). Normal forms for knowledge compilation. Lecture Notes in Computer Science, 3488:304–313.

Silva, F., Castilho, M., and Künzle, L. (2000). Petriplan: a new algorithm for plan generation (preliminary report). In Lecture Notes in Artificial Intelligence, volume 1952, pages 86–95. International Joint Conference IBERAMIA’2000 SBIA’2000.