|
|
|
|
|
by hinkley
384 days ago
|
|
The first SAT solver case that comes to mind is circuit layout, and then you have a k vs n problem. Because you don’t SAT solve per chip, you SAT solve per model and then amortize that cost across the first couple years’ sales. And they’re also “cheating” by copy pasting cores, which means the SAT problem is growing much more slowly than the number of gates per chip. Probably more like n^1/2 these days. If SAT solvers suddenly got inordinately more expensive you’d use a human because they used to do this but the solver was better/cheaper. Edit: checking my math, looks like in a 15 year period from around 2005 to 2020, AMD increased the number of cores by about 30x and the transistors per core by about 10x. |
|
"Oh well my algorithm isn't really O(N^2) because I'm going to print N copies of the answer!"
Absurd!