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

<p>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 <a href="https://en.wikipedia.org/wiki/Ogden&#39;s_lemma" rel="nofollow noreferrer">Ogden's lemma</a>
to prove that the language of all satisfiable conjunctions is not context-free.</p>

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

CC BY-SA 3.0
2017-01-17T17:56:06.970Z
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
Aryeh
CC BY-SA 3.0
2017-01-17T17:57:12.490Z
... 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.
Aryeh
CC BY-SA 3.0
2017-01-17T23:20:55.290Z
The claim with regularity only works for CNFSAT (I added a clarification to my question).
mak
CC BY-SA 3.0
2017-01-18T09:23:17.573Z
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.
Emil Jeřábek
CC BY-SA 3.0
2017-01-18T09:45:11.533Z
@mak I edited the answer to reflect your observation.
Aryeh
CC BY-SA 3.0
2017-01-19T10:12:08.687Z
I do not understand yet how your argument would ensure that the negative pumping does not also remove the parts of the formula that you need to ensure unsatisfiability of any positive unit clause other than $x_N$. Can you elaborate?
mak
CC BY-SA 3.0
2017-01-19T10:19:03.577Z
The negative pumping only affects the string $1^p$ -- because of the way I've placed the marks, as per Ogden's lemma. So while I cannot ensure that a positive pumping will create an unsatisfiable assignment, I can certainly ensure that a negative one will -- since it will create litterals indexed by $1^q$, where $q<p$.
Aryeh
CC BY-SA 3.0
2017-01-20T15:35:18.847Z
I do not follow your argument here. Ogden's Lemma allows any of the strings to have any amount of unmarked positions, so negative pumping does not affect only the marked positions.
mak
CC BY-SA 3.0
2017-01-21T19:17:33.773Z
I think my application of Ogden's Lemma works, even if I may be off by a constant here or there. I mark only the contiguous stretch of 1s in the first variable of the formula. Ogden's lemma (items 1 and 2) force the pumped region to be limited to this contiguous stretch. Hence, *any* negative pumping will create unsatisfiable formulae.
Aryeh
CC BY-SA 3.0
2017-01-21T20:56:47.313Z
Item 2 (referring to the Wikipedia page) is always true if you only mark p positions in total, so this can't help much. Item 1 only requires that 1 marked position is pumped, but does not restrict how much of the unmarked string can be in xy. It seems to me that you could (un)pump, e.g., "(111)(~0)(~1)...(~110)" by picking u="(11", x="1", y="", z=")(~0)...(~110" and v=")", so as to obtain "(11)", which is satisfiable.
mak
CC BY-SA 3.0
2017-01-21T21:28:53.143Z
what is the value of p in your example?
Aryeh
CC BY-SA 3.0
2017-01-21T21:42:19.167Z
p would be 3 here (to make the illustration short), but the example is meant to be generic. I am using binary numbers rather than decimal ones, and I am (as it was easier to write) requiring that all other variables are mapped to false rather than just the ones with a "1" in them.
mak
CC BY-SA 3.0
2017-01-21T22:49:04.367Z
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.
Aryeh
CC BY-SA 3.0
2017-01-22T21:14:15.797Z
Yes, something like this could work, but it might end up being somewhat more complicated than the argument given by Marzio De Biasi here so maybe not worth the effort. Thanks for the quick answer and the discussion.
mak
CC BY-SA 3.0
2017-01-23T07:17:46.150Z
Actually, I'm quite confident that it works. The derivation tree necessarily has bounded out-degree, meaning that to generate a substring of sufficient length, you need some minimal height -- and that immediately allows for a pidgeonhole argument.
Aryeh
CC BY-SA 3.0
2017-01-17T17:03:20.673Z
2017-01-18T09:44:44.803Z
2017-01-18T09:44:44.803Z
Aryeh
<p>Just an alternative proof using a mix of well known results.</p>
<p>Suppose that:</p>
<ul>
<li>variables are expressed with the regular expression <span class="math-container">$d = (+|-)1(0|1)^*$</span></li>
<li>and that the (<em>regular</em>) language (over <span class="math-container">$\Sigma = \{0,1,+,-,\land,\lor\})$</span> used to represent CNF formulas is: <span class="math-container">$S = \{ d^+ (\lor d^+)^*(\land (d^+ (\lor d^+)^*))^* \}$</span>; just note that <span class="math-container">$S$</span> grabs all well-formed CNF formulas up to variable renaming.</li>
</ul>
<p>For example <span class="math-container">$\varphi = (x_1 \lor x_2) \land -x_3$</span> is written as: <span class="math-container">$s_{\varphi} = +1 \lor +10 \land -11 \in S$</span> (the <span class="math-container">$\lor$</span> operator has the precedence over <span class="math-container">$\land$</span>).</p>
<p>Suppose that <span class="math-container">$L = \{ s_{\varphi} \in S \, \mid $</span> s.t. the corresponding formula <span class="math-container">$\varphi$</span> is satisfiable <span class="math-container">$\}$</span> is CF .</p>
<p>If we intersect it with the regular language: <span class="math-container">$R = \{ +1^a \land  -1^b \land -1^c \mid a,b,c &gt; 0 \}$</span> we still get a CF language. We can also apply the homomorphism: <span class="math-container">$h(+) = \epsilon$</span>, <span class="math-container">$h(-) = \epsilon$</span> and the language remains CF.</p>
<p>But the language we obtain is: <span class="math-container">$L' = \{ 1^a \land 1^b \land 1^c \mid a \neq b, a \neq c\}$</span>, because if <span class="math-container">$a=b$</span> then &quot;source&quot; formula is <span class="math-container">$+x_a \land -x_a \land -x_b$</span> which is unsatisfiable (similarly if <span class="math-container">$a=c$</span>). But <span class="math-container">$L'$</span> is a well known non CF language <span class="math-container">$\Rightarrow$</span> contradiction.</p>

