200 Terabyte Proof Demonstrates the Potential of Brute-Force Math

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. Basically, we can put together optimized brute-force problem solving and accessible modern supercomputers and get a reasonable way of solving super-complex problems. Technology is making it so that we don’t necessarily need cleverness in problem solving if we have access to a whole bunch of processor cores. “Today, SAT solving on high-performance computing systems enables us to conquer problems of high complexity, driven by practice,” Heule and Kullmann write. “This combination of enormous computational power with ‘magical brute force’ can now solve very hard combinatorial problems, as well as proving safety of systems such as railways.” To see this potential, we need to understand a bit about formal logic. In propositional logic, a proposition is just a statement that can be true or false. Crucially, such a statement has the property of being able to be negated. The statement “I am going to get a burrito,” for example, in negated form is just “I am not going to get a burrito.” So, the statement is a proposition. Propositional logic involves a whole lot proving that statements are true using logical operators such as AND and OR and NOT. As in my algebra example above, really complicated-seeming statements can often be rearranged into statements whose truth value is obvious. Computer science involves a lot of propositions, or true/false statements. That’s the essence of the whole thing, really. In formal propositional logic, we can imagine a bunch of individual atomic units of truth (that are either true or false combined using the above logical operators. For example, we might have the statement ((true AND false) OR true) AND NOT (true OR false) and be asked if that’s ultimately true or not. It’s not, but that’s probably not obvious. These things get really hard to evaluate and if you’ve ever had to wrestle with formal logic you know that reaching a solution sometimes just involves guessing and checking, which is a brute-force method.”