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

Abstract

This paper applies the idea of conspiracy numbers to derive two heuristic algorithms for searching and/or trees. The first algorithm is an AO* best-first algorithm but the standard guarantees do not apply usefully to it because it conforms to the economic principle of sunk costs. The second algorithm works depth-first and guides the search done by an iterative deepening SLD-resolution theorem prover that we have implemented. To avoid repeated effort, the prover caches successes and failures. It exploits the fact that a new goal matches a cached goal if it is a substitution instance of the latter, not just if the two are identical. Experimental results indicate that conspiracy numbers and especially the new caching scheme are effective in practice.