Is SAT a context-free language?
Just an alternative proof using a mix of well known results.

Suppose that:


variables are expressed with the regular expression $d = (+|-)1(0|1)^*$
and that the (regular) language (over $\Sigma = \{0,1,+,-,\land,\lor\})$ used to represent CNF formulas is: $S = \{ d^+ (\lor d^+)^*(\land (d^+ (\lor d^+)^*))^* \}$; just note that $S$ grabs all valid CNF formulas up to variable renaming.


For example $\varphi = (x_1 \lor x_2) \land -x_3$ is written as: $s_{\varphi} = +1 \lor +10 \land -11 \in S$ (the $\lor$ operator has the precedence over $\land$).

Suppose that $L = \{ s_{\varphi} \in S \, \mid $ s.t. the corresponding formula $\varphi$ is satisfiable $\}$ is CF .

If we intersect it with the regular language: $R = \{ +1^a \land  -1^b \land -1^c \mid a,b,c &gt; 0 \}$ we still get a CF language. We can also apply the homomorphism: $h(+) = \epsilon$, $h(-) = \epsilon$ and the language remains CF.

But the language we obtain is: $L' = \{ 1^a \land 1^b \land 1^c \mid a \neq b, a \neq c\}$, because if $a=b$ then "source" formula is $+x_a \land -x_a \land -x_b$ which is unsatisfiable (similarly if $a=c$). But $L'$ is a well known non CF language $\Rightarrow$ contradiction.