Conspiracy Numbers and Caching for Searching And/Or Trees and Theorem-Proving

1 Introduction

This paper applies the idea of conspiracy numbers [McAllester, 1988] to derive two heuristic algorithms for searching and/or trees. The first algorithm turns out to be a member of the class of AO* best-first algo­ rithms [Nilsson, 1980], but itconforms to the principle of sunk costs (a rule of economic rationality not respected by traditional and/or tree search algorithms) and hence the standard guarantees of termination and admissibility do not apply usefully to it.

The second algorithm works depth-first. It guides the search done by an iterative deepening SLD-resolution theorem prover that we have implemented. In addition to caching successes, the prover caches failures and uses the latter to avoid repeated effort also. The prover ex­ ploits the fact that a new goal matches a cached success or failure if it is a substitution instance of the cached goal, not just if the two are identical. Unlike many heuristics for guiding search and saving effort, the con­ spiracy number and caching ideas introduced in this pa­ per can be implemented efficiently. Our experimental results indicate that conspiracy numbers and especially the new caching scheme are effective in practice.

Section 2 develops the best-first conspiracy numbers algorithm, relates it to traditional and/or tree search algorithms, and then presents the depth-first conspir­ acy numbers algorithm. Section 3 describes our theorem prover and compares it to a similar PROLOG-technology theorem prover [Stickel, 1986]. The caching done by our prover is discussed in Section 4. Finally, our experimen­ tal results appear in Section 5, and Section 6 contains our conclusions.

·This research was supported in part by the United States Office of Naval Research through grant N0014-88-K-0123.

2 Best-first and depth-first conspiracy number algorithms

And/or trees are well-known [Nilsson, 1980; Pearl, 1984], and we shall describe them here only to the extent neces­ sary to make the terminology of this paper understand­ able. Briefly, an and/or tree is a tree where each node is an and-node or an or-node. The children of and-nodes are required to be or-nodes, and vice versa. An and/or tree may be completely or partially explored. Each node of a completely explored and/or tree is solved or failed. An internal and-node is solved if each of its children is solved and it is failed if at least one of its children is failed. Conversely, an internal or-node is solved if at least one of its children is solved, and failed if all its children are failed. A partially explored and/or tree also contains leaf nodes called unexpanded leaves whose children have not yet been discovered. The solved/failed status of an unexpanded leaf is unknown, as is the status of any in­ ternal node of a partially explored tree whose status is not fixed by the status of its children.

A solution of an and/or tree is a subtree that demon­ strates that the root of the tree is solved. The aim of searching an and/or tree is to find a solution. Concretely, a solution is a subtree such that all its nodes are solved, all the children of each of its and-nodes belong to the subtree, and at least one of the children of each of its or-nodes also belongs to the subtree. The basic search­ ing operation on a partially explored and/or tree is to expand an unexpanded leaf of the tree. When such a leaf is expanded there are three possible outcomes: it can be discovered to be solved, it can be discovered to be failed, or it can be discovered to have children, which are new unexpanded leaves. Different searching algo­ rithms choose in different ways which unexpanded leaf to expand next.

2.1 Best-first conspiracy number search

The notion of conspiracy was invented in the context of min/max tree searching [McAllester, 1988]. Informally, a conspiracy for a min/max tree is a set of leaf nodes of the tree such that if their values were to change, then the value obtained for the root of the tree by min/max propagation might also change. The following definition for and/ or trees is analogous.

Definition 2.1: A conspiracy for a partially explored and/or tree is an inclusion-minimal set of unexpanded leaves of the tree such that if each node in the set is found to be solved then the root of the tree is also solved. ·

Our aim in searching an and/or tree is to find a solution as quickly as possible. Intuitively, the bigger a conspir­ acy is, the less likely all ofits members can be solved, and the more time will be required to attempt to solve them. Thus an appealing heuristic for guiding search is always to expand next a member of the currently smallest con­ spiracy. This heuristic characterizes best-first conspira­ torial search.

A best-first conspiratorial search algorithm can quickly identify a member of the smallest conspiracy of a partially explored and/or tree by keeping track of con­ spiracy numbers.

Definition 2.2: The conspiracy number en(a) of a node a is the cardinality of the smallest conspiracy of the partially explored and/or subtree rooted at a. ·

The next lemma provides a constructive definition of conspiracy numbers.

Lemma 2.3:

• If a is a solved leaf then en( a) = 0.
• If a is a failed leaf then en( a) = oo.
• If a is an unexpanded leaf then en( a) = 1.
• If a is an and-node with children at, ... , ak then en(a) = L:~ en(ai)·
• If a is an or-node with children at, ... , ak then en(a) = min{en(ai)}. ·

