一句话：提出并评估四类 SMT 元求解策略，以在性能、准确性与成本间取得平衡。
现代软件工程工具依赖 SMT 求解器的准确性与性能。本文提出四种组合约束求解器的基本模式：最早结论、多数投票、基于特征的求解器选择、基于结论的二次尝试，用于构建平衡准确率、性能和成本的元决策过程。作者分析并最小化 16 个基准套件，在 1.7 万个唯一实例上评测七个先进 SMT 求解器，基于性能数据估计不同元求解策略的效果，并实现分析两种策略进行验证。额外产出包括首个带验证期望结论的唯一 SMT 字符串问题基准套件、包含实例与求解器/元策略性能的数据集，以及便于生成数据以支持类似分析的框架。
Many modern software engineering tools integrate SMT decision procedures and rely on the accuracy and performance of SMT solvers. We describe four basic patterns for integrating constraint solvers (earliest verdict, majority vote, feature-based solver selection, and verdict-based second attempt) that can be used for combining individual solvers into meta-decision procedures that balance accuracy, performance, and cost – or optimize for one of these metrics. In order to evaluate the effectiveness of meta-solving, we analyze and minimize 16 existing benchmark suites and benchmark seven state-of-the-art SMT solvers on 17k unique instances. From the obtained performance data, we can estimate the performance of different meta-solving strategies. We validate our results by implementing and analyzing two strategies. As additional results, we obtain (a) the first benchmark suite of unique SMT string problems with validated expected verdicts, (b) an extensive dataset containing data on benchmark instances as well as on the performance of individual decision procedures and several meta-solving strategies on these instances, and (c) a framework for generating data that can easily be used for similar analyses on different benchmark instances or for different decision procedures.
DOI 原文 ·
@inproceedings{paperbot6585,
title = {Data-Driven Design and Evaluation of SMT Meta-Solving Strategies: Balancing Performance, Accuracy, and Cost},
author = {Malte Mues and Falk Howar},
booktitle = {ASE},
year = {2021},
doi = {10.1109/ase51524.2021.9678881}
}