SAT Certificates for the Matrix-Multiplication Challenges over F2: All Ten `Expected-UNSAT` Instances Are Satisfiable, and a Type-3-Free Rank-23 Scheme

Imagine you are trying to solve a massive, three-dimensional jigsaw puzzle. But this isn't a picture of a sunset or a cat; it's a mathematical machine designed to multiply two grids of numbers together. In the world of computer science and math, this is called "matrix multiplication." For decades, mathematicians have been hunting for the most efficient way to build this machine. They want to know the absolute minimum number of tiny, basic building blocks (called "multiplications") needed to make the whole thing work.

Think of these building blocks as Lego bricks. For a long time, everyone knew how to build a 3x3 multiplication machine using 23 bricks. The big question was: Can we do it with just 22? To find out, researchers turned the problem into a giant logic puzzle, similar to the ones you might see in a video game or a Sudoku book, but on a scale that would make your head spin. They encoded the rules of the math into a format that computers can check, creating a "SAT" problem (which stands for "Satisfiability"). If the computer can find a way to flip all the switches to "on" without breaking any rules, the puzzle is solved. If the computer says "impossible," then maybe 22 bricks aren't enough. This paper dives into a specific set of these logic puzzles that were designed to test the limits of our current computers and our understanding of these mathematical machines.

---

The Great "Impossible" Puzzle That Wasn't

Meet Nick Palladinos, a digital detective who decided to take a fresh look at a set of ten logic puzzles that everyone else had given up on. These puzzles, known as the "Challenge 2" instances, were built by other researchers with a very specific, rigid set of rules. The creators of these puzzles believed they were "impossible" to solve. They thought the rules were so tight that no combination of 23 Lego bricks could possibly fit together to build the machine. It was like being told, "Here is a box with a lock that definitely cannot be opened," and everyone just nodded and walked away.

But Palladinos didn't just try to force the lock open with a bigger hammer. Instead, he looked at the lock itself and realized something crucial: the rules weren't as strict as everyone thought.

The puzzle creators had written the rules using "positive" instructions. They said, "You must have this specific brick here," and "You must have that brick there." But they forgot to say, "And you cannot have any other bricks touching these." It turns out, the math allows for extra bricks to be added, as long as the final machine still works correctly. The "impossible" puzzles were actually just waiting for someone to realize that the door wasn't locked; it was just that everyone was trying to fit the puzzle pieces into a box that was too small, ignoring the fact that the box could actually be a little bigger.

The Magic of Shifting and Swapping

So, how did Palladinos solve them? He used a clever trick involving "symmetry." Imagine you have a Rubik's Cube. If you twist the whole cube or rotate it, the colors move around, but the cube is still the same object. Palladinos realized that the mathematical "machine" he was building had a similar property. He could take a working solution (a set of 23 bricks that successfully multiplies matrices) and twist, rotate, or shuffle the pieces around using a special mathematical dance called the "GL(3, 2) group action."

Think of it like rearranging the furniture in a room. You can move the sofa to the left, the lamp to the right, and the rug in the middle. The room is still a room, and the furniture still works, but the layout is different. Palladinos took a known, working solution and applied these mathematical "twists" to it. Then, he used a matching game to see if these new, shuffled versions of the furniture could fit into the specific "slots" required by the tricky puzzles.

And guess what? They fit perfectly!

In fact, Palladinos didn't just find one solution; he found solutions for all ten of the puzzles that were supposed to be impossible. He proved that these "unsolvable" formulas are actually satisfiable. The computer didn't just guess; it checked every single rule. The paper confirms that for all 10 of these "Challenge 2" files, there is a valid way to arrange the 23 building blocks to make the machine work. The "impossible" label was a misunderstanding of the rules, not a true mathematical barrier.

The "Ghost" Brick and the Perfect Solution

The paper also tackled a third challenge, "Challenge 3." This one asked a different question: Can we build the machine using 23 bricks, but make sure that one specific brick is "ghostly"? In math-speak, this means one of the 23 building blocks should have a "type-3 count" of zero. This is a fancy way of saying that one of the bricks shouldn't participate in a specific, common pattern that usually appears in these machines.

Palladinos managed to do this too. He started with a working solution and performed a tiny, precise swap. He took two bricks that were doing a specific job and replaced them with two different bricks that did the exact same job but looked different. This swap was so clever that it created a "ghost" brick—one that didn't trigger the forbidden pattern at all. He proved that you can indeed build the 3x3 matrix multiplication machine with 23 bricks, where one of them is completely free of that specific pattern.

The Final Check

To make sure no one could say, "Oh, you just got lucky with the computer," Palladinos built a super-strict checker. He generated the full list of 26,541 variables (the switches) for all 21 puzzles (10 from Challenge 1, 10 from Challenge 2, and 1 from Challenge 3). He then ran a separate program that read the original puzzle rules and the new solutions, checking every single one of the 2,461,316 logical clauses.

The result? Zero failures. Every single rule was satisfied. The solutions are real, they are verified, and they are reproducible. Anyone with the right software can run the same code and get the exact same answer in about nine seconds.

What This Means (and What It Doesn't)

So, what's the big takeaway? The paper shows that the "impossible" puzzles were actually solvable all along; the rules just weren't as tight as the puzzle-makers thought. It's a reminder that in math and computer science, sometimes the hardest part isn't finding the solution, but realizing that the problem isn't as broken as it seems.

However, there's a catch. This paper solves the puzzles for a specific type of math world called "F2" (which is like a world where numbers only wrap around after 1, so 1+1=0). It does not prove that we can build a 22-brick machine. The quest for the 22-brick machine (Challenge 4) is still wide open. The paper also doesn't say that these solutions work for every kind of math you might use in the real world, like the complex numbers used in engineering. It just solves the specific logic puzzles as they were written.

But for the puzzles that were written, the verdict is clear: The "impossible" is actually possible. The door was never locked; we just needed the right key to turn the handle.