  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.
