= Solution
\b[Termination is not guaranteed.] Take
$$
Q=\{\neg p\},\qquad T=\bigl\{\{p,\neg q\},\{q,\neg p\}\bigr\}.
$$
Both members of $T$ are valid <Horn clauses> with distinct underlying <Boolean variables>. The only possible continuation alternates
$$
\{\neg p\}\longmapsto\{\neg q\}\longmapsto\{\neg p\}\longmapsto\cdots.
$$
The empty query is unreachable. With the <admissible heuristic> $h=0$, ordinary <A-star search> keeps generating the next <search node> forever, despite there being only two reachable states.
A modification requiring no additional stored state collection is to impose the known <search depth> bound
$$
\boxed{L=2^N-1,\qquad\text{do not expand a non-goal node with }g=L.}
$$
The unit-cost $g$ already stored by <A-star search> is also its <search depth>; the bound is a scalar computed from the input, not a closed <set>. Apply the <goal test> before refusing expansion at the bound.
To prove completeness of this modification, remove any segment between two equal states in a successful proof. The successor choices after the later occurrence are available at the earlier occurrence because the <search transition model> depends only on the current query. Repeating this removal gives a proof with no repeated states, hence at most $2^N-1$ actions. In particular, a shortest proof never needs a repeated state, since every removed segment has positive cost. The depth restriction therefore preserves a shortest proof whenever one exists.
The restricted <search tree> has finite depth and finite <branching factor>, so it is finite. <A-star search> must then either remove a goal or exhaust the <search frontier> and report failure. Its existing <search frontier> may still be large; the modification saves a separate visited-state collection, not all storage used by <tree search>.
Back to article page
