In general, asymptotic complexity concerns itself with the size of the input. In this case, the number of input symbols. SAT is thus not polynomially solvable in the worst case as a function of the number of symbols.
It is also not polynomially solvable with respect to the number of unique variables. This is trivially so, as this is clearly upper bounded by the size of the input.
However, SAT is tractable in the special case that the number of unique variables is low. That is, it's Fixed Parameter Tractable with respect to that parameter. Indeed, we can try each assignment to the variables (of which there are an exponential amount w.r.t. the number of unique variables) and verify whether they satisfy the whole formula (which is linear in the size of the formula). Thus with $n$ unique variables and $m$ total symbols, SAT is solvable in O($2^n$m).