基于SAT的Lam问题求解
A SAT-based Resolution of Lam's Problem
AI总结：
本文通过将Lam问题转化为布尔逻辑并用SAT求解器生成可验证的不存在性证书，解决了十阶射影平面存在性问题，同时揭示此前专用搜索代码的一致性问题。
摘要：
1989年，Lam、Thiel和Swiercz的计算机搜索实验性地解决了来自射影几何的Lam问题——这一长期悬而未决的问题，即确定是否存在十阶射影平面。原始搜索和2011年的独立验证均未发现此类射影平面。然而，这些搜索均使用高度专门化的定制代码执行，且未生成不存在性证书。在本文中，我们通过将问题转化为布尔逻辑并使用可满足性（SAT）求解器来生成可由第三方验证的不存在性证书，从而解决了Lam问题。我们的工作揭示了此前两次搜索中的一致性问题——凸显了依赖专用搜索代码来获得不存在性结果的困难。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
