论文标题
基于SAT的LAM问题解决方案
A SAT-based Resolution of Lam's Problem
论文作者
论文摘要
1989年，Lam，Thiel和Swiercz进行的计算机搜索实验可以从投射几何形状$ \ Unicode {X2014} $确定是否存在订单十个平面的长期问题。原始搜索和2011年的独立验证都没有发现这种投影平面。但是，这些搜索均使用高度专业化的自定义代码进行，并且没有生成不存在的证书。在本文中，我们通过将问题转化为布尔逻辑并使用满意度（SAT）求解器来生成可以由第三方验证的不存在证书来解决LAM的问题。我们的工作发现了两个以前的搜索中的一致性问题$ \ unicode {x2014} $突出了依靠特殊用途搜索代码的难度不存在的结果。
In 1989, computer searches by Lam, Thiel, and Swiercz experimentally resolved Lam's problem from projective geometry$\unicode{x2014}$the long-standing problem of determining if a projective plane of order ten exists. Both the original search and an independent verification in 2011 discovered no such projective plane. However, these searches were each performed using highly specialized custom-written code and did not produce nonexistence certificates. In this paper, we resolve Lam's problem by translating the problem into Boolean logic and use satisfiability (SAT) solvers to produce nonexistence certificates that can be verified by a third party. Our work uncovered consistency issues in both previous searches$\unicode{x2014}$highlighting the difficulty of relying on special-purpose search code for nonexistence results.