Lemma 2.3 implies that whenever a leaf is expanded, only the conspiracy numbers of nodes on the path from that leaf to the root need to be updated. The next lemma says how an unexpanded leaf in the currently smallest conspiracy can be found quickly.

Lemma 2.4: An unexpanded leaf !3m that is a member of the smallest conspiracy of a partially explored and/or tree can be found by following a path f3t, ... , f3m from the root f3t of the tree such that

• (i) for each and-node Pi on the path, f3J+t is a child or-node of Pi and en(f3J+t) > 0, and
• (ii) for each or-node !3; on the path, fJ;+t is a child and­ node of Pi and en(f3J+t) = en({Ji ). ·

2.2 Conspiracy numbers, AO* algorithms, and the principle of sunk costs

Traditional and/or tree search algorithms are mem­ bers of the class of AO* algorithms [Nilsson, 1980;

Pearl, 1984]. AO* algorithms are interesting because un­ der certain conditions, they are guaranteed to terminate and to find optimal solutions. Lemma 2.3 shows that the function en is of the form used by AO* algorithms. However the standard guarantees do not apply usefully to best-first conspiratorial search, because it respects the principle of sunk costs.

Principle of Sunk Costs: Amounts of resources ex­ pended in the past on different activities are irrelevant to the decision of which activity to pursue now. ·

Although people often act contrary to the principle of sunk costs, it is a guideline for rational agents that com­ mands universal assent among economists [McCloskey, 1985; p. 267]. The principle says that, for example, the costs incurred to build a nuclear power plant should have no bearing on the decision whether or not to operate the plant.

For guaranteed termination at a minimal-cost solu­ tion, in deciding which node to expand next and when to halt, one must take into account the cost so far of in­ complete solutions. The principle of sunk costs disallows this.

Termination. The nodes on an indefinitely long path from the root of an and/or tree can all have the same minimal conspiracy number. Hence best-first conspira­ torial search is not guaranteed to terminate.

Admissibility. AO* algorithms find optimal solutions because of their termination criterion, when they use conservative heuristic functions.

Let Q be a function assigning measures to solutions. An AO* heuristic function h is a conservative estimator of Q if for all nodes a, h(a) is less than the lowest Q measure of any solution of the and/or subtree rooted at a. The termination criterion for an AO* algorithm is to stop only when no incomplete solution induces an h value for the root lower than the h value induced by the best complete solution found so far. Then the fact that h is a conservative estimator of Q guarantees that all solutions not yet found are worse under Q than this best solution, given that the h values induced by complete solutions are their Q measures.

The Q that assigns the measure 0 to every solution is the only Q according to which the en values induced by complete solutions are their Q measures. Best-first con­ spiratorial search does find optimal solutions according to this trivial measure.

The en heuristic function is a conservative estimator of some non-trivial solution measures. For example en is a conservative estimator of the number of nodes that a solution contains. However if Q is a non-trivial measure, then best-first conspiratorial search does not in general find optimal solutions according to Q, because the en values induced by complete solutions are less than their Q measures.

2.3 Depth-first conspiracy number search

The intuition behind depth-first conspiracy number search is to explore an and/or tree in depth-first fashion, but to backtrack when the smallest conspiracy involving a leaf is too large. Conspiratorial depth-first search has two advantages: the and/or tree being searched need never be stored explicitly, and the decision whether to expand a leaf can be made using only information avail­ able at that leaf. A disadvantage is that leaves are not expanded in best-first order.

Suppose an and/or tree is searched in depth-first fash­ ion. Then at any time one can identify a stack of or­ nodes whose subtree is currently being explored. The deepest node on this stack is the one whose subtree will be explored next. Each of the or-nodes in the stack has some sibling or-nodes. If the deepest or-node can be solved, and the siblings of all the less deep or-nodes can also be solved, then a solution has been found for the whole tree. Thus the deepest or-node on the stack and the siblings of the less deep or-nodes constitute a con­ spiracy. In fact, they constitute the only conspiracy of the current partial and/or tree, since the nodes on the stack and their siblings are the only nodes of the tree whose subtrees have not already been fully explored, and discovered to be failed.

The information needed to decide during bounded depth-first search whether to expand a leaf is its con­ spiracy depth according to the following definition.

Definition 2.5: The conspiracy depth of a node in a partial and/or tree is the size of the smallest conspiracy of the whole tree involving that node. ·

The next lemma implies that conspiracy depths can be computed with only a constant amount of extra work per node, during depth-first exploration of an and/or tree.

Lemma 2.6: Consider the function cd defined on the nodes of an and/or tree as follows.

• Let a be the root of the tree. Then cd( a) = 1.
• Let a be an and-node with cd(a) = c. Let a have k children a 1 , ... , a 1c which are explored in order. Then cd( a i) = c + k - j.
• Let a be an or-node with cd( a) = c. Let the children of a be a 1 , .. . ,aJc. Then cd(ai) =c.

At the time the decision is made whether or not to ex­ pand a leaf a during depth-first search of an and/or tree, the conspiracy depth of a is cd( a). ·

Conspiratorially bounded depth-first search can be im­ plemented efficiently.

3 A conspiratorial SLD-resolution theorem prover

Conspiratorially bounded depth-first search guides the search done . by a theorem prover that we have im­ plemented. The only inference rule of our prover is SLD-resolution [Lloyd, 1984]. The space that must be searched to find a proof of a given goal (an atomic first­ order predicate calculus formula) by SLD-resolution is an and/or tree, where or-nodes correspond to subgoals that must be unified with the head of some matching clause, and and-nodes correspond to bodies of clauses. For such an and/or tree, a conspiracy consists of a set of subgoals that must all be proved together. In order to do so, one must find an an answer substitution for each sub­ goal such that none of the substitutions conflict. Thus as a conspiracy gets larger, even if whether an answer substitution exists is a statistically independent event for each of its members, heuristically the chance that all the members can be compatibly proved decreases as if the events were negatively correlated.

At the highest level, our prover uses the idea of itera­ tive deepening [Korf, 1985; Stickel and Tyson, 1985]: it repeatedly does depth-first search with increasing con­ spiracy depth bounds, until a solution is found. Our prover is thus similar to the PROLOG-technology theo­ rem prover PTTP [Stickel, 1986]. PTTP does iteratively deepened depth-first search using a depth function sd which is the same as the conspiracy depth function cd except on and-nodes. If a is an and-node with k chil­ dren at, ... , a1c then sd( ai) = c + k for each child ai, whereas cd(aj) = c + k- j. The function sd is not con­ sistent with the principle of sunk costs. In depth-first search, the child ai of an and-node is only expanded if its siblings at, ··. , aj_1 have been solved. The effort required to do this is in the past at the moment the de­ cision is made whether or not to expand ai. At that moment it is only relevant what subgoals remain to be solved, and there are c + k - j of them.

A second difference between PTTP and our prover is that PTTP attains first-order completeness, because it uses a model elimination inference rule in addition to SLD-resolution. In future work we plan to extend our prover similarly.

Using conspiracy depths to limit search leads to one difficulty: the conspiracy depth of an indefinitely large partial solution can be finite. If an and-node a has a sin­ gle child a' then cd(a') = cd(a), so in a partial and/or tree, it is possible for the nodes on an infinite path each to have the same conspiracy depth. This problem is circumvented in our prover by using a modified conspir­ acy depth function cd' such that if ai is any child of the and-node a, then cd'(aj) > cd'(a). Specifically, the definition of cd' is identical to that of cd, except that if a is an and-node with k children a1, ... , a1c then cd' (a i) = c + k - j + c. For want of any principled way to choose £, our prover takes £ = 1.

