论文标题
通过解决SAT解决Zarankiewicz问题的攻击
An attack on Zarankiewicz's problem through SAT solving
论文作者
论文摘要
Zarankiewicz函数可为选择的矩阵和次要尺寸提供二进制矩阵中最大数量的函数。已经编译了有关小参数的此功能的表，但是其中已知错误。在平方未成年人的情况下，我们既纠正错误又扩展了这些表，并表达了在特定点找到值的问题，该问题是一系列布尔可满足性问题，从而利用了置换对称性，从而大大降低了所需的工作。当环境矩阵也是正方形时，我们还给出了达到最大矩阵的所有非晶状体示例，直至上述对称性。发现大多数最大矩阵具有某种形式的对称性。
The Zarankiewicz function gives, for a chosen matrix and minor size, the maximum number of ones in a binary matrix not containing an all-one minor. Tables of this function for small arguments have been compiled, but errors are known in them. We both correct the errors and extend these tables in the case of square minors by expressing the problem of finding the value at a specific point as a series of Boolean satisfiability problems, exploiting permutation symmetries for a significant reduction in the work needed. When the ambient matrix is also square we also give all non-isomorphic examples of matrices attaining the maximum, up to the aforementioned symmetries; it is found that most maximal matrices have some form of symmetry.
