Use the shortest path distances in the directed dependency graph to define
The additional counts the final use of a positive unit Horn clause, which corresponds to a fact rather than an edge of .
To justify the new lower bound, consider any complete proof from and fix . At some step this obligation must be removed using a Horn clause with head . If that Horn clause is the fact , we have already found a dependency graph path of length zero ending at a fact. Otherwise select one negative body Boolean literal . Immediately after the step it belongs to the query, whether newly inserted or merged with an existing obligation. It must subsequently be removed. Record the edge and repeat this argument at its later removal.
The selected removal times strictly increase. Since the proof is finite and ends with no obligations, this chain eventually uses a fact. A proof of actions therefore produces a dependency walk of at most edges from to a fact. Removing any cycles from that walk gives . Hence for every initial obligation. If , no such proof exists. Combining this bound with the admissible heuristic by taking their maximum preserves admissibility.
For a strict improvement, use
Here , so while . The three successive obligations are , followed by the empty query, so the improved bound is exact.
Do not sum all the values without an additional argument: different obligations may share work. For example, with , the query takes three actions, while that sum would be four.

Articles by others on the same topic (0)

There are currently no matching articles.