The Preconditions of ADL Actions

The preconditions of STRIPS actions consist of one structural feature - an `and' clause, allowing conjunctive preconditions and predicates with constant or parameterised bindings. ADL actions have a far greater range of structural features in their preconditions. They allow `or', `imply', `not', `forall' and `exists', which can be combined in any well-formed manner. In Marvin, the ADL preconditions are processed using two steps. First, all quantified preconditions are fully enumerated. Second, the resulting precondition formula is translated into Negation Normal Form (NNF) using the standard procedure: by replacing $(a \Rightarrow b)$ with $(\lnot a \lor b)$, and using De Morgan's laws to eliminate negations of clauses. Further reductions are then applied to eliminate redundancy, such as replacing (and A (and B C)) with (and A B C), and (or A (or B C)) with (or A B C).

Internally, within Marvin, the NNF precondition formula forms the basis of a `satisfaction tree', the nodes of which are the `and' and `or' elements of formula and the literals (negated and non-negated) form the leaves. The structure of the satisfaction tree for a given action schema is fixed, although the propositions at the leaves vary between groundings.

To determine which ground ADL action instances are applicable in a given state based on their preconditions, the algorithm shown by the pseudo-code fragment in Figure 6 is used. Initially, the satisfaction counters associated with each ground action's satisfaction tree nodes are reset using the following rules:

• Each `and' nodes has its counter set to denote the number of children it has.
• Each `or' node has its counter set to 1.
• Negative preconditions are assumed to be true, and the satisfaction counters of their parents decremented accordingly.

As these values are state-independent, for reasons of efficiency the values used to reset the satisfaction counters are computed once and cached for later use.

Having reset the satisfaction counters, each proposition in the current state is considered, and the satisfaction trees updated accordingly:

• The satisfaction counters of parent nodes that have the current proposition as a negative precondition are incremented.
• The satisfaction counters of parent nodes that have the current proposition as a positive precondition are decremented.

Then, by propagating the effects of truth value changes upwards through the tree, any action whose root node has sufficiently many children satisfied is applicable.

Figure 6: Pseudo-code for action applicability testing