一种SAT+CAS方法寻找优良矩阵：新实例与反例
计算机科学中的逻辑
2019-07-30 v1 符号计算
组合数学
摘要
我们枚举了所有阶数可被3整除且不超过70的奇数阶循环优良矩阵。作为其结果，我们找到了一组先前被忽略的27阶优良矩阵和一组新的57阶优良矩阵。我们还发现循环优良矩阵在51、63和69阶不存在，从而找到了三个新的反例，反驳了此类矩阵在所有奇数阶均存在的猜想。此外，我们证明了优良矩阵元素间的一种新关系，并在枚举算法中利用了该关系。我们的方法应用了SAT+CAS范式，将计算机代数功能与现代SAT求解器结合，以高效搜索由代数与逻辑约束共同指定的大空间。
引用
@article{arxiv.1811.05094,
title = {A SAT+CAS Approach to Finding Good Matrices: New Examples and Counterexamples},
author = {Curtis Bright and Dragomir Z. Djokovic and Ilias Kotsireas and Vijay Ganesh},
journal= {arXiv preprint arXiv:1811.05094},
year = {2019}
}