Thomson问题的机械化算法研究

It is an important subfield of machine proof of theorems that to find out the optimal solution in the set of feasible solution of combinational problem with discrete variables by computers, including the construction of mechanization algorithms during solving process. The famous Thomson problem is such a cominational geometry problem with a profound background of physics. The main diffculty of the problem is that the rapidly increasing of computational complexity with n increasing which will easily exceed the computer processing capacity. We are focusing our research on the solution of Thomson's Problem: the optimal distribution and the upper bound of maximal distance sum of n (n<=16) spherical points by using the method such as rectangular division, symbolic-numeric hybrid computation of numeric computation with controllable error and GPU prallel computation. We will also research Erdos-Szekeres problem following the similar pattern. The research of these problems not only have the good forwardness and important theoretical significance, but also have a good application prospect.

利用计算机在含离散变量的组合问题的可行解集中找出最优解，特别是求解过程中的机械化算法构建，早已成为定理机器证明的一个重要分支。著名的Thomson问题是一个具有深厚物理学背景的组合几何问题。其主要难点在于随着球面点数的增大，计算复杂度将迅速增长从而超出计算机的处理能力。本项目的主要研究内容有：利用矩形区域剖分法、误差可控的符号数值混合计算、GPU并行运算等方法建立通用的机械化算法求解Thomson问题中球面n点(n≤16)最优分布模型及距离的最大和上界，并适当探索Erdos-Szekeres问题的机械化解法。这些研究不仅具有很好的前沿性和较重要的理论意义，而且有着很好的应用前景。

本项目以Thomson问题低维情形等若干有难度组合优化问题为切入点，致力于对数学机械化算法的研究。该方向正是人工智能中的符号推理与定理机器证明方向的具体体现，利用计算机和基于符号计算高效算法在含有离散变量的组合问题可行解集中找出最优解，亦是属于数学和计算机科学交叉的前沿领域。三年内，我们的研究内容主要包括对Thomson问题的球面n点(n为奇素数)最优分布模型及距离最大和的上界不等式的研究；以及对基于符号数值混合算法的大间距离散不规则样本重建算法和其实际应用；同时也对研究过程中的一些核心不等式如离散高阶Wirtinger型不等式的逆形式和离散Holder型不等式的逆形式进行了推广和探索。. 我们主要取得的成果则包括：(1)建立了基于球极投影坐标、Wirtinger不等式范数逼近、区域剖分法等技术手段的机械化算法，在计算过程中对中间结式消元采用了误差可控的符号数值混合计算，有效消解了中间过程膨胀问题，较好地解决了Thomson 问题中m = 3，n = 7， λ = 1的情形，验证了球面上7点距离和最大时的最优分布模型。(2)提出了基于牛顿-龙格插值法的数值插值检验法和基于笛卡尔符号法则与Dixon结式的零点隔离法,对高次大多项式进行数值逼近,并由误差值对精确值进行确定.之后由柱型代数分解法对高次不等式组进行证明，由此确定了球面点间两两距离和的上界。(3)将符号数值混合插值逼近法运用到了电能大数据分析建模领域,建立了基于大间距样本重建的电能传输质量评估体系,此成果和合作者获得2017年上海市科技成果三等奖。本项目研究过程中得到的算法和其收敛性、终止性研究在信号分析、编码理论、数据可视化等众多领域中都有着广泛和深远的应用前景。