Is SAT known to be non-context-free or even non-regular?
One possible encoding of SAT is as a string over the alphabet $\{x,\land,\lor,\lnot,0,1\}$ which encodes a satisfiable CNF. This language is not regular since intersecting it with an appropriate regular expression, we obtain the language semantically representing $x_i \land \lnot x_i$, which is essentially the language of squares $ww$, classically known to be non-regular. The same argument also shows that UNSAT is not context-free. It is highly likely that similar arguments (perhaps using fancier template formulas) would show that SAT is also not context-free.