Unsatisfiability Proofs for Weight 16 Codewords in Lam's Problem
Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence
Main track. Pages 1460-1466. https://doi.org/10.24963/ijcai.2020/203
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 2010, 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.
Heuristic Search and Game Playing: Combinatorial Search and Optimisation
Constraints and SAT: SAT: : Solvers and Applications
Constraints and SAT: SAT: Algorithms and Techniques
Constraints and SAT: Constraint Satisfaction