Graph Neural Networks for Scheduling of SMT Solvers
Jan Hůla, David Mojžíšek, Mikoláš Janota · 2021 IEEE 33rd International Conference on Tools with Artificial Intelligence (ICTAI) · 2021
This paper develops an approach to the scheduling of solvers in the domain of Satisfiability Modulo Theories (SMT) using a Graph Neural Network (GNN). In contrast to related methods, GNNs do not require manual feature design as they enable discovering relevant features in the raw data. We train them to predict the effectivity of individual solvers on a given problem. Rather than choosing only one solver with the best prediction, we schedule the solvers by ordering them according to the predicted runtime and dividing the overall runtime into all solvers uniformly. We compare our approach to several baselines. In the selected benchmarks, we show a substantial improvement over these baselines in terms of the number of solved problems and overall solving time.