论文标题
通过样品细胞投影解决多项式公式的满意度
Solving Satisfiability of Polynomial Formulas By Sample-Cell Projection
论文作者
论文摘要
提出了一种决定多项式公式对真实公式的满意度的新算法。该算法的关键点是一个新的投影操作符，称为样本细胞投影操作员，用于冲突驱动的子句学习（CDCL）式搜索的定制制造。尽管新运算符也是类似于给定样品的细胞（不一定是圆柱形）的类似投影算子的CAD（圆柱代数分解），其类似的投影算子，因此，来自问题的每个多项式都在细胞上签名，但它具有单一的Expeffiend Time Expultigation Time复杂性。样品细胞投影运算符可以有效地指导CDCL风格的搜索，从冲突状态下。实验显示了新算法的有效性。
A new algorithm for deciding the satisfiability of polynomial formulas over the reals is proposed. The key point of the algorithm is a new projection operator, called sample-cell projection operator, custom-made for Conflict-Driven Clause Learning (CDCL)-style search. Although the new operator is also a CAD (Cylindrical Algebraic Decomposition)-like projection operator which computes the cell (not necessarily cylindrical) containing a given sample such that each polynomial from the problem is sign-invariant on the cell, it is of singly exponential time complexity. The sample-cell projection operator can efficiently guide CDCL-style search away from conflicting states. Experiments show the effectiveness of the new algorithm.
