Let be the set of Boolean variables occurring in or the initial query , and put . Represent a current query by a subset : the Boolean literals in this set are the outstanding obligations. The initial state is , and the goal test is .
An action chooses a Horn clause with positive Boolean literal , provided . Its search transition model is precisely the given resolution inference rule:
Thus it removes the obligation and inserts all negative Boolean literals of . 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 actions gives a proof containing 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 negative Boolean literals. Therefore
This bounds the state space, including the empty query, rather than the possibly infinite search tree of action histories.[ref]
A-star search is best-first search with priority
Here is a search node, is its state, is its accumulated path cost, and is the minimum remaining cost to any goal state, interpreted as if no goal is reachable. The inequality defines an admissible heuristic. Thus is a lower bound on the cost of any solution extending that particular action history.
Initialize the search frontier with the root. Repeatedly remove a search node of least , apply the goal test, and, if it is not a goal, insert its applicable-action children with their updated and . In tree search, different action histories remain distinct search nodes even when they reach the same state; there is no global visited-state set.
For the finite branching factor and unit costs here, an admissible heuristic ensures that any first goal removed is optimal. If a cheaper solution existed, the search frontier would contain an unexpanded prefix of it with at most that cheaper cost, contradicting selection of the more expensive goal. Nonnegative also means only finitely many search nodes can have below any fixed finite cost, so a finite solution will eventually be reached. This does not guarantee termination when no proof exists.
Termination is not guaranteed. Take
Both members of are valid Horn clauses with distinct underlying Boolean variables. The only possible continuation alternates
The empty query is unreachable. With the admissible heuristic , 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
The unit-cost 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 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.
Yes: is an admissible heuristic. One application of the resolution inference rule removes just one current negative Boolean literal. It may add other negative Boolean literals, and some of those may already occur, but it cannot remove any other current obligation. Consequently
If actions lead from to , applying this inequality at every step gives . Thus
It is also a consistent heuristic, since and . In particular, merging duplicate obligations cannot invalidate the lower bound: removing several duplicates from the representation never counts as removing several distinct members of a set.
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.
When the values of several admissible heuristics are already available, choose their maximum:
Every , so their maximum is still an admissible heuristic. It has heuristic dominance over their minimum and their arithmetic average, which are also admissible heuristics but give no larger lower bound. Thus the maximum supplies the most informative generally valid choice among these alternatives.
Their sum can overestimate by counting the same remaining action repeatedly. If two heuristic functions both give the exact value at a state one action from the goal, their sum gives . A valid sum requires extra structure such as dividing each action's cost between the component estimates; admissibility of the components alone does not provide that structure.
Larger admissible values reduce the region that A-star search must expand before an optimal solution of cost can be removed. This is a statement about heuristic dominance, not a strict claim about running time under every tie-breaking rule or evaluation cost.

Articles by others on the same topic (0)

There are currently no matching articles.