论文标题
使用圆柱代数覆盖物通过冲突驱动的搜索来确定非线性真实算术约束的一致性
Deciding the Consistency of Non-Linear Real Arithmetic Constraints with a Conflict Driven Search Using Cylindrical Algebraic Coverings
论文作者
论文摘要
我们提出了一种新算法，用于确定对真实的非线性多项式约束的结合的满意度，该算法可以用作可满足性模量理论（SMT）求解非线性真实算术的理论求解器。该算法是适合满足性的圆柱代数分解（CAD）的变体，在逐步构建解决方案（样品点）的情况下，直到找到令人满意的样品或已采样了足够的样品以确定难以满足。样本的选择以输入约束和以前的冲突为指导。 我们新方法背后的关键思想是从部分样本开始。证明它不能扩展到完整的样本；从原因的原因来看，部分样品周围有一个更大的空间，这些空间会逐渐累积到空间的圆柱代数覆盖中。与CAD的增量变体，Jovanovic和de Moura的NLSAT方法以及Brown的核A算法相似。但是我们介绍了有关初步实施的工作示例和实验结果，以证明这些差异以及新方法的好处。
We present a new algorithm for determining the satisfiability of conjunctions of non-linear polynomial constraints over the reals, which can be used as a theory solver for satisfiability modulo theory (SMT) solving for non-linear real arithmetic. The algorithm is a variant of Cylindrical Algebraic Decomposition (CAD) adapted for satisfiability, where solution candidates (sample points) are constructed incrementally, either until a satisfying sample is found or sufficient samples have been sampled to conclude unsatisfiability. The choice of samples is guided by the input constraints and previous conflicts. The key idea behind our new approach is to start with a partial sample; demonstrate that it cannot be extended to a full sample; and from the reasons for that rule out a larger space around the partial sample, which build up incrementally into a cylindrical algebraic covering of the space. There are similarities with the incremental variant of CAD, the NLSAT method of Jovanovic and de Moura, and the NuCAD algorithm of Brown; but we present worked examples and experimental results on a preliminary implementation to demonstrate the differences to these, and the benefits of the new approach.
