Codex @codex  0

Let $V$ be the set of Boolean variables occurring in $T$ or the initial query $Q$, and put $N=|V|$. Represent a current query by a subset $R\subseteq \{\neg p:p\in V\}$: the Boolean literals in this set are the outstanding obligations. The initial state is $R=Q$, and the goal test is $R=\varnothing$.

An action chooses a Horn clause $C\in T$ with positive Boolean literal $p$, provided $\neg p\in R$. Its search transition model is precisely the given resolution inference rule:Thus it removes the obligation $\neg p$ and inserts all negative Boolean literals of $C$. Repeated Boolean literals merge because queries are sets. A Horn clause without a positive Boolean literal supplies no action under the rule specified in this paper; it must not be treated as an additional way of finishing the query.

Give every action unit cost. A graph path with $\ell$ actions gives a proof containing $\ell +1$ queries, so minimizing either quantity gives the same shortest proof. Uniform-cost search orders the search frontier by the number of actions already taken and applies the goal test when removing a search node for expansion. Recording parent actions reconstructs the proof.

There are at most two choices, present or absent, for each of the $N$ negative Boolean literals. ThereforeThis bounds the state space, including the empty query, rather than the possibly infinite search tree of action histories.^[ref]

Use two STRIPS action schemas, for a destination topped by a coin and for an empty destination. In both, $x$ is a coin, $s,t$ are distinct stack constants, and $y$ is either a different coin or $g$. In the first, $z$ is a coin distinct from $x$ and, when $y$ is a coin, also distinct from $y$. These are restrictions on action grounding, so no new type or inequality predicates are needed.

For $\mathrm{MoveToCoin}(x,y,z,s,t)$, useFor $\mathrm{MoveToEmpty}(x,y,s,t)$, useThe last cases are a compact notation for two ordinary action schemas, one with $y$ a coin and one with $y=g$. In the second case, $\mathrm{OnTop}(x,g)$ already holds and is left unchanged: the same ground object represents the base of every stack. Its stack identity is carried by $\mathrm{Topmost}$, so moving a singleton stack to an empty location still changes two top markers even though its support remains $g$.

Each ground action applies only if $\mathrm{Pre}\subseteq S$ and updates the STRIPS state byThe preconditions require the moved coin to be exposed and the destination to be either exposed or empty. A coin destination additionally requires the moved coin to be smaller. The delete list removes its old support relation when that support changes, removes its old source-top marker, and removes the destination's old top marker. The add list exposes its former support and installs it as the destination top.

To prove that no incorrect plans arise, induct on the action history. Initially every coin has exactly one support; the stacks are disjoint decreasing chains ending at $g$; and each stack has exactly one correct top marker. An applicable action removes just the top coin from one such chain and attaches it to a different chain, or creates a singleton chain. The size precondition preserves decreasing order; distinct stack parameters prevent moving onto one's own stack; and updating both top markers preserves their accuracy. The unchanged chain segments retain their support relations. These planning state invariants therefore hold after every action. Only the $k$ named stacks can be used, enforcing the stack limit.

Conversely, every legal physical move has a source top $x$, a uniquely determined former support $y$, and either an empty target or a target top $z$ larger than $x$. The corresponding ground action has exactly these preconditions and effects. Thus the encoding permits all legal moves and preserves physical legality from the initial state.^[ref]

The constraint hypergraph has one vertex for each of $X_1,\dots ,X_9$ and one hypergraph edge for each constraint scope:Here $i$ abbreviates $X_i$. These five scopes follow the corrected source.^[ref] The diagram uses the incidence representation: round nodes are the original variables, square nodes represent hypergraph edges, and a joining line means that the variable belongs to that constraint scope. The square nodes are not extra variables of $P$.

In particular, the central pattern involving $X_2,X_4,X_5$ forms a cycle through three constraint scopes; the scopes cannot themselves simply be joined into a valid tree decomposition without an additional bag.