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

项目名称： 若干组合几何全局优化问题的机械化算法

项目编号： No.11471209

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 数理科学和化学

项目作者： 曾振柄

作者单位： 上海大学

项目金额： 72万元

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

中文关键词： 数学机械化；符号计算；组合几何；全局优化；并行计算

英文摘要： 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.

英文关键词： Mathematics mechanization;Symbolic computation;Combinatorial geometry;Global optimization;Parallel computation