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$).

  • $\begingroup$ If it were, then P = NP. $\endgroup$ Jan 17, 2017 at 15:33
  • 1
    $\begingroup$ If SAT were context free then dynamic programing (the CYK algorithm) would give a polynomial time algorithm for testing membership in SAT, giving P=NP. Even P=NP wouldn't mean that SAT were Context-Free. This encoding of variables seems like it might be more important than you're giving it credit for. I haven't worked out the details but if you added unary or binary "subscripts" to the variables I think you'd have trouble distinguishing (x and y) from (x and not x) for large enough indices. $\endgroup$
    – AdamF
    Jan 17, 2017 at 15:35
  • $\begingroup$ You have to be precise about the representation before claiming P=NP conclusions. For example, factoring a number N is polynomial-time in N (the interesting question is concerning the number of bits needed to write N in binary, or about log N). $\endgroup$
    – Aryeh
    Jan 17, 2017 at 18:17
  • $\begingroup$ I was aware of the P=NP conclusion and that the answer therefore was not expected to be "yes" (sorry for being a little provocative in how I phrased this ;-). I was still wondering if this is really known or merely something that "most experts believe" (answers now clearly indicate that the former is true; I will select one in due course). $\endgroup$
    – mak
    Jan 17, 2017 at 22:56
  • $\begingroup$ 1) Wouldn't UNSAT be more likely to be a CFL because all UNSAT formulae have refutation proofs in proof systems (e.g. Resolution or Extended Resolution or Frege) that at least look like they could be context-free? (2) UNSAT and SAT look more like they would be context-free graph languages (CNFs can be viewed as bipartite graphs) which in general are known to be NP-complete to parse, so if they were context-free as graph grammars it wouldn't immediately imply that P=NP. $\endgroup$
    – botsina
    Nov 4, 2023 at 7:18

2 Answers 2


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.

  • $\begingroup$ I accepted this answer now since there is still an open issue with the other approach (see comments) and I like the somewhat more basic argument. It might be nice to emphasize that the argument is specific to the chosen encoding and it is indeed unknown if one could find another simple (logspace) encoding that leads to a context-free language. $\endgroup$
    – mak
    Jan 22, 2017 at 21:16
  • 1
    $\begingroup$ @mak: I suspect that any other "reasonable" encoding of SAT can be proved to be non CF with a similar technique. Perhaps another interesting direction would be to study if we can apply some sort of diagonalization to get a more general proof: the SAT formula encodes a computation that simulates a push down automata on a given input and it is satisfiable if and only if it doesn't accept it. But it's only a fuzzy idea ... $\endgroup$ Jan 22, 2017 at 22:28
  • $\begingroup$ Checking if a string is in a regular language is in P. Assume SAT was in Reg. Then NP=coNP. Let L be in Reg. Consider the formula that is true if it is not in L. It is in NP so it can be expressed as a SAT formula. It is in the language iff it is not. $\endgroup$
    – Kaveh
    Jan 24, 2017 at 3:27

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.]

  • $\begingroup$ Note: In my claim that for a finite number of variables the language is finite, I am implicitly disallowing repeating a variable within a clause or a clause unboundedly many times $\endgroup$
    – Aryeh
    Jan 17, 2017 at 17:56
  • $\begingroup$ ... But I think the language is still regular, because one takes the finite collection of "essentially distinct" (i.e., without trivial repetitions) formulae and then allows the various repetitions. $\endgroup$
    – Aryeh
    Jan 17, 2017 at 17:57
  • $\begingroup$ The claim with regularity only works for CNFSAT (I added a clarification to my question). $\endgroup$
    – mak
    Jan 17, 2017 at 23:20
  • 4
    $\begingroup$ Even with arbitrary non-CNF formulas in finitely many variables, satisfiability (and any language that cannot distinguish two logically equivalent formulas for that matter) is easily seen to be context-free. However, I fail to see the relevance of this. Satisfiability of formulas in finitely many varibles is a trivial problem that has nothing to do with the complexity of SAT. $\endgroup$ Jan 18, 2017 at 9:23
  • 1
    $\begingroup$ OK, I see the problem -- I was implicitly assuming that $|xyz|$ can be bounded in length (as in the classic pumping lemma), while also being able to specify something about its location in the string. I think the argument can be fixed by re-doing the pumping lemma from scratch. We'll make that first variable a really long sequence of 1's -- long enough that some sub-tree generating a contiguous substring of those 1's has to be sufficiently deep for the pidgeonhole principle to apply. $\endgroup$
    – Aryeh
    Jan 21, 2017 at 22:49

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.