Past exam of the computer science course of the University of Oxford / 2023 / Artificial intelligence / 2

In STRIPS, a state records the true ground facts; under the closed-world assumption, an absent fact is false. An action with positive preconditions $P$, add effects $A$ and delete effects $D$ applies when $P\subseteq S$, producing $(S\setminus D)\cup A$.

The given movement action adds the destination fact without deleting the old boat location. After its first crossing the boat can therefore be recorded at both banks, allowing physically impossible loading. Its source-bank symbol is also not a declared action parameter. Repair both issues by using the fully parameterized STRIPS actionHere $\mathrm{notEqual}(s,t)$ excludes a vacuous same-bank crossing. The two static inequality facts already supplied suffice.

The given loading action has no capacity check. Consecutive loads can put arbitrarily many items aboard. Introduce a nullary planning fluent $\mathrm{Empty}$, true initially, and repair loading toUnloading must restore $\mathrm{Empty}$, as in part (c). Including the bank $s$ explicitly as an action parameter removes the other unbound action variable. Equivalently, instantiate separate east-bank and west-bank actions.

These repairs establish the planning state invariants that the boat is at exactly one bank, each item is either at one bank or aboard, and at most one item is aboard. The first two hold initially and are preserved by deleting the former location when adding the new one; the capacity marker permits loading only when no item is aboard. Grounding implicit location variables alone would not repair the missing delete effect or the missing capacity check.

The automated planning goal is the conjunction of the delivered-item facts:The boat need not separately be constrained to end west, although any successful plan with $n>0$ must bring the final item there before unloading it.

Use the STRIPS actionThe onboard precondition prevents inventing an item at a bank, and deleting $\mathrm{onBoat}(x)$ preserves the item's unique location. Restoring $\mathrm{Empty}$ preserves the one-item planning state invariant.

For $i=1,\dots ,n$, executeand, if $i<n$, append $\mathrm{Move}(\mathrm{WEST},\mathrm{EAST})$ before the next iteration.

Each load starts with an empty boat beside an undelivered item. Each unload leaves that item west and restores the loading precondition. By mathematical induction on $i$, after iteration $i$ the first $i$ items are west and the remaining items are east. Thus the automated planning goal holds after $2n-1$ crossings and $4n-1$ actions for $n\ge 1$. For $n=0$, the empty plan already achieves the goal.

Replace the one-place marker $\mathrm{Empty}$ by three nullary planning fluents $q_0,q_1,q_2$, meaning that zero, one or two items are aboard. Initially only $q_0$ is true. Exactly one of these facts is maintained. No additional object constants are needed.

For compactness, define the common loading preconditionsand common unloading preconditionsThe four STRIPS actions areHere the first unloading removes one of two items, and the last unloading removes the sole remaining item; items do not require fixed seat identities. The movement action remains as repaired in part (a) and changes none of the occupancy facts.

The planning state invariant is $q_j$ true exactly when $j$ items are aboard. Every action changes the marker by the same amount as the actual onboard count, so it follows by mathematical induction from the initial empty boat. In particular, a third load is impossible.

Partition the items into successive groups of size two, with a singleton final group if $n$ is odd. For a pair $(x,y)$ on the east bank, executeFor a singleton $x$, executeReturn the empty boat east between groups. Each group starts and ends with marker $q_0$, and its items finish west, proving all preconditions and the final goal by mathematical induction over the groups. For $n\ge 1$ there are $\lceil n/2\rceil$ outward journeys and $2\lceil n/2\rceil -1$ crossings in total; $\lceil \cdot \rceil$ is the ceiling function. Again $n=0$ needs no actions.

Keep the corrected one-place STRIPS model, replace the item constants and their initial typing facts by $\mathrm{FOX},\mathrm{RABBIT},\mathrm{CARROT}$, and require all three west in the goal. The farmer travels with the boat, so the boat's bank also records where supervision is available. The new requirement concerns the bank being left: incompatible items may coexist at the farmer's current bank, but must not be left there together.

Here is a compilation using only ordinary positive STRIPS preconditions. Replace $\mathrm{onBoat}(x)$ everywhere by $\mathrm{at}(x,\mathrm{BOAT})$, extending the item's possible locations toThe boat itself still has only bank locations, enforced by $\mathrm{isBank}$. Initialize a static relation $\mathrm{SafePair}(p,q,s)$ for every $p,q\in \mathcal{L}$ and bank $s$ except $p=q=s$. It states that two incompatible items at locations $p,q$ are not both on the bank about to be left.

Introduce planning safety certificates $\mathrm{SafeToSail}(\mathrm{EAST})$ and $\mathrm{SafeToSail}(\mathrm{WEST})$, neither initially true. The following checking action grants a certificate:Add $\mathrm{SafeToSail}(s)$ to the preconditions of $\mathrm{Move}(s,t)$. Every load, unload and move deletes both certificate facts. The other movement and capacity effects remain unchanged.

Deleting certificates on every location change prevents a stale safety check from authorizing a later unsafe departure. A certificate is granted only for the actual current locations and only when both incompatible pairs are separated on the departure bank. During a crossing the remaining bank is therefore safe; on arrival the farmer supervises the destination bank. This proves the required safety property by mathematical induction over crossings. The static $\mathrm{SafePair}$ facts are never changed.

Write $F,R,C$ for the three item constants, $E,W$ for the banks, $L,U,M$ for the corrected load, unload and move actions, and $K_s$ for $\mathrm{Check}(s,p_F,p_R,p_C)$ instantiated with the items' actual current locations. A fully executable plan in the STRIPS model of part (g) isThus the seven crossings carry rabbit west, nothing east, fox west, rabbit east, carrot west, nothing east, rabbit west.

Immediately before those crossings, the items left on the departure bank are respectively $\{F,C\},\{R\},\{C\},\{F\},\{R\},\{F,C\},\varnothing$. None contains an incompatible pair, so each displayed $K_s$ has its safety preconditions. Each loaded crossing carries exactly one item, and all three finish west.