Planning as satisfiability is a very efficient technique for classical planning, i.e., for planning domains in which both the effects of actions and the initial state are completely specified. In this paper we present C-SAT , a SAT-based procedure capable of dealing with planning domains having incomplete information about the initial state, and whose underlying transition system is specified using the highly expressive action language C. Thus, C-SAT allows for planning in domains involving (i) actions which can be executed concurrently; (ii) (ramification and qualification) constraints affecting the effects of actions; and (iii) nondeterminism in the initial state and in the effects of actions. We first prove the correctness and the completeness of C-SAT , discuss some optimizations, and then we present C-PLAN, a system based on C-SAT . C-PLAN works on any C planning problem, but some optimizations have not been fully implemented yet. Nevertheless, the experimental analysis shows that SAT-based approaches to planning with incomplete information are viable, at least in the case of problems with a high degree of parallelism.

SAT-based planning in complex domains: Concurrency, constraints and nondeterminism

GIUNCHIGLIA, ENRICO;TACCHELLA, ARMANDO
2003-01-01

Abstract

Planning as satisfiability is a very efficient technique for classical planning, i.e., for planning domains in which both the effects of actions and the initial state are completely specified. In this paper we present C-SAT , a SAT-based procedure capable of dealing with planning domains having incomplete information about the initial state, and whose underlying transition system is specified using the highly expressive action language C. Thus, C-SAT allows for planning in domains involving (i) actions which can be executed concurrently; (ii) (ramification and qualification) constraints affecting the effects of actions; and (iii) nondeterminism in the initial state and in the effects of actions. We first prove the correctness and the completeness of C-SAT , discuss some optimizations, and then we present C-PLAN, a system based on C-SAT . C-PLAN works on any C planning problem, but some optimizations have not been fully implemented yet. Nevertheless, the experimental analysis shows that SAT-based approaches to planning with incomplete information are viable, at least in the case of problems with a high degree of parallelism.
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11567/250514
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 58
  • ???jsp.display-item.citation.isi??? 48
social impact