Andreas Meier, Carla Gomes, and Erica Melis
Our experiments show the effectiveness of our randomized proof planning approach by showing a significant improvement in performance over a testbed of 160 non-isomorphism problems. In particular, with our approach, a much larger fraction of problem instances is solvable (from 67.5% to 97.5%; 2hr time limit per proof) and a variety of proofs is generated for each problem instance. Our work demonstrates that randomization and restarts can be successfully applied to deduction systems. We believe these results are very promising and might apply to other problem domains using deduction techniques such as e.g., software verification.