Time complexities of state-of-the-art SAT solvers with respect to length of the formula
For 3SAT, the number of variables is polynomially related to the number of clauses. (See the end for the justification.)

Consequently, any algorithm for 3SAT whose running time is polynomial in the number of clauses would also be polynomial in the number of variables; and any algorithm for 3SAT whose running time is polynomial in the number of variables would also be polynomial in the number of clauses.

It is known that there is a polynomial-time algorithm for 3SAT, if and only if there is a polynomial-time algorithm for SAT, if and only if there is a polynomial-time algorithm for CircuitSAT (e.g., for formulas).  Also, despite decades of work on SAT solvers, no one knows any algorithm for 3SAT that runs in polynomial time (or indeed in less than exponential time in the worst case).  You could take this as evidence that there is no polynomial-time algorithm for 3SAT; which implies that there is no polynomial-time algorithm for SAT or CircuitSAT, either, and also implies that P != NP.



Justification: Let $n$ denote the number of variables and $m$ the number of clauses.  We have $n \le 3m$ (a variable that doesn't appear in any clause can be ignored) and $m \le 8n^3$ (each clause has three literals, and you can ignore repeated clauses).  It follows that $n/3 \le m \le 8n^3$ and $\sqrt[3]{m/8} \le n \le 3m$, i.e., each is polynomially related to the other.



I see that you revised your question.  That clarifies that I think you have a misconception.  You talk about "run[ning] [a SAT solver] on arbitrary Boolean formulas".  However, you can't run a SAT solver on an arbitrary Boolean formula.  SAT solvers only work on CNF formulas.

However, we do know that any Boolean formula can be converted to an equisatisfiable CNF formula of size at most polynomial in the size of the formula, and vice versa.  If you had an algorithm that could test satisfiability of arbitrary Boolean formulas in time polynomial in the size of the formula, then it would follow that you have an algorithm that could test satisfiability of 3CNF formulas in time polynomial in the size of the formula (every 3CNF formula is a Boolean formula), and thus an algorithm that could test satisfiability of 3CNF formulas in time polynomial in the number of variables -- which contradicts the available evidence.  So, if you believe that there is no algorithm to solve 3SAT in time polynomial in the number of variables, then you should also believe that there is no algorithm to test satisfiability of arbitrary Boolean formulas in time polynomial in the size of the formula.