Lower upper bound on # variables in k-SAT with m clauses
If you want to prove the worst-case running time of your algorithm, you probably don't need to prove that.  It's probably enough that there exists instances of SAT with (say) $\frac12 mk$ variables that are NP-hard; and that can be proven.

When each variable occurs only twice in the formula, SAT can be solved in polynomial time (via resolution).

With the restriction that each variable can occur up to three times in the formula, SAT remains NP-hard.  (Proof: start with an ordinary CNF formula $\varphi$.  If $x_i$ appears $k$ times, introduce variables $x_{i,1},\dots,x_{i,k}$, replace the $j$th occurrence of $x_i$ with $x_{i,j}$, and add clauses for $\neg x_{i,1} \lor x_{i,2},\neg x_{i,2} \lor x_{i,3},\dots,\neg x_{i,k-1} \lor x_{i,k}, \neg x_{i,k} \lor x_{i,1}$.)

Therefore, there exists a class of instances of $k$-SAT with $m$ clauses and $\frac{1}{3} mk$ variables, such that solving those instances is NP-hard.

To answer your original question, there is no useful answer to your original question.  For all $\varepsilon&gt;0$, there exists a class of instances of $k$-SAT with $m$ clauses and $(1-\varepsilon)mk$ variables that is NP-hard.   In particular, take an ordinary CNF formula $\varphi$ with $n$ variables and then just append useless clauses of the form $x_{t} \lor x_{t+1} \lor \cdots \lor x_{t+k}$; each useless clause mentions $k$ new variables that appear only in that one clause and nowhere else.  The resulting formula is exactly as hard as $\varphi$, but now has a number of variables that is an arbitrarily large fraction of $mk$.