This paper’s main contribution is a nice introduction of the Boolean satisfiability (SAT) problem to the general public. The basic idea is that the brute force approach of SAT to problem solving, called brute reasoning, is relevant.

Despite the untamed aspect of brute force, implying that all possibilities in a search space are explored, modern techniques and heuristics have been developed to systematically control such search space. The paper describes the two main techniques in an intuitive way: look-ahead and clause learning. It also discusses these techniques in two different contexts, local and global search. Some mathematical knowledge is necessary to understand them in detail, but helpful figures with examples are included.

The paper also focuses on a general-public application of such brute reasoning: automatic construction of mathematical proofs. Mathematicians have routinely trusted only short handwritten proofs and brute force proofs were considered a barbaric monster, due to their size of thousands of pages and the incapability of a human to understand them completely. However, SAT has been successfully applied here, generating a 200-terabyte proof for the Boolean Pythagorean triples problem. Other examples are presented in the paper, motivating a characterization of mathematical proofs: human truths (no computer help), weakly human truths (human could still check), weakly alien truth (only a computer can check), alien truth (no computer can check).

Another interesting point raised by this paper is whether a SAT proof can be trusted. If a problem has a solution, it is easy to check. But if a problem has no solution (it is unsatisfiable), it is difficult to construct a mathematical proof and to validate it. The paper motivates how the construction of a proof of unsatisfiability also trims the search space, invigorating the effectiveness of SAT to practical applications.