3 ms·

From a technical standpoint, this is a terribly written article. First, giving an example of solving an algebraic equation using brute force is misleading, bec

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.

bassman9000 9y ago
I stopped reading after this This is thanks to a newish technology called Satisfiability (SAT) solving, which is a method of generating proofs in propositional logic. SAT3 was old when I was in college. And it's not to generate proofs.
slaymaker1907 9y ago
Even for integral/rational solutions, the problem is still Turing complete since there may be no solution at all.
- opportune 9y ago
  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
legulere 9y ago
This article is about SMT-solvers, which are used in formal verification, which can be about security. SMT solvers are kind of newish: https://excape.cis.upenn.edu/documents/ClarkBarrettSlides.pdf https://excape.cis.upenn.edu/documents/ClarkBarrettSlides.pd...
- opportune 9y ago
  The article and the linked paper (https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext 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 Apologies for being nasty
chx 9y ago
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.

bassman9000 9y ago

I stopped reading after this This is thanks to a newish technology called Satisfiability (SAT) solving, which is a method of generating proofs in propositional logic. SAT3 was old when I was in college. And it's not to generate proofs.

slaymaker1907 9y ago

Even for integral/rational solutions, the problem is still Turing complete since there may be no solution at all.

opportune 9y ago
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

legulere 9y ago

This article is about SMT-solvers, which are used in formal verification, which can be about security. SMT solvers are kind of newish: https://excape.cis.upenn.edu/documents/ClarkBarrettSlides.pdf https://excape.cis.upenn.edu/documents/ClarkBarrettSlides.pd...

opportune 9y ago
The article and the linked paper (https://cacm.acm.org/magazines/2017/8/219606-the-science-of-brute-force/fulltext 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 Apologies for being nasty

chx 9y ago

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.