Targeted Configuration of an SMT Solver

We present a generic method to configure an automated reasoning solver in order to increase its performance on selected target problems. We describe a strategy invention system Grackle that is designed to invent a set of strong and complementary solver strategies. The strategies are then used to train a gradient boosted decision tree model to select the best strategy for a specific input problem. We evaluate our method on the SMT solver Bitwuzla and we obtain a significant increase in the number of solved problems, and a substantial decrease in runtime.