权为15码字的十阶射影平面不存在性证明
A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords
摘要：
使用技术领域的符号计算和可满足性检查，我们验证的情况下使用的地标结果，十阶投影平面不存在。特别是，我们表明，不存在投影平面的顺序10，产生码字的重量15，结果首先显示在1973年通过一个详尽的计算机搜索。我们提供了一个简单的可满足性（SAT）实例和一个不可满足性证书，可用于首次自动验证此结果。之前所有关于这一结果的演示都依赖于难以或不可能验证的搜索程序-事实上，我们的搜索发现了部分投影平面，这些平面由于之前未发现的错误而被之前的搜索所遗漏。此外，我们展示了如何SAT求解器的性能可以显着增加采用功能从计算机代数系统（CAS）。我们的SAT+CAS搜索运行速度明显快于所有其他已发布的验证此结果的搜索。
英文摘要：
Using techniques from the fields of symbolic computation and satisfiability checking we verify one of the cases used in the landmark result that projective planes of order ten do not exist. In particular, we show that there exist no projective planes of order ten that generate codewords of weight fifteen, a result first shown in 1973 via an exhaustive computer search. We provide a simple satisfiability (SAT) instance and a certificate of unsatisfiability that can be used to automatically verify this result for the first time. All previous demonstrations of this result have relied on search programs that are difficult or impossible to verify---in fact, our search found partial projective planes that were missed by previous searches due to previously undiscovered bugs. Furthermore, we show how the performance of the SAT solver can be dramatically increased by employing functionality from a computer algebra system (CAS). Our SAT+CAS search runs significantly faster than all other published searches verifying this result.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
