From a technical standpoint, this is a terribly written article.
First, giving an example of solving an algebraic equation using brute force is misleading, because you can't enumerate all values of a real number.
Second, the risks of secrutity regarding brute force computing having nothing to do with SAT.
Also, their description of SAT is inaccurate. It's not new, and it was actually one of the first formal problems studied in computer science. Also, the original, linked paper notes that it is not brute-force computing that is itself the breakthrough, but the addition of heuristics in SAT solvers that make brute-forcing feasible.
The article and the linked paper (https://cacm.acm.org/magazines/2017/8/219606-the-science-of-...) are about SAT solvers. The paper mentions SMTs briefly in passing. There may be a disconnect in whether SMTs are referred to as SAT solvers or their own distinct entity, though
True, countability doesn't change the problem. Solving a mathematical equation is just a bad way in general to explain what a brute force solver does. Much better to use an example such as a crossword puzzle or sudoku
Finally someone notes that! I read "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. " and began to twitch.
First, giving an example of solving an algebraic equation using brute force is misleading, because you can't enumerate all values of a real number.
Second, the risks of secrutity regarding brute force computing having nothing to do with SAT.
Also, their description of SAT is inaccurate. It's not new, and it was actually one of the first formal problems studied in computer science. Also, the original, linked paper notes that it is not brute-force computing that is itself the breakthrough, but the addition of heuristics in SAT solvers that make brute-forcing feasible.