From a proof-theoretic perspective, mapping a problem to SAT and proving a statement by solving a SAT instance may be regarded as "brute force" because, as the article mentions, the proof is in a sense "meaningless" and hard to generalize.<p>However, from an algorithmic perspective, an approach such as the described one, which uses look-ahead and conflict-driven clause learning (CDCL), is much more sophisticated than a naive exhaustive search that relies solely on brute force to solve the task. The article mentions this:<p><i>“Look-ahead recursively splits the problem as cleverly as possible into subproblems, via looking-ahead. CDCL tries to assign variables to find a satisfying assignment in a straight-forward way, and if that fails (the normal case), then the failure is transformed into a clause, which is added to the formula.”</i><p>Quoting from <a href="https://en.wikipedia.org/wiki/Conflict-driven_clause_learning" rel="nofollow">https://en.wikipedia.org/wiki/Conflict-driven_clause_learnin...</a>:<p>“The CDCL algorithm has made SAT solvers so powerful that they are being used effectively in several real world application areas like AI planning, bioinformatics, software test pattern generation, software package dependencies, hardware and software model checking, and cryptography.”