Nagging: A General, Fault-Tolerant Approach to Parallel Search Pruning

Abstract

For some interesting problems, all known algorithms rely, to some degree, on exhaustive search. Since combinatorial search cannot scale to large problem instances, no general-case solutions to these problems are available. However, because solutions to many of these problems have practical value, various software techniques have been developed to avoid or reduce search in a number of useful, special cases. Unfortunately, different software techniques exhibit varying performance advantages from one problem instance to the next; given a particular problem instance, it is not always clear which approach would be most effective. This paper introduces a parallel search-pruning technique called nagging which is means of coordinating the activity of a number of different search procedures. Under this technique, search-based problem solvers compete in parallel to solve parts of a particular problem instance. Each problem solver contributes to advancing the search wherever it is the most effective. Nagging's intrinsic fault tolerance and scalability make it particularly suitable for commonly available, low-bandwidth, high-latency distributed computing environments. It is sufficiently general to be effective in a number of domains. A prototype implementation has been developed for first-order theorem proving, a domain both responsive to a very simple nagging model and amenable to many refinements of this model. Nagging is evaluated by testing this implementation on a suite of well-known theorem proving problems.