BriefGPT.xyz
Dec, 2020
基于SAT的Lam问题分辨
A SAT-based Resolution of Lam's Problem
HTML
PDF
Curtis Bright, Kevin K. H. Cheung, Brett Stevens, Ilias Kotsireas, Vijay Ganesh
TL;DR
本文使用布尔逻辑和可满足性（SAT）求解器来产生可由第三方验证的不存在证明，以解决Lam的问题，从而揭示了以前两个专门搜索代码的一致性问题。
Abstract
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 exi
→