In this paper we focus on Planning as Satisfiability (SAT). We build from the simple consideration that the values of fluents at a certain time point derive deterministically from the initial situation and the sequence of actions performed till that point. Thus, the choice of actions to perform is the only source of nondeterminism. This is a rather trivial considerations, but which has important positive consequences if implemented in current planners via SAT. In fact, it produces a dramatic size reduction of the space of the truth assignments searched in by the SAT decider used to solve the final SAT problem. To justify this claim, we repeat many of the experiments reported in (Erns, Millstein, & Weld 1997), and show that the CPU time requested to solve a problem can go down up to 4 orders of magnitude
Act, and the Rest Will Follow: Exploiting Determinism in Planning as Satisfiability
Sebastiani, Roberto
1998-01-01
Abstract
In this paper we focus on Planning as Satisfiability (SAT). We build from the simple consideration that the values of fluents at a certain time point derive deterministically from the initial situation and the sequence of actions performed till that point. Thus, the choice of actions to perform is the only source of nondeterminism. This is a rather trivial considerations, but which has important positive consequences if implemented in current planners via SAT. In fact, it produces a dramatic size reduction of the space of the truth assignments searched in by the SAT decider used to solve the final SAT problem. To justify this claim, we repeat many of the experiments reported in (Erns, Millstein, & Weld 1997), and show that the CPU time requested to solve a problem can go down up to 4 orders of magnitudeI documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
