In another thread, Joe Fitzsimons asked about "the best current lower bounds on 3SAT."
I'd like to go the other way: What's the best current upper bounds on 3SAT? In other words, what is the time complexity of the most efficient SAT solver?
In particular, is it conceivable to find a sub-exponential (yet super-polynomial) algorithm for SAT?
The best algorithm for 3-SAT now has numerical upper bound $O^{*}(1.306995^n)$ on unique-3-SAT and on general-3-SAT it is also fastest but now the specific values have not been analyzed yet.
Authors say they hope the improved bounds for unique-3-SAT also apply directly to 3-SAT by using essentially the arguments of Hertli.
The algorithm is described in this paper:
Thomas Dueholm Hansen, Haim Kaplan, Or Zamir, Uri Zwick, Faster k-SAT algorithms using biased-PPSZ, 2019
Simply speaking, it adds bias to the PPSZ algorithm to let some literals have a higher, lower or equal probability to turn to some value.
In the paper, they say that the derandomization of this algorithm may be not very hard and moreover, they believe this algorithm can achieve $O^{*}(1.30331^n)$ for 3-SAT.
For future work, they say there is a more challenging way to obtian further improvements by guessing more varibles biasedly without using a set of disjoint clauses as a scaffolding that simplifies analysis.
In the paper, the problem whether bound for k-SAT can be of form ${2^{\left(1 - \frac{\omega (1)}{k}\right)n}}$ is proposed by authors and is believed to be more important than just giving a better constant bound for 3-SAT.
There are two kinds of "best" SAT solvers, one for theory, one for practice.
randomized $O(1.32113^n)$ for 3SAT.
randomized $O(1.321^n)$ for 3SAT.
deterministic $O(1.439^n)$ for 3SAT.
Check SAT conference for competition results for each year.
I am not aware of any zero-error randomized algorithms (or coNE/Eadvice algorithms,
for that matter) for SAT that have better bounds than known deterministic algorithms,
regardless of whether or not there is promised to be at most one satisfying assignment.
"Problem 3-SAT is deterministically solvable in time $\overset{\sim}{O}(1.3303^n)$."
"For a uniquely satisfiable 3-CNF (resp. 4-CNF) on $n$ variables, the satisfying assignment
can be found in deterministic running time at most $O\hspace{.02 in}(1.3071^n)$ (resp. $O\hspace{.02 in}(1.4699^n)$)."
- "There exists a randomized algorithm for 3-SAT with
one-sided error that runs in time $O\hspace{.02 in}(1.30704^n)$."- "There exists a randomized algorithm for 4-SAT with
one-sided error that runs in time $O\hspace{.02 in}(1.46899^n)$."
"There is a randomized algorithm for unique-3-SAT such that for $\: \epsilon = 1\hspace{-0.03 in}\big/\hspace{-0.06 in}\left(\hspace{-0.03 in}10^{\hspace{.02 in}24}\hspace{-0.04 in}\right) \:$ and
$S$ the real number that lets the previous paper's runtime bound for 3-SAT be expressed
as $\: O\hspace{-0.04 in}\left(2^{(S+o(1))\cdot n}\right) \:$, $\;$ the current paper's algorithm runs in time $\: O\hspace{-0.04 in}\left(2^{(S-\epsilon+o(1))\cdot n}\right)$ ."
Schoening's algorithm is a probabilistic algorithm for k-SAT with running time $O(a^n)$, where $a = 2(k-1)/k$. This results in an $O(1.33334^n)$ algorithm for 3SAT, an $O(1.5^n)$ algorithm for 4SAT, etc.
The algorithm has also been (almost completely) derandomized by Moser and Scheder, who give a deterministic algorithm for solving kSAT running time $O((a+\epsilon)^n)$ where $a$ is the same constant as before, and $\epsilon>0$ can be made arbitrarily small.
Note: In this answer the big Oh notation hides poly(n) factors. I wanted to use the $O^*$ notation, but it isn't rendering properly.
As was already mentioned, if you are interested in theoretical running time guarantees, this question is a duplicate.
But I'd like to point out that if you really want to solve a concrete problem (like the colouring problem that you mentioned), I think that it makes absolutely no sense at all to study theoretical upper bounds.
Even though you wanted to avoid "engineering" aspects, I'd suggest that you just take some popular SAT solvers, try them out, and see what happens (most of them can read the same DIMACS file format, so it is easy to try different solvers). You may have both positive and negative surprises. Recently I had a family of SAT instances; a bunch of instances with tens of thousands of variables and more than one million clauses turned out to be easy to solve, while seemingly much simpler instances with just hundreds of variables and thousands of clauses were far too difficult for any solver that I tried.
deterministic $O(1.308^n)$ for 3SAT.
It is impossible for 3SAT to have sub-exponential algorithms unless the exponential time hypothesis is false.
randomized algorithm with expected running time $O({1.324}^n)$ for 3SAT.
randomized algorithm with expected running time $O({1.32216}^n)$ for 3SAT.
This post deals with upper bounds on SAT. This one deals with best lower bounds. This link gives details of the annual competition comparing SAT solver implementations, which are all downloadable. For simplicity, you could start with SAT4J, a Java based library for SAT solving.
The best deterministic algorithm for 3-SAT now has upper bound 1.32793^n, see https://arxiv.org/abs/1804.07901 by Sixue Liu. Basically the upper bounds for all k-SAT have been improved in this paper.
