Is SAT a context-free language?

Question

I am considering the language of all satisfiable propositional logic formulae, SAT (to ensure that this has a finite alphabet, we would encode propositional letters in some suitable way [edit: the replies pointed out that the answer to the question may not be robust under varying encodings, so one needs to be more specific -- see my conclusions below]). My simple question is

Is SAT a context-free language?

My first guess was that today's (early 2017) answer should be "Nobody knows, since this relates to unresolved questions in complexity theory." However, this is not really true (see answer below), though not completely false either. Here is a short summary of things we know (starting with some obvious things).

1. SAT is not regular (because even the syntax of propositional logic is not regular, due to matching parentheses)
2. SAT is context-sensitive (it is not hard to give an LBA for it)
3. SAT is NP-complete (Cook/Levin), and in particular decided by nondeterministic TMs in polynomial time.
4. SAT can also be recognized by one-way nondeterministic stack automata (1-NSA) (see W. C. Rounds, Complexity of recognition in intermediate Level languages, Switching and Automata Theory, 1973, 145-158 http://dx.doi.org/10.1109/SWAT.1973.5)
5. The word problem for context-free languages has its own complexity class $\textbf{CFL}$ (see https://complexityzoo.uwaterloo.ca/Complexity_Zoo:C#cfl)
6. $\textbf{CFL}\subseteq\textbf{LOGCFL}\subseteq\textbf{AC}^{\textbf{1}}$, where $\textbf{LOGCFL}$ is the class of problems logspace reducible to $\textbf{CFL}$ (see https://complexityzoo.uwaterloo.ca/Complexity_Zoo:L#logcfl). It is known that $\textbf{NL}\subseteq\textbf{LOGCFL}$.
7. It is not known whether $\textbf{NL}\subsetneq\textbf{NP}$ or $\textbf{NL}=\textbf{NP}$ (in fact, even $\textbf{NC}^{\textbf{1}}\subsetneq\textbf{PH}$ is open; I think I got this from S. Arora, B. Barak: Computational Complexity: A Modern Approach; Cambridge University Press 2009). Hence, there cannot be any $\textbf{NP}$-complete problem that is known to not be in $\textbf{LOGCFL}$. Hence, it must be unknown if SAT is in $\textbf{LOGCFL}$.

However, this last point still leaves the possibility that SAT is known to not be in $\textbf{CFL}$. In general, I could not find much about the relationship of $\textbf{CFL}$ to the $\textbf{NC}$ hierarchy that might help to clarify the epistemic status of my question.

Remark (after seeing some initial answers): I am not expecting the formula to be in conjunctive normal form (this will not make a difference to the essence of the answer, and usually arguments still apply since a CNF is also a formula. But the claim that the constant-number-of-variables version of the problem is regular fails, since one needs parentheses for syntax.).

Conclusion: Contrary to my complexity-theory inspired guess, one can show directly that SAT is not context-free. The situation therefore is:

1. It is known that SAT is not context-free (in other words: SAT is not in $\textbf{CFL}$), under the assumption that one uses a "direct" encoding of formulae where propositional variables are identified by binary numbers (and some further symbols are used for operators and separators).
2. It is not know if SAT is in $\textbf{LOGCFL}$, but "most experts think" that it is not, since this would imply $\textbf{P}=\textbf{NP}$. This also means that it is unknown if other "reasonable" encodings of SAT are context-free (assuming that we would consider logspace an acceptable encoding effort for an NP-hard problem).

Note that these two points do not imply $\textbf{CFL}\subsetneq\textbf{LOGCFL}$. This can be shown directly by showing that there are languages in $\textbf{L}$ (hence in $\textbf{LOGCFL}$) that are not context-free (e.g., $a^nb^nc^n$).

Answer 1

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 well-formed 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 > 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.

Answer 2

If the number of variables is finite then so is the number of satisfiable conjunctions, so your SAT language is finite (and hence regular). [Edit: this claim assumes the CNFSAT form.]

Otherwise, let's agree to encode formulae such as $(x_{17}\vee \neg x_{21})\wedge (x_{1}\vee x_{2}\vee x_3)$ by $(17+\tilde{} 21)(1+2+3)$. We will use Ogden's lemma to prove that the language of all satisfiable conjunctions is not context-free.

Let $p$ be the "marking" constant in Ogden's lemma, and consider a sat-formula $w$ whose first clause consists of $(1^p)$ -- that is, the encoding of $(x_N)$, where $N$ is the decimal number consisting of $p$ ones. We mark the $p$ ones of $1^p$ and then require that all pumpings of the appropriate decomposition of $w$ (see the conclusion of Ogden's lemma) also be satisfiable. But we can easily block this by requiring that no clause containing $x_q$, where $q$ is a sequence of $1$'s shorter than $p$, be satisfiable -- for example, by ensuring that every other clause of $w$ has a negation of every such $x_q$. This means that $w$ fails the "negative pumping" property and we conclude that the language is not context-free. [Note: I've ignored the trivial cases where the pumping produces ill-formed strings.]