Pushing Back the Doubly-Exponential Wall of Cylindrical Algebraic Decomposition

如果一个语句有限定条件，如“人人都有”或“存在”，则该语句被量化。让我们考虑一个在高中数学中经常遇到的学习二次曲面的例子：“存在x，使得ax^2 bx c=0对x有两个不同的解”。这一陈述在数学上是精确的，但其含义并不清楚：这一关于存在的陈述对我们施加了什么限制？量词消除(QE)用一个等价的未量化的语句来代替这样的语句，在这种情况下是“a不是零并且b^2-4ac大于0，或者a=b=c=0的全部”。量词“存在”和变量x已被删除。其要点是：(A)结果可以由计算机使用量化宽松从原始语句自动推导出来；(B)量化宽松揭示了当a=0时人类经常遗漏的特殊情况！量化宽松问题的解决方案不是数字，而是提供洞察力的代数描述。在上面的例子中，QE没有提供特定方程的解--它通常告诉我们解的数量如何取决于(a，b，c)。量化宽松明确了隐藏的数学结构：它是一种“简化”甚至“解决”数学问题的方法。对于实数上的多项式的表述，总会存在一个没有量化的等价公式。然而，实际获得答案在计算方面可能非常昂贵，而且这些成本随着问题的大小而增加。我们称这为“双指数墙”，因为它指的是它们上升的速度。双指数意味着与幂的幂成正比，例如，一个大小为n的问题大约需要2^(2^n)。当量化宽松在实践中应用时，对于小问题可能很容易找到结果，但随着规模的增加，不可避免地会遇到计算永远不会完成的墙壁。双重指数墙不能完全打破：这种成本上升是不可避免的。不过，这项计划的目的是“推倒围墙”，让量化宽松可以解决更多实际问题。这里的规模意味着，即使是以很小的方式推墙也会带来巨大的潜力：例如，2^(2^4)不到66,000，而2^(2^5)超过40亿！我们将通过开发新的算法来实现这一点，新算法的灵感来自现有的过程(柱面代数分解)，但具有实质性的创新。第一个创新是一种新的计算路径，它受到计算机科学的另一个领域(可满足性检查)的启发，它推动了另一个著名的困难问题(布尔可满足性)的解决。这个团队是这里一个新的知识交流社区的创始成员。第二个创新是发展了一种基本代数理论的新的数学形式，以便它可以利用逻辑中的结构。该小组以前有过此类开发的经验，并有一名项目合作伙伴加入，他是这一主题的世界专家(McCallum)。第三个创新是放宽了对基本代数对象的条件，这些条件已经存在了40年。该团队与项目合作伙伴亚伯拉罕共同创作了这样一种松弛(柱面代数覆盖)。QE有许多应用，也许最关键的是在关键软件的验证中。同样在人工智能领域：一种使用量化宽松技术的人工智能最近通过了美国东京大学的数学入学考试。这个项目将集中在两个新兴的应用领域：(1)生物学，量化宽松可以用来确定系统中参数的医学上重要的值；(2)经济学，量化宽松可以用来验证发现，识别缺陷和探索可能性。在这两种情况下，尽管作者已经证明量化宽松在理论上是适用的，但目前程序在应用于许多问题实例时耗尽了计算机时间/内存。加入我们的还有来自以下学科的项目合作伙伴：来自系统生物学的共生和经济学家穆利根。

A statement is quantified if it has a qualification such as "for all" or "there exists". Let us consider an example commonly encountered in high school mathematics when studying quadratics: "there exists x such that ax^2 + bx + c = 0 has two different solutions for x". The statement is mathematically precise but the implications are unclear: what restrictions does this statement of existence force upon us? Quantifier Elimination (QE) replaces such a statement by an equivalent unquantified one, in this case by "either a is not zero and b^2 - 4ac is greater than 0, or all of a=b=c=0". The quantifier "there exists" and the variable x have been eliminated. The key points are: (a) the result may be derived automatically by a computer from the original statement using QE; (b) QE uncovers the special case when a=0 which humans often miss!Solutions to QE problems are not numbers but algebraic descriptions which offer insight. In the example above QE did not provide solutions to a particular equation - it told us in general how the number of solutions depends on (a,b,c). QE makes explicit the mathematical structure that was hidden: it is a way to "simplify" or even "solve" mathematical problems. For statements in polynomials over real numbers there will always exist an equivalent formula without the quantification. However, actually obtaining the answer can be very costly in terms of computation, and those costs rise with the size of the problem. We call this the "doubly exponential wall" in reference to how fast they rise. Doubly exponential means rising in line with the power of a power, e.g. a problem of size n costs roughly 2^(2^n). When applying QE in practice, results may be found easily for small problems, but as sizes increase you inevitably hit the wall where a computation will never finish.The doubly exponential wall cannot be broken completely: this rise in costs is inevitable. However, the aim of this project is to "push back the wall" so that lots more practical problems may be tackled by QE. The scale here means that pushing the wall even a small way offers enormous potential: e.g. 2^(2^4) is less than 66,000 while 2^(2^5) is over 4 billion! We will achieve this through the development of new algorithms, inspired by an existing process (cylindrical algebraic decomposition) but with substantial innovations. The first innovation is a new computation path inspired by another area of computer science (satisfiability checking) which has pushed back the wall of another famously hard problem (Boolean satisfiability). The team are founding members of a new community for knowledge exchange here. The second innovation is the development of a new mathematical formalisms of the underlying algebraic theory so that it can exploit structure in the logic. The team has prior experience of such developments and is joined by a project partner who is the world expert on the topic (McCallum). The third innovation is the relaxation of conditions on the underlying algebraic object that have been in place for 40+ years. The team are the authors of one such relaxation (cylindrical algebraic coverings) together with project partner Abraham.QE has numerous applications, perhaps most crucially in the verification of critical software. Also in artificial intelligence: an AI recently passed the U. Tokyo Mathematics entry exam using QE technology. This project will focus on two emerging application domains: (1) Biology, where QE can be used to determine the medically important values of parameters in a system; (2) Economics where QE can be used to validate findings, identify flaws and explore possibilities. In both cases, although QE has been shown by the authors to be applicable in theory, currently procedures run out of computer time/memory when applied to many problem instances. We are joined by project partners from these disciplines: SYMBIONT from systems biology and economist Mulligan.