一句话：提出基于图神经网络的 SMT 求解器自动选择器 Sibyl，显著加速多种软件工程工具中的 SMT 查询求解。
SMT 求解器常用于程序验证、测试生成和程序合成等工具的后端。不同求解器针对不同逻辑和问题优化，查询微小变化即可改变最优求解器，设计时固定选择会错失优化机会。本文提出基于图神经网络（GNN）的自动 SMT 选择器 Sibyl。Sibyl 将查询表示为图，用 GNN 预测各候选求解器在该查询上的性能，并自动学习训练集特征，无需人工特征工程。训练后能快速准确预测，大幅减少求解一组查询的时间。在 SMT 竞赛、符号执行引擎、有界模型检测器和程序合成工具四种场景中评估，Sibyl 几乎在所有情况下优于现有技术，泛化性更好，开销低，有潜力加速多种工具。
SMT solvers are often used in the back end of different software engineering tools─e.g., program verifiers, test generators, or program synthesizers. There are a plethora of algorithmic techniques for solving SMT queries. Among the available SMT solvers, each employs its own combination of algorithmic techniques that are optimized for different fragments of logics and problem types. The most efficient solver can change with small changes in the SMT query, which makes it nontrivial to decide which solver to use. Consequently, designers of software engineering tools often select a single solver, based on familiarity or convenience, and tailor their tool towards it. Choosing an SMT solver at design time misses the opportunity to optimize query solve times and, for tools where SMT solving is a bottleneck, the performance loss can be significant. In this work, we present Sibyl, an automated SMT selector based on graph neural networks (GNNs). Sibyl creates a graph representation of a given SMT query and uses GNNs to predict how each solver in a suite of SMT solvers would perform on said query. Sibyl learns to predict based on features of SMT queries that are specific to the population on which it is trained - avoiding the need for manual feature engineering. Once trained, Sibyl makes fast and accurate predictions which can substantially reduce the time needed to solve a set of SMT queries. We evaluate Sibyl in four scenarios in which SMT solvers are used: in competition, in a symbolic execution engine, in a bounded model checker, and in a program synthesis tool. We find that Sibyl improves upon the state of the art in nearly every case and provide evidence that it generalizes better than existing techniques. Further, we evaluate Sibyl's overhead and demonstrate that it has the potential to speedup a variety of different software engineering tools.