带等式约束的圆柱代数分解
摘要：圆柱代数分解（CAD）长期以来一直是符号计算中最重要的算法之一，作为在实数上执行一阶逻辑量词消除的工具。最近，它在可满足性检测领域中越来越受重视，作为在非线性实数算术问题中识别满足解的工具。 原始算法根据多项式的符号产生分解，而通常需要的是根据包含这些多项式的公式的真值进行分解。实现这种更粗糙（但希望更便宜）分解的一种方法是将CAD中识别的多项式转化为反映逻辑结构的多项式，从而降低解空间维度：等式约束（ECs）的存在。 本文可以作为使用带有ECs的CAD的教程：我们描述了所有必要的背景和当前的最新技术水平。特别是，我们介绍了如何利用McCallum的简化投影理论在提升阶段进一步节省成本的最新工作：包括我们提升的多项式和提升到的单元格。我们给出了一个新的复杂性分析，以证明CAD的最坏情况复杂性界限的双指数与ECs的数量相对应地降低。我们展示了这种减少可以适用于产生的多项式的数量和它们的次数。
作者：Matthew England, Russell Bradford and James H. Davenport
论文ID：1903.08999
分类：Symbolic Computation
分类简称：cs.SC
提交时间：2020-03-23