Ruling Out Low-rank Matrix Multiplication Tensor Decompositions with Symmetries via SAT
Jason Yang
TL;DR
The paper tackles exact rank decompositions of the $3\times3$ matrix multiplication tensor over GF(2), targeting rank at most $21$ to surpass Strassen style asymptotics. It develops a SAT based framework that encodes tensor decompositions with heavy symmetry reductions, including cyclic, cyclic plus transpose, and cyclic plus involute-sandwich symmetries, and uses Z3 to certify nonexistence for several symmetry classes. The main findings demonstrate that there are no $\le 21$ rank decompositions with the examined symmetries, and that certain symmetry constraints sharply limit the existence of faster algorithms in these restricted classes, while also offering a canonicalization approach to avoid rank redundancy. The work guides future exploration by suggesting sparsity based constraints, stronger canonical forms, and examination of additional symmetry groups to further narrow the landscape of explicit small tensor decompositions with potential algorithmic implications.
Abstract
We analyze rank decompositions of the $3\times 3$ matrix multiplication tensor over $\mathbb{Z}/2\mathbb{Z}$. We restrict our attention to decompositions of rank $\le 21$, as only those decompositions will yield an asymptotically faster algorithm for matrix multiplication than Strassen's algorithm. To reduce search space, we also require decompositions to have certain symmetries. Using Boolean SAT solvers, we show that under certain symmetries, such decompositions do not exist.