公平且进取的量化符实例化枚举
人工智能
2021-05-31 v1
摘要
SMT 求解器通常通过用公式中基元部分的项元组实例化量化符变量来处理量化符。近期的量化符实例化枚举方法按某种启发式顺序考虑项元组。本文研究了对这些元组排序的不同策略及其对性能的影响。我们将排序问题解耦为两部分：首先是每个量化变量所考虑项序列的顺序，其次是实例化元组自身的顺序。尽管最偏好与最不偏好的元组（即所有变量都被赋予最偏好或最不偏好项的元组）是明确的，但其间组合在实现中允许灵活性。我们考察了完全枚举的原则性策略，其中某些策略更公平（即同等对待所有变量），而某些策略可能更进取（即更敢于沿偏好列表向下探索）。我们进一步描述了丢弃无关实例化的新技术，这些技术对实践中这些策略的性能至关重要。这些策略已在 SMT 求解器 cvc5 中实现，正如我们的实验结果所示，它们有助于求解器配置空间的多样化。
引用
@article{arxiv.2105.13700,
title = {Fair and Adventurous Enumeration of Quantifier Instantiations},
author = {Mikoláš Janota and Haniel Barbosa and Pascal Fontaine and Andrew Reynolds},
journal= {arXiv preprint arXiv:2105.13700},
year = {2021}
}