An attack on Zarankiewicz's problem through SAT solving

TL;DR

This paper corrects and extends tables of Zarankiewicz's function by formulating the problem as SAT instances, leveraging symmetries to efficiently find maximum matrices and analyze their properties.

Contribution

It introduces a SAT-based approach to compute Zarankiewicz's function, corrects previous errors, and provides a comprehensive analysis of maximal matrices with symmetries.

Findings

Corrected existing tables of Zarankiewicz's function

Extended the tables for square minors

Most maximal matrices exhibit some form of symmetry

Abstract

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.