Strategy Selection by Genetic Programming

Strategy parallelism is a powerful concept for applying parallelism to automated theorem proving. One of the most important problems to be solved in this approach is the proper distribution of the available resources among the different strategies. This task usually requires a lot of user expertise. When the resource distribution has to be done automatically, an adaptive algorithm must be used to optimize prover performance. We introduce a genetic algorithm that can be used for such an optimization and we show how such an algorithm can be integrated with other methods for automatic prover configuration. We give some experimental data to verify the validity of our approach and explain some of the future development possibilities.