# Asymptotically sub-optimal but provably optimal algorithms in a finite range for NP-Hard problems?

Given a formula in propositional logic with $$100$$ variables. We know that there can be no SAT-checking provably faster than $$O(2^n)$$, unless P=NP. Now let's say I could find an algorithm which does SAT-solving provably in $$O(2^{{n\choose3}/10^6})$$. Now this algorithm is asymptotically poor, but is provably optimal till $$n=1000$$.

Question: Are there such algorithms in literature ? i.e asymptotically sub-optimal but provably optimal in a certain range ?

Edit : I mistakenly wrote $$O(2^{{n\choose3}/10^6})$$ as $$O({{n\choose3}/10^6})$$. Thanks @Yonatan N

• $O\left({n \choose 3} / 10^6\right) = O(n^3)$ which is asymptotically very good for SAT. Anyway, on any finite domain, there is a provably optimal algorithm that hard-codes a lookup table of outputs. Surely this is not what you want. Can you clarify a bit on the direction you do want to go in? There are lots of possible reinterpretations of your problem, including circuit problems, speed-up theorems, and so on. Feb 15, 2021 at 18:34
• I am actually working on model counting for probabilistic inference purposes (but I am a Physicist by background), I don't have a clear direction, but would definitely want that the algorithm to be for general SAT. Also, I am sorry, I think my use of big O is still a bit abusive as I guess $O(2^{{n \choose 3}}) = O(2^{n^3})$. But I would just like to know are such problems investigated and interesting to people ? Feb 15, 2021 at 18:46
• I have also thought that proving "finitist" complexity results, for example something like "3-SAT with at most 100 variables can be solved in $10^9$ steps", would be cool. However I think the reason why nobody bothers to spend time on such results is that really they would just combine the worst of both worlds of theory and practice: for theory people there would not be beautiful maths, just more careful analysis and casework, and for practice people the result would likely still be irrelevant because the worst-case model is so pessimistic compared to the real world. Feb 15, 2021 at 22:04