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”来代替。量词“there exists”和变量x被删除了。要点是：（a）结果可以由计算机使用QE从原始语句自动导出;（B）QE揭示了人类经常忽略的a=0的特殊情况！量化宽松问题的解决方案不是数字，而是提供洞察力的代数描述。在上面的例子中，量化宽松并没有提供特定方程的解--它一般地告诉我们解的数量如何取决于（a，B，c）。量化宽松使隐藏的数学结构变得清晰：它是一种“简化”甚至“解决”数学问题的方法。对于真实的数上的多项式中的语句，总是存在一个没有量化的等价公式。然而，实际上获得答案在计算方面可能非常昂贵，并且这些成本随着问题的大小而增加。我们称之为“双指数墙”，指的是它们上升的速度。双指数意味着与幂的幂次方成正比，例如，一个大小为n的问题的成本约为2^（2^n）。在实践中应用量化宽松时，小问题的结果可能很容易找到，但随着规模的增加，你不可避免地会遇到计算永远无法完成的障碍。双指数墙无法完全打破：成本的上升是不可避免的。然而，这个项目的目的是“推倒墙”，以便量化宽松可以解决更多的实际问题。这里的规模意味着，即使是很小的方式推动墙提供了巨大的潜力：例如，2^（2^4）是小于66，000，而2^（2^5）是超过40亿！我们将通过开发新的算法来实现这一目标，这些算法受到现有过程（圆柱代数分解）的启发，但具有实质性的创新。第一个创新是一个新的计算路径的灵感来自于计算机科学的另一个领域（可满足性检查），它已经推回了另一个著名的难题（布尔可满足性）。该团队是一个新的知识交流社区的创始成员。第二个创新是发展了一种新的数学形式主义的基础代数理论，使它可以利用结构的逻辑。该小组有这种开发的经验，并由一名项目伙伴加入，他是该主题的世界专家（McCallum）。第三个创新是放松了已经存在了40多年的基础代数对象的条件。该团队与项目合作伙伴Abraham一起是一个这样的松弛（圆柱代数覆盖）的作者。QE有许多应用，也许在关键软件的验证中最重要。同样在人工智能方面：一个人工智能最近通过了美国专利。使用QE技术的东京数学入学考试。该项目将侧重于两个新兴的应用领域：（1）生物学，量化宽松可用于确定系统中参数的医学重要值;（2）经济学，量化宽松可用于验证发现，识别缺陷和探索可能性。在这两种情况下，虽然QE已经被作者证明在理论上是适用的，但目前的程序在应用于许多问题实例时会耗尽计算机时间/内存。来自这些学科的项目合作伙伴加入了我们：系统生物学的SYMBIONT和经济学家Mulligan。

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.