半代数系统的高效求解算法及其在不等式机器证明中的应用

Solving semi-algebraic system is an important theoretical problem in mathematics, which includes a series of problems concerning the real solutions of semi-algebraic systems. It also has many applications to a great deal of research fields. Existing methods for solving semi-algebraic systems all have to face the bottleneck of high computational complexity. The scale of problems which can be solved by existing symbolic methods being not big strongly limits the applications of those methods. Therefore, it is an urgent need to improve existing algorithms or to design new and efficient ones. This is just the key target of this proposal. The expected deliverables of this project include the following: 1. new and efficient algorithms for triangular decomposition of semi-algebraic systems; 2. new and efficient algorithms for real solution classification of parametric semi-algebraic systems; 3. new and efficient algorithms for real solution isolation of constant semi-algebraic systems; and 4. special algorithms for some special classes of problems with concrete backgrounds, especially those originating from the field of automated inequality proving and discovering. The contributions of this research project may offer benifits to the theory, the algorithms and the tools for solving semi-algebraic systems. In particular, we hope our work can facilitate the research of automated inequality proving and discovering.

半代数系统求解不是单个孤立的问题，它包含一系列关于半代数系统实解的研究问题，是数学中一个重要的理论问题，同时又有广泛的应用领域。目前半代数系统求解方法都面临计算复杂度高、能解决的问题规模有限的瓶颈，这严重阻碍了相关方法的推广和应用。因此，设计新的高效算法或改进现有算法效率、降低计算复杂度就是一个亟待研究的课题，也是本项目的核心研究目标。在该问题的研究中，我们有多年的研究积累，打下了坚实的工作基础。本项目计划围绕半代数系统的高效三角分解、半代数系统实解分类和实解隔离的高效算法研究以及以应用问题为背景的不等式机器证明问题类的提取和针对性的高效算法设计等四个有紧密逻辑联系的主要研究内容，对半代数系统的一系列求解问题开展更系统深入的研究，以期丰富和发展半代数系统求解理论、算法和工具，提高算法效率，解决一些过去难以解决的规模较大的问题，拓展我们方法的应用领域。特别地，希望能促进不等式机器证明的研究。

本项目主要研究半代数系统（包括一般的系统和具有不同问题背景的特殊系统）的高效求解算法。对一般的半代数系统，我们研究参数系统的三角分解和常系数系统的实解隔离；我们重点研究了三类特殊半代数系统，它们分别来自不等式机器证明、混成系统验证和生物系统稳定性分析。主要成果概述如下：.1. 对著名的柱形代数分解算法（Cylindrical Algebraic Decomposition, CAD）提出了两种改进算法，可以在证明多项式不等式时，缩小投影算子的规模并大幅减少样本点的数目，从而极大地提高效率。CAD领域的国际权威专家认为我们的方法是对CAD投影算子的重要改进；.2. 在混成系统验证中，提出了可以构造非线性Craig interpolant和barrier certificate的高效算法，而目前这方面的研究基本上还只能处理线性情形；在线性系统可达性判定问题上，给出了目前最广一类系统的判定性结果；.3. 针对一类生物系统的稳定性分析，给出了全新的高效算法，比已知的符号算法效率高得多；.4. 改进了基于半定规划（SDP）的平方和（SOS）分解算法，对两类SOS多项式，可以将原来的问题等价地简化为几个规模较小的问题，极大地提高了此类算法的效率和结果的可靠性；.5. 定义了包括不稳定簇（RDU）在内的一系列新概念，提出了弱相对单纯分解（WRSD）算法等一系列新算法，严格证明了所有算法的正确性，从而建立了完整的用分层策略求解一般参数系统的理论。.6. 对常系数多项式系统，给出了一种基于数值和符号混合计算策略的实根隔离算法。大量实验结果表明，除个别规模很小的系统外，我们的新方法要远优于之前的实根隔离的符号算法。.上述算法都已实现为程序，比较成熟的几个软件包可以通过网络下载，部分算法集成在著名数学软件Maple之中。.发表8篇SCI期刊论文，6篇EI会议论文，出版1本英文专著，其中5篇JSC（符号计算领域最权威的杂志，CCF分区B，CORE分区A）；1篇ISSAC（符号计算领域最权威的会议，CORE分区A*）；1篇CAV（程序验证领域最权威的会议之一，CCF分区A，CORE分区A*）；1篇IJCAR（自动推理领域最权威的会议之一，CCF分区B，CORE分区A*）。