论文标题
椭圆形的不存在证书，在订单十的投影平面
Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
论文作者
论文摘要
1983年，在订单十的投影平面上对椭圆形进行了计算机搜索。搜索是详尽而负面的，这意味着这种椭圆形不存在。但是，此搜索没有生成不存在的证书，据我们所知，搜索从未得到独立验证。在本文中，我们在订单十的投影平面上重新搜索椭圆形，并产生一系列非持有证书，这些证书在一起，这意味着不存在这种椭圆形。我们的搜索程序使用来自满意度（SAT）检查领域（SAT）检查的立方体和搜索范式，并与程序化的SAT求解器和Nauty Symbolic Computation库一起从搜索中删除对称性。
In 1983, a computer search was performed for ovals in a projective plane of order ten. The search was exhaustive and negative, implying that such ovals do not exist. However, no nonexistence certificates were produced by this search, and to the best of our knowledge the search has never been independently verified. In this paper, we rerun the search for ovals in a projective plane of order ten and produce a collection of nonexistence certificates that, when taken together, imply that such ovals do not exist. Our search program uses the cube-and-conquer paradigm from the field of satisfiability (SAT) checking, coupled with a programmatic SAT solver and the nauty symbolic computation library for removing symmetries from the search.
