论文标题
LAM问题中的重量16代码字证明
Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem
论文作者
论文摘要
在1970年代和1980年代，L。Carter，C。Lam，L。Thiel和S. Swiercz进行的搜索表明，重量为16号codeWords的订单十平面不存在。这些搜索需要高度专业化和优化的计算机程序，并且在大型机和超级计算机上需要大约2,000个小时的计算时间。在2011年，D。Roy使用优化的C程序和16,000小时的台式机对这些搜索进行了验证。我们通过将问题减少到布尔可满足性问题（SAT）来对这些搜索进行验证。我们的验证使用了Cube and-Conquer SAT解决范式，使用计算机代数系统枫木的对称性破坏技术，以及卡特的结果是，有十个非同构病例可以检查。我们的搜索在台式机上大约30小时内完成，并在DRAT（删除分辨率不对称的重言式）格式中产生了大约1 trabyte的不存在证据。
In the 1970s and 1980s, searches performed by L. Carter, C. Lam, L. Thiel, and S. Swiercz showed that projective planes of order ten with weight 16 codewords do not exist. These searches required highly specialized and optimized computer programs and required about 2,000 hours of computing time on mainframe and supermini computers. In 2011, these searches were verified by D. Roy using an optimized C program and 16,000 hours on a cluster of desktop machines. We performed a verification of these searches by reducing the problem to the Boolean satisfiability problem (SAT). Our verification uses the cube-and-conquer SAT solving paradigm, symmetry breaking techniques using the computer algebra system Maple, and a result of Carter that there are ten nonisomorphic cases to check. Our searches completed in about 30 hours on a desktop machine and produced nonexistence proofs of about 1 terabyte in the DRAT (deletion resolution asymmetric tautology) format.
