我的阅读状态 （保存写回仓库，全设备同步；首次保存需输入访问令牌）

AI 速览

一句话：提出基于最近邻分类与运行时估计的在线 SMT 求解器选择方法，实现 MedleySolver，选择近乎最优且求解快三倍。

SMT 求解器种类繁多且性能互补，对给定查询挑选合适的求解器或算法是提升效率的关键问题。本文提出一种在线的 SMT 求解器选择方法，利用最近邻分类预测查询应交给哪个求解器，并结合运行时估计来做出决策，从而避免离线训练成本并适应查询分布。作者将该方法实现为 MedleySolver 工具，并在查询数据集上进行评估。实验表明，该方法做出的选择接近理论最优，且整体求解数据集的速度约为任何单一求解器的三倍，说明动态、按查询选择算法能显著优于固定的单一求解器策略。

问题

面对性能互补的众多 SMT 求解器，如何针对每个查询动态选择最合适的求解器或算法，以避免单一求解器在某些查询上的性能劣势。

方法

提出在线选择方法，结合最近邻分类与运行时估计来预测并选择求解器，并实现为 MedleySolver。

评估

在查询数据集上评估 MedleySolver，结果显示其选择近乎最优，且求解数据集的速度约为任何单一求解器的三倍。

链接与引用

DOI 原文 · PDF（开放获取） ·

@inproceedings{paperbot5873,
  title = {Dynamic algorithm selection for SMT},
  author = {Nikhil Pimpalkhare},
  booktitle = {ASE},
  year = {2020},
  doi = {10.1145/3324884.3418922}
}