"Ok, here's an optimal SAT algorithm (universal search)".
"Nice, but what is the big O complexity of universal search for SAT?".
"Nobody knows".
You're no better off than before if you wanted an answer like "exponential". On the other hand a provably sub-exponential SAT algorithm would be a huge theoretical breakthrough even if "galactic". Same for a proof that P=NP where the exponent in the P-time SAT algorithm was the 5000th busy beaver number, or whatever.
Also empirically, pretty much any provably polynomial algorithm we have found for anything has fairly tame exponents. That's a big part of why 'polynomial' works as a short-hand for 'tractable' that also has nice theoretical properties.
Btw, I don't know whether the tame exponents are in some sense natural, or whether they are a product of how humans find and design algorithms. Perhaps AI will change that.
https://cstheory.stackexchange.com/questions/6660/polynomial...