RECENT PROGRESS IN automated reasoning and supercomputing gives rise to a new era of brute force.
The game changer is “SAT,” a disruptive, brute-reasoning
technology in industry and science. We illustrate its
strength and potential via the proof of the Boolean
Pythagorean Triples Problem, a long-standing open
problem in Ramsey Theory. This 200TB proof has been
constructed completely automatically—paradoxically,
in an ingenious way. We welcome these bold new proofs
emerging on the horizon, beyond human understanding—
both mathematics and industry need them.
Many relevant search problems,
from artificial intelligence to combinatorics, explore large search spaces to
determine the presence or absence of a
certain object. These problems are hard
due to combinatorial explosion, and
have traditionally been called infeasible. The brute-force method, which
at least implicitly explores all possibilities, is a general approach to systematically search through such spaces.
Brute force has long been regarded
as suitable only for simple problems.
This has changed in the last two decades, due to the progress in Satisfiability (SAT) solving, which by adding
brute reason renders brute force into
a powerful approach to deal with many
problems easily and automatically.
Search spaces with far more possibilities than the number of particles in the
universe may be completely explored.
SAT solving determines whether a
formula in propositional logic has a
solution, and its brute reasoning acts
in a blind and uninformed way—as a
feature, not a bug. We focus on applying SAT to mathematics, as a systematic development of the traditional
method of proof by exhaustion.
Can we trust the result of running complicated algorithms on
many machines for a long time? The
strongest solution is to provide a
proof, which is also needed to show
correctness of highly complex systems, which are everywhere, from
finance to health care to aviation.
Mathematics solves problems by pen and
paper. CS helps us to go far beyond that.
BY MARIJN J.H. HEULE AND OLIVER KULLMANN
˽ Long-standing open problems in
mathematics can now be solved
completely automatically resulting in
clever though potentially gigantic proofs.
˽ Our time requires answers to hard
questions regarding safety and security.
In these cases knowledge is more
important than understanding as long as
we can trust the answers.
˽ Powerful SAT-solving heuristics facilitate
linear speedups even when using
thousands of cores. Combined with the
ever-increasing capabilities of high-performance computing clusters they
enable solving challenging problems.