### Technical Report No. 216 - Abstract

**Jussi Rintanen, Keijo Heljanko, Ilkka Niemela**

*Planning as satisfiability: parallel plans and algorithms for plan search*

We address two aspects of constructing
plans efficiently by means of satisfiability
testing: efficient encoding of the problem
of existence of plans of a given number *t*
of time points in the propositional logic,
and strategies for finding plans given the
formulae representing these formulae for
different values of *t*.
For the first problem we consider a number
of semantics for plans with parallel
operator application. The standard semantics
used most often in earlier work require
that parallel operators are independent
and can therefore be executed in any order.
We consider a more relaxed definition of
parallel plans, first proposed by
Dimopoulos et al., as well as normal
forms for parallel plans that require
every operator to be executed as early
as possible.
We formalize the semantics of parallel
plans emerging in this setting, and
present translations of these semantics
into the propositional logic. The sizes
of the translations are asymptotically
optimal.
For the second problem we consider
strategies based on testing
the satisfiability of several formulae
representing plans of n time steps for
several values of *n* concurrently by
several processes. We show that big
efficiency gains can be obtained in
comparison to the standard strategy
of sequentially testing the satisfiability
of formulae for an increasing number of
time steps.

Report No. 216 (PostScript)