AAAI Publications, Sixth European Conference on Planning

Font Size: 
Randomization and Restarts in Proof Planning
Andreas Meier, Carla P. Gomes, Erica Melis

Last modified: 2014-05-21


Proof planning considers mathematical theorem proving as a planning problem. It has enabled the derivation of mathematical theorems that lay outside the scope of traditional logic-based theorem proving systems. One of its strengths comes from heuristic mathematical knowledge that restricts the search space and thereby facilitates the proving process for problems whose proofs belong in the restricted search space. But this may exclude solutions or restrict the kinds of proofs that can be found for a given problem. We take a different perspective and investigate problem classes for which little or no heuristic control knowledge is available and test the usage of randomization and restart techniques. Our approach to control in those mathematical domains is based on investigations on so-called heavy-tailed distributions (Gomes et al. 2000; 1998; 1998). Because of the non-standard nature of heavy-tailed cost distributions the controlled introduction of randomization into the search procedure and quick restarts of the randomized procedure can eliminate heavy-tailed behavior and can take advantage of short runs. To apply these techniques to the complicated domains of proof planning, the first task was to find problem classes for which proof planning exhibits an unpredictable run time behavior, i.e., with heavy-tailed cost distributions. Secondly, the experiments provided the basis for determining suitable cutoff values, i.e., the time interval after which a running proof attempt is interrupted and a new attempt is started. Finally, we designed a new control strategy which dramatically boosts the performance of our proof planner for a class of problems for which proof planning exhibits heavy-tailed cost behavior.

Full Text: PDF