十阶射影平面不存在性证书：基于权 15 码字的情形
离散数学
2020-04-17 v2 计算机科学中的逻辑
符号计算
组合数学
摘要
利用符号计算与可满足性检查领域的技术，我们验证了用于证明十阶射影平面不存在这一里程碑结果中所用的一个情形。具体而言，我们证明不存在生成权十五码字的十阶射影平面，该结果最初于 1973 年通过穷举计算机搜索得出。我们提供了一个简单的可满足性（SAT）实例及不可满足性证书，可首次用于自动验证此结果。此前所有对该结果的演示都依赖于难以或无法验证的搜索程序——事实上，我们的搜索发现了因先前未发现的缺陷而被以往搜索遗漏的部分射影平面。此外，我们展示了通过借助计算机代数系统（CAS）的功能可大幅提升 SAT 求解器的性能。我们的 SAT+CAS 搜索比所有其他已发表的验证该结果的搜索显著更快。
引用
@article{arxiv.1911.04032,
title = {A Nonexistence Certificate for Projective Planes of Order Ten with Weight 15 Codewords},
author = {Curtis Bright and Kevin Cheung and Brett Stevens and Dominique Roy and Ilias Kotsireas and Vijay Ganesh},
journal= {arXiv preprint arXiv:1911.04032},
year = {2020}
}
备注
To appear in Applicable Algebra in Engineering, Communication and Computing