CC BY-SA 3.0
2017-01-22T21:16:17.727Z
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.
mak
CC BY-SA 3.0
2017-01-22T22:28:53.860Z
@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 ...
Marzio De Biasi
CC BY-SA 3.0
2017-01-24T03:27:58.340Z
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.
Kaveh
CC BY-SA 4.0
2017-01-17T21:57:07.503Z
2023-11-02T22:18:07.287Z
2023-11-02T22:18:07.287Z
Marzio De Biasi
<p>I am considering the language of all satisfiable propositional logic formulae, <strong>SAT</strong> (to ensure that this has a finite alphabet, we would encode propositional letters in some suitable way <em>[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]</em>). My simple question is</p>

<blockquote>
  <p>Is <strong>SAT</strong> a context-free language?</p>
</blockquote>

<p>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).</p>

<ol>
<li><strong>SAT</strong> is not regular (because even the syntax of propositional logic is not regular, due to matching parentheses)</li>
<li><strong>SAT</strong> is context-sensitive (it is not hard to give an LBA for it)</li>
<li><strong>SAT</strong> is NP-complete (Cook/Levin), and in particular decided by nondeterministic TMs in polynomial time.</li>
<li><strong>SAT</strong> can also be recognized by one-way nondeterministic stack automata (1-NSA) (see W. C. Rounds, <em>Complexity of recognition in intermediate Level languages</em>, Switching and Automata Theory, 1973, 145-158 <a href="http://dx.doi.org/10.1109/SWAT.1973.5" rel="noreferrer">http://dx.doi.org/10.1109/SWAT.1973.5</a>)</li>
<li>The word problem for context-free languages has its own complexity class $\textbf{CFL}$ (see <a href="https://complexityzoo.uwaterloo.ca/Complexity_Zoo:C#cfl" rel="noreferrer">https://complexityzoo.uwaterloo.ca/Complexity_Zoo:C#cfl</a>)</li>
<li>$\textbf{CFL}\subseteq\textbf{LOGCFL}\subseteq\textbf{AC}^{\textbf{1}}$, where $\textbf{LOGCFL}$ is the class of problems logspace reducible to $\textbf{CFL}$ (see <a href="https://complexityzoo.uwaterloo.ca/Complexity_Zoo:L#logcfl" rel="noreferrer">https://complexityzoo.uwaterloo.ca/Complexity_Zoo:L#logcfl</a>). It is known that $\textbf{NL}\subseteq\textbf{LOGCFL}$.</li>
<li>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: <em>Computational Complexity: A Modern Approach</em>; 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 <strong>SAT</strong> is in $\textbf{LOGCFL}$.</li>
</ol>

<p>However, this last point still leaves the possibility that <strong>SAT</strong> 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.</p>

<p><strong>Remark (after seeing some initial answers):</strong> 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.).</p>

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

<ol>
<li>It is known that <strong>SAT</strong> is <strong>not context-free</strong> (in other words: <strong>SAT</strong> is not in $\textbf{CFL}$), <strong>under the assumption that one uses a "direct" encoding</strong> of formulae where propositional variables are identified by binary numbers (and some further symbols are used for operators and separators).</li>
<li>It is not know if <strong>SAT</strong> 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 <strong>unknown if other "reasonable" encodings of SAT are context-free</strong> (assuming that we would consider logspace an acceptable encoding effort for an NP-hard problem).</li>
</ol>

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

CC BY-SA 3.0
2017-01-17T15:33:43.010Z
If it were, then P = NP.
Ryan Dougherty
CC BY-SA 3.0
2017-01-17T15:35:27.933Z
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.
AdamF
CC BY-SA 3.0
2017-01-17T18:17:06.710Z
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).
Aryeh
CC BY-SA 3.0
2017-01-17T22:56:55.867Z
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).
mak
CC BY-SA 4.0
2023-11-04T07:18:02.817Z
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.
botsina
<cc.complexity-theory><circuit-complexity><sat><context-free>
Is SAT a context-free language?
mak
# Is SAT a context-free language?

