<p>Given a formula in propositional logic with <span class="math-container">$100$</span> variables. We know that there can be no SAT-checking provably faster than <span class="math-container">$O(2^n)$</span>, unless P=NP. Now let's say I could find an algorithm which does SAT-solving provably in <span class="math-container">$O(2^{{n\choose3}/10^6})$</span>. Now this algorithm is asymptotically poor, but is provably optimal till <span class="math-container">$n=1000$</span>.</p>
<p>Question: Are there such algorithms in literature ? i.e asymptotically sub-optimal but provably optimal in a certain range ?</p>
<hr />
<p>Edit : I mistakenly wrote <span class="math-container">$O(2^{{n\choose3}/10^6})$</span> as <span class="math-container">$O({{n\choose3}/10^6})$</span>. Thanks @Yonatan N</p>

CC BY-SA 4.0
2021-02-15T18:34:43.673Z
$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](https://en.wikipedia.org/wiki/Circuit_complexity), [speed-up theorems](https://en.wikipedia.org/wiki/Blum%27s_speedup_theorem), and so on.
Yonatan N
CC BY-SA 4.0
2021-02-15T18:46:08.243Z
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 ?
SagarM
CC BY-SA 4.0
2021-02-15T22:04:02.833Z
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.
Laakeri
<sat>
Asymptotically sub-optimal but provably optimal algorithms in a finite range for NP-Hard problems?
SagarM
# Asymptotically sub-optimal but provably optimal algorithms in a finite range for NP-Hard problems?

(Asked by: username_0 on 2021-02-15)

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 @username_1

**Tags:** sat

> **Comments:**
> **username_1**: $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](https://en.wikipedia.org/wiki/Circuit_complexity), [speed-up theorems](https://en.wikipedia.org/wiki/Blum%27s_speedup_theorem), and so on.  
> **username_0**: 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 ?  
> **username_2**: 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.  

---

## 0 answers

