2021.02.14 13:28:30 (1360928904676929539) from Daniel J. Bernstein, replying to "Boaz Barak (@boazbaraktcs)" (1359883579673595906):
The literature on SAT challenge problems focuses on the edge of what a general-purpose SAT solver can handle on an academic's computer. This is quantitatively (and, I would expect, qualitatively) very different from the edge of what cryptanalysts can break using serious hardware.
2021.02.11 07:53:05 (1359757329386754052) from Daniel J. Bernstein:
Guess for where the 20000 comes from: (1) X falls for D-Wave's BS that n-qubit quantum computers will magically minimize any n-variable quadratic, in particular breaking n-variable SAT. (2) X "discovers" well-known conversion of typical cipher into SAT with about 20000 variables.
2021.02.11 08:16:58 (1359763343599280130) from Daniel J. Bernstein:
It's easy to see how #2 turns into a press release if X is a snake-oil salesman, but I think the bigger problem is D-Wave's BS. Can we agree on some "Has D-Wave solved these yet?" challenge problems? What's the strongest cipher that we can express quadratically in n variables?
2021.02.11 16:14:45 (1359883579673595906) from "Boaz Barak (@boazbaraktcs)":
I’d guess that to find a hard quadratic problem with a small number of variables, the best approach is not to try to reduce a cipher but rather to look at some graph coloring problems. People studied constructing small hard instances for SAT (e.g. http://www.cs.qub.ac.uk/~i.spence/sgen/ )