from Hacker News

The Science of Brute Force (2017)

by QuinnWilton on 12/15/20, 1:10 AM with 2 comments

• by triska on 12/15/20, 7:42 AM

  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.

  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:

  “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.”

  Quoting from https://en.wikipedia.org/wiki/Conflict-driven_clause_learnin...:

  “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.”

• by gumby on 12/15/20, 2:58 PM

  My problem with these massive / exhaustive proofs is they provide no insight. Sure, you can use them as a building block to prove something else, but they don’t uncover new tools and approaches to solve other problems.

  Compare it to, say, Wiles’s proof of Fermat’s last theorem: I can’t understand that proof either, but there are many who can, and for them it teaches a bunch of things.