利用柱代数覆盖的冲突驱动搜索判定非线性实算术约束的一致性
符号计算
2021-06-17 v2 计算机科学中的逻辑
摘要
我们提出一种判定实数上非线性多项式约束合取式可满足性的新算法,该算法可用作非线性实算术的满足模理论(SMT)求解的理论求解器。该算法是柱代数分解(CAD)针对可满足性问题的变体,其中解候选(样本点)被增量式构造,直到找到满足的样本或已采样足够多的样本以判定不可满足。样本的选择由输入约束和先前的冲突引导。我们新方法背后的关键思想是:从一个部分样本开始;证明它不能被扩展为完整样本;并据此将部分样本周围更大的空间排除掉,这些排除区域增量式构建成空间的柱代数覆盖。该方法与 CAD 的增量变体、Jovanovic 和 de Moura 的 NLSAT 方法以及 Brown 的 NuCAD 算法有相似之处;但我们给出了具体示例和初步实现的实验结果,以展示其与这些方法的区别以及新方法的优势。
引用
@article{arxiv.2003.05633,
title = {Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings},
author = {Erika Ábrahám and James H. Davenport and Matthew England and Gereon Kremer},
journal= {arXiv preprint arXiv:2003.05633},
year = {2021}
}