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.