若干组合几何全局优化问题的机械化算法

In this project we will study the fundamental theory and new algorithms for the mechanization of combinational geometry including the algebraic representation methods of the convexity and metric properties of finite sets, and the efficient implementation of the algorithms via symbolic-numerical hybrid computation on parallel machines for certain unsolved global optimization problems. The research will focus on the investigation for innovative methods for constructing neighborhoods to isolating singular points and critical points, finite rectangle partition of compact polytopes, and semi-algebraic sets based on metric equations, as well as extension of message passing interface to describe searching paths and calculating processes, dynamic task redistribution supporting load balance strategies, and real-time re-organizing of computing nodes cluster computers for sub-tasks that form simplicial complex topological structures in parallel symbolic computation. To ensure the wide applicability of the theory and the substantial performance of the algorithms in the research, we will target on specified difficult classical open combinatorial optimization problems and devote to establishing new methods of formal substitutions in searching in large state spaces and in expansion of very large objects to reduce the intermediate of symbolic computation, the early terminations techniques in GPU-based numeric interpolation, error analysis and symbolic expression recovering via certified and reliable approximate numerical computation. The research results will not only contribute new approaches to mathematics mechanization, but also provide valuable experience on using of parallel symbolic computation with cluster computers to many other fields.

组合几何定理的机械化证明需要构造联系离散点集合的度量性质和凸性等组合性质的代数化表示, 其中的全局最优化问题还涉及大量空间复杂度极高的符号计算问题. 本项目围绕若干有代表性的问题, 探索有创造性的方法, 包括基于度量方程的代数化, 奇点隔离, 矩形剖分等算法; 研究这些算法在并行和GPU计算设备上的有效实现方法,包括带计算过程和搜索路径的消息传递扩展方法、支持动态任务分配的负载均衡策略、单纯复合形网络拓扑上的计算节点小组重组技术等; 研究组合搜索和复杂结式计算中出现的中间过程膨胀压缩等大数据处理方法, 试验形式代换、数值插值、模运算、用可控制误差的近似计算替代符号计算等新方法. 通过本项目研究逐步建立组合几何机械化的理论和算法基础，不仅有希望得到一些困难的组合几何公开问题, 还可为其他专门方向的数学机械化研究提供在并行/GPU计算机上利用并行符号计算的一些有效的参考经验.

本项目研究了一类组合几何全局最优化问题的机械化求解算法及其实现方法. 这类组合几何优化问题, 包含较多的几何不变量之间的等式和不等式约束条件, 转化为代数问题之后, 由于计算复杂度高的限制, 以及求解的目标是无计算误差的证明, 不能直接用现有的优化方法和现有的计算机软件解决. 为此, 本项目以几个具体的、以前未解决的组合几何全局最优化问题为切入研究对象, 探讨了基于度量方程的代数化表示、奇点隔离、矩形剖分、符号数值混合计算、并行计算等方法在全局最优化机械化求解中的应用，一方面解决了若干有影响和难度的公开问题，包括正方形内9点Heilbronn分布、球面上欧氏度量意义下的Fermat-Torricelli点构造、Vasc不等式猜想、平面上经过给定小正方形区域的最小多项式的最低次数以及有限点集距离空间的若相容分割距离分解快速计算等问题，另一方面建立了隐函数方程插值、稀疏插值、基于Dixon结式的多元结式消元方法、基于概率的算法等处理复杂计算问题的符号-数值计算新方法，并且在共享内存集群计算机、带通用图形处理器(GPGPU)等不同架构的并行计算机上具体实现了这些方法。项目还研究了超几何函数的化简计算和凸体混合体积的估计问题，设计了Ramsey问题机械化证明、置换群Cayley图直径计算等组合数学的代数方程表示方法，通过研究多元稀疏插值，发现了关于分拆数p(n)的渐近表达式的一个新的猜测，改进了Hardy-Ramanujan的经典结果。此外，还将项目中建立的方法用于不变式生成、程序安全性验证等应用问题的研究。在期刊和国际会议发表论文20余篇，国内外报告论文10余篇。约10篇已完成尚未发表。项目培养毕业博士研究生4名、硕士研究生5名，在读研究生14名。项目显著促进了与国内外同行之间的学术交流。项目获得的结果将推动组合数学机械化研究，有望在人工智能领域与组合、优化有关的算法设计中得到应用。