真值表不变柱形代数分解
Truth Table Invariant Cylindrical Algebraic Decomposition
摘要：
当使用柱形代数分解（CAD）来解决关于一组多项式的问题时，可能不是那些多项式的符号是最重要的，而是涉及它们的某些量词自由公式的真值。这一观察激发了我们的文章和真值表不变CAD（TTICAD）的定义。在ISSAC 2013中，当前作者提出了一种算法，该算法可以有效地直接为公式列表构建TTICAD，其中每个公式都有一个等式约束。这是通过推广麦卡勒姆的理论减少投影算子。在本文中，我们提出了一个扩展版本，我们的理论，可以应用到一个任意列表的公式，实现储蓄，如果至少有一个等式约束。我们还解释了如何减少投影算子的理论可以允许进一步改进的CAD算法的提升阶段，即使在一个单一的等式约束的情况下。该算法是完全在Maple中实现的，我们从实验和复杂性分析中展示了我们的贡献的好处。
英文摘要：
When using cylindrical algebraic decomposition (CAD) to solve a problem with respect to a set of polynomials, it is likely not the signs of those polynomials that are of paramount importance but rather the truth values of certain quantifier free formulae involving them. This observation motivates our article and definition of a Truth Table Invariant CAD (TTICAD). In ISSAC 2013 the current authors presented an algorithm that can efficiently and directly construct a TTICAD for a list of formulae in which each has an equational constraint. This was achieved by generalising McCallum's theory of reduced projection operators. In this paper we present an extended version of our theory which can be applied to an arbitrary list of formulae, achieving savings if at least one has an equational constraint. We also explain how the theory of reduced projection operators can allow for further improvements to the lifting phase of CAD algorithms, even in the context of a single equational constraint. The algorithm is implemented fully in Maple and we present both promising results from experimentation and a complexity analysis showing the benefits of our contributions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
