<p>Though not directly constructing a context sensitive grammar for SAT, the following paper might shed some light.</p>

<p>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">http://dx.doi.org/10.1109/SWAT.1973.5</a></p>

<p>The paper by Rounds gives a one-way nondeterministic stack automaton (1-NSA) recognizing SAT, and then shows the membership problem of 1-NSA (and its proper superset, Aho's Indexed Grammar) is in general in NP. In other words, SAT as a CSL/linear-bounded-automata is special in the sense that it uses its memory only as a stack.</p>

CC BY-SA 3.0
2012-01-30T15:44:34.477Z
Thanks, exactly what I was looking for!  Rounds shows that SAT is a one-way stack language, an indexed language, and a tree transducer language, giving three different language-theoretic reasons why it it special.
András Salamon
CC BY-SA 3.0
2012-01-31T21:44:31.607Z
so maybe "sufficient" but it is not immediately clear if those conditions are necessary (for the CSL/CSG recognition to be in NP). so it does seem to me like your general question may not be studied much. CSLs/CSGs seem not to have a large amt of research behind them.
vzn
CC BY-SA 3.0
2012-02-03T16:43:44.300Z
further thought on this. its a problem generally in the form "is recognition of a language in larger class Y actually in smaller language class X". for Y=CFG and X=RLs (regular language) the problem is undecidable see eg [does this cfg define a regular language](http://cstheory.stackexchange.com/questions/10048/decidability-of-does-this-cfg-define-a-regular-language). therefore Y=CSL and X=NP seems likely to be undecidable in general also.
vzn
CC BY-SA 3.0
2012-01-30T11:38:14.610Z
2012-01-30T11:46:32.993Z
2012-01-30T11:46:32.993Z
kinaba
<p>By a classic result of Kuroda, the complexity class <a href="http://en.wikipedia.org/wiki/Linear_bounded_automaton">NSPACE[$n$]</a> (also known as NLIN-SPACE) is precisely the class CSL of <a href="http://en.wikipedia.org/wiki/Context-sensitive_language">context-sensitive languages</a>.  The satisfiability problem <a href="http://en.wikipedia.org/wiki/Boolean_satisfiability_problem">SAT</a> is in NSPACE[$n$], since a linear-sized guess for a solution can be checked with at most a linear amount of overhead for book-keeping.  This means that SAT must have a <a href="http://en.wikipedia.org/wiki/Context-sensitive_grammar">context-sensitive grammar</a> (CSG).</p>

<blockquote>
  <p>Has anyone attempted to provide a CSG for SAT?</p>
</blockquote>

<p>I realise many questions related to CSLs are undecidable (for instance deciding if a given CSG generates the empty language).  Even given a CSG for SAT one would still have to overcome the obstacle that deciding membership in the language given by a CSG is PSPACE-complete in general.  <strike>But it might be the case that the membership problem for the CSG that defines SAT is in NP, due to some special structure of the language.</strike>  <em>Rephrasing, to address comment by MCH:</em> But it might be the case that the membership problem for the CSG that defines SAT could be shown to be in NP due to some special structure of the grammar, and not because we already know it must be in NP.</p>

<ul>
<li>S.-Y. Kuroda, <em>Classes of languages and linear-bounded automata</em>, Information and Control <strong>7</strong>(2) 207–223, 1964.  doi:<a href="http://dx.doi.org/10.1016/S0019-9958%2864%2990120-2">10.1016/S0019-9958(64)90120-2</a></li>
</ul>

<hr>

<h2>Clarification:</h2>

<p>The intended focus here is the special feature of the grammar for SAT which allows it to be recognized by an NTIME[poly($n$)] machine, rather than the NSPACE[$n$] $\subseteq$ DTIME[$2^{O(n)}$] bound.</p>

<p>The proof of Theorem 3 in Landweber's 1963 paper constructs a CSG from a linear-bounded automaton.  (Kuroda provided the converse, constructing a linear-bounded automaton for any CSG.)  However, Landweber's procedure does not seem to yield a grammar for SAT that is of special form: all NSPACE[$n$] recognizers are treated in the same generic way.  In other words, it is not clear why the SAT CSG should have an NP membership problem, rather than being PSPACE-complete.  I was hoping for a more explicit construction that uses the NP-ness of SAT in some essential way.</p>

<p>Perhaps a better, more precise, question is whether:</p>

<ol>
<li>there exists a linear-bounded automaton that recognizes SAT,</li>
<li>from which one can extract a CSG,</li>
<li>so that the language defined by the CSG is in NP due to some feature of the grammar (and not because we already know it is in NP)?</li>
</ol>

<p>In the intervening five decades, surely someone has tried to do this!  Since I can't find anything published along these lines, I would be interested in understanding why this approach did not work, or a pointer to work I have missed.</p>

<ul>
<li>Peter S. Landweber, <em>Three theorems on phrase structure grammars of type 1</em>, Information and Control <strong>6</strong>(2) 131–136, 1963.  doi:<a href="http://dx.doi.org/10.1016/S0019-9958%2863%2990169-4">10.1016/S0019-9958(63)90169-4</a></li>
</ul>

CC BY-SA 3.0
2012-01-29T23:36:35.063Z
I don't understand. Can't you just follow the proof and produce the CSG for SAT? Is it non-constructive? Also about the last sentence, "it might be the case that the membership problem for the CSG that defines SAT is in NP", it *is* in NP since the membership problem is just SAT, which is in NP.
Mahdi Cheraghchi
CC BY-SA 3.0
2012-01-30T09:14:43.097Z
@MCH: Thanks for your comment, I hope the edit clarifies the question.
András Salamon
CC BY-SA 3.0
2012-01-30T23:16:51.487Z
it sounds like another way to phrase this might be like this: there exist CSLs/CSGs that are recognizable in NP time in (contrast to PSPACE in the general case) based on converting SAT. what is special about their "structure" that permits this? converting SAT to a CSL/CSG might give a "hint" but does not nec. give a more general criteria. in other words given an arbitrary CSL/CSG is there some criteria that indicates its recognition is actually in NP?
vzn
<cc.complexity-theory><fl.formal-languages><sat><space-bounded>
Context-sensitive grammar for SAT?
András Salamon
# Context-sensitive grammar for SAT?

(Asked by: username_0 on 2012-01-29)

By a classic result of Kuroda, the complexity class [NSPACE[$n$]](http://en.wikipedia.org/wiki/Linear_bounded_automaton) (also known as NLIN-SPACE) is precisely the class CSL of [context-sensitive languages](http://en.wikipedia.org/wiki/Context-sensitive_language). The satisfiability problem [SAT](http://en.wikipedia.org/wiki/Boolean_satisfiability_problem) is in NSPACE[$n$], since a linear-sized guess for a solution can be checked with at most a linear amount of overhead for book-keeping. This means that SAT must have a [context-sensitive grammar](http://en.wikipedia.org/wiki/Context-sensitive_grammar) (CSG).

> Has anyone attempted to provide a CSG for SAT?

I realise many questions related to CSLs are undecidable (for instance deciding if a given CSG generates the empty language). Even given a CSG for SAT one would still have to overcome the obstacle that deciding membership in the language given by a CSG is PSPACE-complete in general. But it might be the case that the membership problem for the CSG that defines SAT is in NP, due to some special structure of the language. *Rephrasing, to address comment by MCH:* But it might be the case that the membership problem for the CSG that defines SAT could be shown to be in NP due to some special structure of the grammar, and not because we already know it must be in NP.

* S.-Y. Kuroda, *Classes of languages and linear-bounded automata*, Information and Control **7**(2) 207–223, 1964. doi:[10.1016/S0019-9958(64)90120-2](http://dx.doi.org/10.1016/S0019-9958%2864%2990120-2)

---

## Clarification:

The intended focus here is the special feature of the grammar for SAT which allows it to be recognized by an NTIME[poly($n$)] machine, rather than the NSPACE[$n$] $\subseteq$ DTIME[$2^{O(n)}$] bound.

The proof of Theorem 3 in Landweber's 1963 paper constructs a CSG from a linear-bounded automaton. (Kuroda provided the converse, constructing a linear-bounded automaton for any CSG.) However, Landweber's procedure does not seem to yield a grammar for SAT that is of special form: all NSPACE[$n$] recognizers are treated in the same generic way. In other words, it is not clear why the SAT CSG should have an NP membership problem, rather than being PSPACE-complete. I was hoping for a more explicit construction that uses the NP-ness of SAT in some essential way.

Perhaps a better, more precise, question is whether:

1. there exists a linear-bounded automaton that recognizes SAT,
2. from which one can extract a CSG,
3. so that the language defined by the CSG is in NP due to some feature of the grammar (and not because we already know it is in NP)?

In the intervening five decades, surely someone has tried to do this! Since I can't find anything published along these lines, I would be interested in understanding why this approach did not work, or a pointer to work I have missed.

* Peter S. Landweber, *Three theorems on phrase structure grammars of type 1*, Information and Control **6**(2) 131–136, 1963. doi:[10.1016/S0019-9958(63)90169-4](http://dx.doi.org/10.1016/S0019-9958%2863%2990169-4)

**Tags:** cc.complexity-theory, fl.formal-languages, sat, space-bounded
> **Comments:**
> **username_1**: I don't understand. Can't you just follow the proof and produce the CSG for SAT? Is it non-constructive? Also about the last sentence, "it might be the case that the membership problem for the CSG that defines SAT is in NP", it *is* in NP since the membership problem is just SAT, which is in NP.  
> **username_0**: @MCH: Thanks for your comment, I hope the edit clarifies the question.  
> **username_2**: it sounds like another way to phrase this might be like this: there exist CSLs/CSGs that are recognizable in NP time in (contrast to PSPACE in the general case) based on converting SAT. what is special about their "structure" that permits this? converting SAT to a CSL/CSG might give a "hint" but does not nec. give a more general criteria. in other words given an arbitrary CSL/CSG is there some criteria that indicates its recognition is actually in NP?  

---

## 1 answers

### Answer by username_3 on 2012-01-30. Score: 9 | Accepted answer

Though not directly constructing a context sensitive grammar for SAT, the following paper might shed some light.

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>

The paper by Rounds gives a one-way nondeterministic stack automaton (1-NSA) recognizing SAT, and then shows the membership problem of 1-NSA (and its proper superset, Aho's Indexed Grammar) is in general in NP. In other words, SAT as a CSL/linear-bounded-automata is special in the sense that it uses its memory only as a stack.

> **Comments:**
> **username_0**: Thanks, exactly what I was looking for!  Rounds shows that SAT is a one-way stack language, an indexed language, and a tree transducer language, giving three different language-theoretic reasons why it it special.  
> **username_2**: so maybe "sufficient" but it is not immediately clear if those conditions are necessary (for the CSL/CSG recognition to be in NP). so it does seem to me like your general question may not be studied much. CSLs/CSGs seem not to have a large amt of research behind them.  
> **username_2**: further thought on this. its a problem generally in the form "is recognition of a language in larger class Y actually in smaller language class X". for Y=CFG and X=RLs (regular language) the problem is undecidable see eg [does this cfg define a regular language](http://cstheory.stackexchange.com/questions/10048/decidability-of-does-this-cfg-define-a-regular-language). therefore Y=CSL and X=NP seems likely to be undecidable in general also.  

---

