自动推理技术破解百年几何难题

某中心学者Marijn Heule与柏林工业大学同事Manfred Scheucher共同解决了匈牙利-澳大利亚数学家Esther Szekeres近100年前提出的几何问题。这位某机构学者兼卡内基梅隆大学计算机科学教授采用自动推理工具SAT求解器成功证明了空六边形问题的解。

百年数学难题的突破

该问题被传奇数学家Paul Erdős称为"幸福结局问题"，要求确定平面上需要多少个点（任意三点不共线）才能保证其中n个点构成不包含其他点的凸多边形。Esther Szekeres在1930年代解决了n=4的情况，Heiko Harborth在50年后确定需要10个点来保证空五边形存在，而Joseph Horton同期证明七边及以上多边形无解。空六边形问题一直悬而未决，直到Heule和Scheucher证明30个点足以保证存在不包含其他点的凸六边形。

自动推理技术的创新应用

为了证明这一结果，研究人员使用SAT求解器——一种能判断长逻辑约束链是否可满足的自动推理工具。SAT求解器生成关于变量赋值的证明，而验证证明正确性需要另一个自动推理工具：证明检查器。

证明可能达到数百TB规模，证明检查过程中的输入输出（I/O）和数据检索极其耗时。Heule表示：“检查成本可能达到原始求解时间的100%到200%。“作为某机构自动推理组成员，Heule与同事开发了新的流式证明检查基础设施，通过专用服务器核心在证明生成时实时检查，将证明检查开销从100%-200%降低到约10%。

技术实现细节

SAT问题是NP完全的，意味着存在宇宙寿命内所有计算机都无法解决的SAT问题。但并非所有SAT问题都无解，自动推理研究者的艺术在于如何将问题表述为SAT求解器可解决的形式。

幸福结局问题可以使用二元变量描述三点方向关系。每个变量具有相同形式：给定三个不共线点A、B、C，C位于通过A和B的直线上方（如果变量为假，C必然在下方）。通过连接足够多这样的关系，可以指定六边形情况的30个点（或29个点等其他数量）。

在此框架下，难点在于描述存在至少一个内部无点的六边形的条件。Scheucher团队多年来一直未能找到SAT求解器可处理的表述方式，这正是Heule的贡献所在。

问题简化的关键洞察

处理空六边形问题的自然方法是将六边形分解为三角形并推理每个三角形内部是否包含点。先前尝试采用通用方法，指定可应用于集合中任何三角形和包含该三角形的所有六边形的逻辑约束。Heule表示，这种表达式易于制定但难以推理。

Heule建议采用相反方法：明确标记每个六边形的所有可能配置，使用这些标签指定各个三角形，并检查每个命名三角形内部是否包含点。

SAT求解器通过寻找逻辑冗余并移除它们来降低问题复杂性。在空六边形问题的初始规范中，Heule将点集中的每个六边形分为四个三角形并检查每个三角形内部是否包含点。然而，他注意到SAT求解器将此步骤简化为每个六边形只检查一个三角形。

通过深入思考，Heule和Scheucher意识到每个六边形中存在一个内三角形，与六边形的其他三个外三角形共享所有边。如果这个内三角形为空，则可以从点集中推导出空六边形的存在。

技术应用的广泛前景

这项创新将对自动推理组未来在软件安全、可证明正确软件和硬件验证等方面的工作产生重要影响。当然，这些应用仍然需要开发人员创建严格的系统形式化模型。但在证明检查阶段，“如果能够以10%的开销而不是150%完成工作，这显然是重大胜利，“Heule表示。

Heule经常看到求解器提供有用反馈，尽管这是针对专家的反馈。他认为让非专家也能获得这种反馈非常重要。例如，用户实现某些功能时，求解器可以说"你试图这样做，但表达式的这部分不需要”。这种反馈可用于重新表述表达式，使其更容易解决。

一旦理解求解器的反馈，研究人员就能设计更实用的SAT问题规范。求解器能够推理30点集的所有可能性，并证明在该集合中必须存在至少一个内三角形不包含其他点的六边形。

这仍然是一个极其漫长的证明，但Heule及其同事的新证明检查机制能够相对快速地确认其有效性。

Heule指出：“其中一个问题是许多工具用户不知道如何充分发挥这些工具的潜力。这不仅适用于这个特定问题，也适用于许多其他问题。在某机构内部，存在许多SAT求解器可以验证开发人员工作或找到更好解决方案的应用场景。我可以通过编写有效的编码来提供帮助，但理想情况下，所有工作都应该自动完成。我希望看到自己从这个等式中被取代。”