4 Caching successes and failures

This section explains the caching scheme implemented in our SLD-resolution prover. The idea of caching is to store the results of past computations in order not to waste time repeating them in the future [Keller and Sleep, 1986; Pugh, 1988]. Caching is especially useful combined with iterative deepening, because results that have been cached during search to one depth bound can be reused during later searches. Our caching scheme is distinctive in two respects.

First, if we fail to prove a subgoal within a specified conspiracy depth bound, we cache the fact of the failure. If we attempt to prove the same subgoallater within the same or a lower conspiracy depth bound, the attempt is recognized as doomed to failure and it is aborted. Some systems cache subgoals known to be false, which are of­ ten called contradictions or nogoods [de Kleer, 1986]. Our prover also caches resource-bounded failures.

Second, we take advantage of the fact that with SLD­ resolution, an attempt to prove a subgoal is an attempt to prove any substitution instance of it. If our prover succeeds or fails in proving a subgoal, then later it takes any instance of the subgoal as proven or impossible to prove, respectively.

The new prover maintains two separate caches, called the success and failure caches. Both the success and failure caches grow monotonically across iterative deep­ ening cycles. The success cache II is where proven sub­ goals are remembered. Whenever a subgoal j3 is proven with answer substitution u, then /3' is added to II, where /3' = j3u. The next lemma says that a subgoal can be taken as proven if it is an instance of an entry in II.