(Asked by: username_0 on 2017-01-17)

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

**Tags:** cc.complexity-theory, circuit-complexity, sat, context-free
> **Comments:**
> **username_1**: If it were, then P = NP.  
> **username_2**: 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.  
> **username_3**: 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).  
> **username_0**: 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).  
> **username_4**: 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.  

---

## 2 answers

### Answer by username_6 on 2017-01-17. Score: 8 | Accepted answer

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.

> **Comments:**
> **username_0**: 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.  
> **username_6**: @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 ...  
> **username_7**: 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.  

---

### Answer by username_3 on 2017-01-17. Score: 5

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](https://en.wikipedia.org/wiki/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.]

> **Comments:**
> **username_3**: 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  
> **username_3**: ... 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.  
> **username_0**: The claim with regularity only works for CNFSAT (I added a clarification to my question).  
> **username_5**: 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.  
> **username_3**: @mak I edited the answer to reflect your observation.  
> **username_0**: I do not understand yet how your argument would ensure that the negative pumping does not also remove the parts of the formula that you need to ensure unsatisfiability of any positive unit clause other than $x_N$. Can you elaborate?  
> **username_3**: The negative pumping only affects the string $1^p$ -- because of the way I've placed the marks, as per Ogden's lemma. So while I cannot ensure that a positive pumping will create an unsatisfiable assignment, I can certainly ensure that a negative one will -- since it will create litterals indexed by $1^q$, where $q<p$.  
> **username_0**: I do not follow your argument here. Ogden's Lemma allows any of the strings to have any amount of unmarked positions, so negative pumping does not affect only the marked positions.  
> **username_3**: I think my application of Ogden's Lemma works, even if I may be off by a constant here or there. I mark only the contiguous stretch of 1s in the first variable of the formula. Ogden's lemma (items 1 and 2) force the pumped region to be limited to this contiguous stretch. Hence, *any* negative pumping will create unsatisfiable formulae.  
> **username_0**: Item 2 (referring to the Wikipedia page) is always true if you only mark p positions in total, so this can't help much. Item 1 only requires that 1 marked position is pumped, but does not restrict how much of the unmarked string can be in xy. It seems to me that you could (un)pump, e.g., "(111)(~0)(~1)...(~110)" by picking u="(11", x="1", y="", z=")(~0)...(~110" and v=")", so as to obtain "(11)", which is satisfiable.  
> **username_3**: what is the value of p in your example?  
> **username_0**: p would be 3 here (to make the illustration short), but the example is meant to be generic. I am using binary numbers rather than decimal ones, and I am (as it was easier to write) requiring that all other variables are mapped to false rather than just the ones with a "1" in them.  
> **username_3**: 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.  
> **username_0**: Yes, something like this could work, but it might end up being somewhat more complicated than the argument given by Marzio De Biasi here so maybe not worth the effort. Thanks for the quick answer and the discussion.  
> **username_3**: Actually, I'm quite confident that it works. The derivation tree necessarily has bounded out-degree, meaning that to generate a substring of sufficient length, you need some minimal height -- and that immediately allows for a pidgeonhole argument.  

---

