利用 SAT 排除具有对称性的低秩矩阵乘法张量分解

我们分析了 $\mathbb{Z}/2\mathbb{Z}$ 上 $3\times 3$ 矩阵乘法张量的秩分解。我们将注意力限制在秩 $\le 21$ 的分解上，因为只有这些分解才能产生比 Strassen 算法渐近更快的矩阵乘法算法。为了减少搜索空间，我们还要求分解具有某些对称性。利用布尔 SAT 求解器，我们证明了在特定对称性下，此类分解不存在。