Lemma 4.1: If "( is in II and "( 1 is a substitution instance of 'Y, then 1- "( 1 ·

Proof: Suppose 'Y is in II, so 1- 'Y· That signifies 1- VX 'Y where x is the vector of free variables of 'Y· So for any vector of terms t, it is the case that 1- "f[x 1---+ t]. Let "( 1 be a substitution instance of 'Y· That means "( 1 = "f[x 1---+ t] for some t. ·

Whenever our prover attempts to prove a subgoal j3 within the conspiracy depth bound m and fails, it adds the pair (/3, m} to the failure cache fl. The next lemma justifies the way entries in f2 are exploited. The notation 1-m/3 means j3 is provable within the conspiracy depth bound m.

Lemma 4.2: If ("f, n} is in f2 and 'Y' is a substitution instance of"( and m ~ n, then 'f m "( 1 ·

Proof: An attempt to prove 'Y with resource bound n succeeds with answer substitution u if for some m < n and some u, it is the case that 1-m"fU. Thus if ("f, n) is in f2 then for all u and m ~ n, 'fm"fU. But 'Y' = "fU for some u. ·

Suppose the attempted proof of the subgoal 'Y failed absolutely: the space of potential proofs of 'Y was ex­ plored completely and no proof was found. Then for all n, lfn "( 1 if "( 1 is an instance of 'Y· Our prover takes this into account.

Conversely, the prover only takes a goal "( 1 as proven because it is an instance of an entry 'Y in the success cache II if the depth bound on the current attempt to prove "( 1 is not greater than the depth of the proof of 'Y that caused 'Y to be added to II. The effect of this restriction is that the and/or tree of potential proofs explored with caching is exactly the same as the tree explored without caching.

The caching scheme just described was independently discovered and implemented in unpublished work by Stickel. He found that the overhead of caching out­ weighed its benefits, for the class of theorems he inves­ tigated. Our experimental results, reported in the next section, are different. The remainder of this section dis­ cusses how to implement caches efficiently and proves that caching is asymptotically beneficial under reason­ able assumptions.

4.1 Implementing instance-lookup caches

An implementation of a success or failure cache E must support two abstract access operations:

• install(E, "(, m): place 'Yin E with associated depth m, and
• query(E, "(, m): decide whether a j3 with associated depth n exists in E such that 'Y is an instance of j3 and n ~ m.

The entries in a cache are atomic logical formulas. Ac­ cessing a cache involves substitution instance testing, so it is not possible to use standard hashing techniques to implement caches. For our prover we choose to represent each cache by a binary tree with a member of the cache stored at each node of the tree.

Let a( n) be the value stored at node n. According to a total order -< on terms, the tree representing each cache is symmetric-ordered: for all nodes n,

• if the node I belongs to the left subtree of n then a(l)-< a(n), and
• if the node r belongs to the right subtree of n then a(r) >- a(n).

The relation-< is defined on formulas and their subterms as follows.

• -< is an alphabetic order on pairs of atomic symbols and on pairs of variables.
• f(x) -< g(y) if f -< g or f = g and x -< y lexico­ graphically.
• If x is a variable then x -< t for every non-variable term t.

The operation query(E, "(, m) is performed by walking down from the root of E, at each node n answering yes if"( is an instance of a( n ), otherwise moving left if 'Y -< a(n), moving right if"( >- a(n), and answering no if n is a leaf. The operation install(E, "(, m) is performed similarly.

If the tree representing a cache is balanced, then install(E, "(, m) and query(E, "(, m) operations both use O(log lEI) time. There are standard techniques for keep­ ing symmetric-ordered trees balanced [Tarjan, 1983], which will not be discussed here.

Unfortunately the order-< on formulas is not instance­ respecting: it may be the case that 'Y is a substitution in­ stance of a1 and "( -< a2 yet a 2 -< a1. Thus it may happen that query(E, "(, m) is answered no when the correct answer is yes. In our experience this happens infrequently. The next lemma says that there is no al­ ternative order to -< that avoids this problem.

Lemma 4.3: No instance-respecting total order exists. Proof: Suppose< is an instance-respecting total order. Let x, y, and z be three distinct variables. Without loss of generality assume x < y < z. Now x is an instance of z and. x < y so z < y, a contradiction. ·

The order -< can be made into an instance-respecting partial order by declaring that if x is a variable, then for any term t, x -/< t and t -/< x. We believe that there are efficient ways to implement caches supporting substitu­ tion instance queries based on this partial order, or on discrimination trees [Forgy, 1982; Charniak et al., 1987].

When a subgoal is found to be an instance of a cache entry, then that subgoal gives rise to no child subgoals. Thus one expects caching to reduce the effective branch­ ing factor of the and/or tree representing the space to be searched to find an SLD-resolution proof. The following theorem says how much the effective branching factor must be reduced for caching to be beneficial.

Theorem 4.4: Let the effective branching factor be be with caching, and bo without caching. Let the time to execute an instaii(E, -y, m) or query(E, -y, m) operation be c(IEI) = o(IEIP). Then caching saves time if 1 + p < log bo/ log be.

Proof: Let the time required to find a solution be To without caching, and Te with caching. We wish to know when Te < To. Let to be the time required to expand one subgoal, without caching. It is reasonable to assume that to is a constant and To = moto, where mo is the number of subgoals expanded before finding a solution. If a solution is first found at depth d, then a lower bound on m0 is m(d- 1, b0 ), where

The solution found first with caching is the same, at the same depth d. The time required to expand one subgoal with caching is te = to+ c(IEI), where E is the cache at the time that subgoal is expanded. The cache grows monotonically, but cannot have more than one entry for each different subgoal expanded, so lEI < b~ always. Thus

Caching is advantageous if logTe < logT0 · We have log To> dlogbo + 0(1) and

Thus for some do, for all d > do, if 1 + p < log bo/ log be then Te <To. ·

Note that if c(IEI) = O(log lEI) then c(IEI) = o(IEIP) for all p > 0, so for caching to be beneficial it is only necessary that be < bo.

In our experience caches do not grow fast. For the problem described in the next section, where m0 is greater than 1000 000, both the success and failure caches ended with under 150 entries. It is definitely ad­ vantageous to treat any instance of an explicit cache en­ try as an implicit entry.

5 Experimental results

We have performed two sets of experiments to evalu­ ate the usefulness of the ideas developed in this pa­ per. Each experiment involved using a different search algorithm to search the same and/or tree. The tree used in all our experiments is the tree representing the SLD-resolution search space for a monkey-and-bananas situation-calculus planning problem [Plaisted, 1986).

The first set of experiments compared iterative deep­ ening with three different depth functions: actual proof depth, the PTTP depth function, and the modified con­ spiracy depth function cd'. The results of the experi­ ments are shown in Figure 1. Measured by the total number of nodes expanded, the conspiracy depth func­ tion has a slight advantage. (The first solution to the monkey-and-bananas problem has actual proof depth 11, PTTP depth 24, and modified conspiracy depth 29. Search to any depth is cut off when a solution is found, so the maximum number of nodes expanded occurs with PTTP depth bound 23 or conspiracy depth bound 28.)

Using iterative deepening with the conspiracy depth function cd', the second set of experiments compared four caching regimes: no caching, caching of successes only, caching of failures only, and full caching. In each case the same search space was explored. Note that with caching of successes or with full caching, the first solution found is cached, so the problem can then be solved with just one node expansion when searching to depth 30, 31, and so on.

The results of the second set of experiments are shown in Figure 2. With no caching the effective branching fac­ tor is approximately 1.61. Caching successes reduces it to 1.46, caching failures to 1.55, and caching both to 1.40. The improvement is clear. It is especially encouraging that the benefits of caching successes and failures are cumulative. For our sample problem, the branching fac­ tor reduction achieved with full caching translates into a 99% reduction in the search space size.

6 Conclusion

In this paper we have described heuristic best-first and depth-first algorithms for searching and/or trees based on the intriguing idea of conspiracy numbers. We have also described an SLD-resolution theorem prover that uses the depth-first conspiracy numbers algorithm and a caching scheme that is sophisticated yet amenable to theoretical analysis. The theorem prover relies only on heuristics that can be implemented efficiently: it does not sacrifice speed for intelligence.

Naturally many issues remain unresolved. We con­ jecture that an algorithm conforming to the principle of sunk costs provably dominates in some way an algorithm that violates the principle, but we do not know in what way. We also do not know how to characterize the class of theorem-proving problems for which the caching ideas described here are beneficial.

Acknowledgements. Section 2 reports on work done jointly with David McAllester. Discussions with James Altucher, Wilfred Chen, David McAllester, and Alberto Segre were helpful in developing the ideas reported m Section 4.