基于可逆性条件求解量化位向量
计算机科学中的逻辑
2018-05-15 v2
摘要
我们提出了一种基于计算位向量算子符号逆的方法，用于求解可满足性模理论（Satisfiability Modulo Theories, SMT）中的量化位向量公式的新方法。我们推导出了精确刻画位向量约束何时可逆的条件，这些条件针对 SMT 求解器普遍支持的一组具有代表性的位向量算子。我们利用语法引导的综合技术来辅助建立这些条件，并使用多个 SMT 求解器独立验证了它们。我们证明了可逆性条件可以使用 Hilbert 选择表达式嵌入到量词实例化中，并给出了实验证据表明，利用这些技术的反例引导的量词实例化方法在求解量化位向量约束方面带来了相对于 SOTA 求解器的性能提升。
引用
@article{arxiv.1804.05025,
title = {On Solving Quantified Bit-Vectors using Invertibility Conditions},
author = {Aina Niemetz and Mathias Preiner and Andrew Reynolds and Clark Barrett and Cesare Tinelli},
journal= {arXiv preprint arXiv:1804.05025},
year = {2018}
}