What does this mean for NP-complete problems? Is the term “fast” only applicable to this small Sudoku board, or are solvers optimized to the point where something like O(2^256) doesn’t take that much time to run?
SAT solvers aren't a magic "asymtotic complexity shrinker" like that. They are more like really clever backtracking algorithms, cleverer than what you would usually write by hand.
The actual difficulty of an NP complete problem depends on what the problem is, and what particular instance you are trying to solve. In a "constraint solving" setting, underconstrained instances are usually trivially solvable with a YES solution, overconstrained instances have an easy to find NO solution, and the instances that have just the right amount of constraints are the ones that are trully hard.
What a good SAT solver does is that it can solve some instances that a naive backtracking algorithm probably would not be able to do. Here are some examples of tricks that SAT solvers perform:
* non chronological backtracking: when a search branch is deemed non-viable, instead of undoing just the last choice, the algorithm determines what choice was to "blame" for the lack of solutions, and undoes back to that instead.
* learning new constraints. When a search branch is deemed invalid, a new constraint is calculated based on the choices made on that search branch. This helps avoid the same sequence of choices from being repeated in a future search.
* aggressive randomization and restarts. The time distribution taken to solve a random instance of an NP-complete problem is fat-tailed. In these cases, an aggressive restart policy might speed things up even without other algorithmic improvements.
It's impossible to create a solver that is efficient on any and all NP-complete problems. That applies to any solver.
Still, it is possible to create efficient solvers for some subset of the NP-complete problem space. They will work fine on some problem exhibiting the proper "shape" / internal structure. What that is is often hard to tell...
So in practice using SAT solvers (or SMT, or constraint, or MIP ones...) has some empirical side to it. It can work extremely well in some cases: it's possible to solve problems with 10s of millions of Boolean variables for example. It can also fail (time out). That depends a lot on the problem type and the solver heuristics. It's common in this area to try different solvers, and be happy if one gets a result in reasonable time. So there can be magic, but also some frustration.
As a practical example, SMT solvers are used for software formal proof. It's typical for those tools (like Frama C) to try several solvers. If any find a proof, you're good and the proof is for free (no human work needed). If none work, it's up to the engineer to reshape the problem to "help" the solver, or bite the bullet and deal with the proof (semi) manually with coq or a similar tool.
All this being said, modern solvers are really powerful. If it's a human scale problem solvable "by hand" with lots of work, a solver should deal with it very quickly.
fast here means compared to a naive implementation. They use a lot of optimization and heuristics.
What would be a O(2^256) problem? A boolean formula with 256 binary variables? In many cases those can be broken down to independent smaller formulas which are easier to solve, in which case a solver might be quite fast on it, yes. But something that provably does not reduce to a smaller complexity would still take forever, I guess. Corrections welcome.
