email: wolfa@in.tum.de, phone: +49 89 28927924, fax: +49 89 28927902
Introduction. A search problem is typically solved by a uniform search procedure. In automated deduction, different search strategies may have a strongly different behavior on a given problem. Unfortunately, in general, it cannot be decided in advance which strategy is the best for a given problem. This motivates the competitive use of different strategies, especially if the available resources are restricted. In order to be successful with such an approach, the strategies must satisfy the following two conditions: (1) The quotient of the number of problems solved in time t by t is sub-linear for each strategy, and (2) the sets of problems solved by the involved strategies must differ "significantly". If both conditions are satisfied, then a competitive use of different strategies can be more successful than the best single strategy. The first condition is typically satisfied in automated theorem proving whereas the second one has not been focused by automated deduction research so far.
The selection of more than one search strategy in combination with techniques to partition the available resources task-dependently defines the new parallelization method strategy parallelism. Distributed competitive agents deal with the same problem, but with modified search spaces. The strategies shall traverse the search space such that, in practice, the repeated consideration of the same parts is avoided.
Related approaches are Partitioning, TeamWork, Clause Diffusion, and Nagging (references omitted). There is a number of issues with importance for strategy parallelism. How can strategy sets be obtained that solve as many problems as fast as possible and have sets of solved problems that differ as much as possible? Often, strategies are successful for a certain problem class. The identification of such features makes the selection of strategies more specificly and hence more successfully. The success of the selected strategies depends on the training set. How do we obtain a training set which is representative for the considered domain of problems? The number of sensible strategies which are successful and differ as much as possible seems to be bounded. This restricts the scalability to large platforms. Can we find a systematic method for producing as many successful and differing strategies as we want?
Strategy Selection. We are faced with a strategy allocation problem. Given a set of training problems, a set of usable strategies, a time limit, and a number of processors, we want to determine an optimal distribution of resources to each strategy, i.e., a combination of strategies which solves a maximal number of problems from the training set within the given resources. Unfortunately, even the one processor decision variant of this problem is strongly NP-complete. Therefore, in practice, the determination of an optimal solution for the problem is problematic. We use a combination of randomization elements with a gradient procedure of restricted dimension to select strategies.
Implementation. We used the SETHEO [3] prover and implemented an environment for strategy parallel theorem proving, p-SETHEO. Currently, all contained strategies are variants of SETHEO. The implementation uses PERL, PVM, C, and shell tools. The parallelization model of p-SETHEO works as follows. (1) Select a set of triples of strategies, times, and processors according to the actual problem. (2) Perform the needed preprocessing. (3) Start all prover strategies, the first successful prover stops the others.
Experiments. Within the ILF system [1] a simplified version of p-SETHEO was compared with other provers on 97 problems from the MIZAR library [2]. The time limit was 15 seconds CPU time per attempt. Without direct support of the prover authors the compared provers reached the following results: Gandalf 47, Otter 60, p-SETHEO 76, SPASS 52, all together 94 problems.
Assessment. Our experiments showed that one can significantly increase the performance of theorem provers. Often the advanced user can tune a prover to a given problem using his experience. This is not possible if the theorem prover is used as a black box like in ILF [1]. Here, strategy parallelism provides automatic configuration.
References
1. B. I. Dahn et al. Integration of Automated and Interactive Theorem Proving . . . CADE-14, pp. 57{60, 1997.
2. B. I. Dahn, C. Wernhard. 1st Order Proof Problems . . . FTP-97, RISC Linz, Austria, pp. 58-62, 1997.
3. M. Moser et al. SETHEO and E-SETHEO. The CADE-13 Systems. JAR, 18(2), pp.