= Solution
Use balls $a,b$, buckets $1,2$, transition index $k$ and the grounded <action schemas> from (a). Under a sequential encoding, one example <successor-state axiom> is
$$
\boxed{\operatorname{In}(a,1)_{k+1}\leftrightarrow
\operatorname{Drop}(a,1)_k\lor
\bigl(\operatorname{In}(a,1)_k\land\neg\operatorname{Pick}(a,1)_k\bigr).}
$$
Ball $a$ is in bucket $1$ afterwards exactly when it is dropped there now, or it was there and is not picked up. Actions involving other balls or arm movement leave this fact unchanged. This is both an effect rule and a persistence rule, rather than an implication that permits spontaneous appearances.
An example <action precondition axiom> is
$$
\boxed{\operatorname{Pick}(a,1)_k\to
\operatorname{In}(a,1)_k\land\operatorname{At}(1)_k\land\operatorname{Empty}_k.}
$$
A selected pick action must have the ball, arm and empty hand in the appropriate current state. The static type conditions have already been satisfied by <action grounding>.
An example <action exclusion axiom> is
$$
\boxed{\neg\bigl(\operatorname{Pick}(a,1)_k\land\operatorname{Pick}(b,1)_k\bigr).}
$$
The single arm cannot pick up both balls in one step. For a serial encoding include such an exclusion for every pair of distinct action occurrences at one layer; with at-most-one rather than exactly-one actions, a layer may idle. Initial-state clauses, goal clauses and corresponding <successor-state axioms> for all other <planning fluents> complete the plan-as-<SAT> construction. The plan-as-<SAT> approach was introduced by <Henry Kautz> and <Bart Selman> in 1992.<Planning as satisfiability by Henry Kautz and Bart Selman>[ECAI 1992, pp. 359–363; author-hosted publication listing]{ref}
Back to article page
