# Local Search for Fast Matrix Multiplication

## TL;DR

This paper introduces two SAT-based local search methods to discover new matrix multiplication schemes, significantly expanding the known solutions and demonstrating the effectiveness of local search over traditional SAT solvers.

## Contribution

The paper presents novel SAT-based local search techniques for finding matrix multiplication schemes, increasing the number of known solutions and advancing computational methods in this area.

## Key findings

- Local search SAT solvers outperform CDCL solvers in this task.
- Hundreds of new schemes found individually, thousands combined.
- Methods significantly expand the known space of matrix multiplication schemes.

## Abstract

Laderman discovered a scheme for computing the product of two 3x3 matrices using only 23 multiplications in 1976. Since then, some more such schemes were proposed, but it remains open how many there are and whether there exist schemes with fewer than 23 multiplications. In this paper we present two independent SAT-based methods for finding new schemes. Both methods allow computing a few hundred new schemes individually, and many thousands when combined. Local search SAT solvers outperform CDCL solvers consistently in this application.