It's disappointing that the authors use the term "brute force" to describe modern SAT solving, in an article intended for people who may not be familiar with the algorithms used.

That term implies that the speed of the computer that was used to find the solution is the determining factor.

It is not. Modern SAT solvers use very elegant search algorithms that have enabled the solution of SAT-encoded problems that could never have been solved if only "brute force" was used.