200 Terabyte Proof Demonstrates the Potential of Brute-Force Math

Michael Byrne:

In computer science, the “brute force” solution is usually the suboptimal solution. It gets there eventually, but also inefficiently and without cleverness. The existence of a brute force solution to a problem usually implies the existence of a more elegant but perhaps less obvious solution.

You could take a basic algebra problem as an example: 2x + 100 = 500. To solve this with brute force, we simply check every possible value of x until one works. We know, however, that it is far more efficient to rearrange the given equation using algebraic rules and in just two computations we get an answer.

Computer scientists are giving brute force another look, however. In a paper published in the current Communications of the ACM, Marijn Heule and Oliver Kullmann argue that we’re entering a new era where brute force may have a key role to play after all, particularly when it comes to security- and safety-critical systems. This is thanks to a newish technology called Satisfiability (SAT) solving, which is a method of generating proofs in propositional logic.