By a classic result of Kuroda, the complexity class NSPACE[n] (also known as NLIN-SPACE) is precisely the class CSL of context-sensitive languages. The satisfiability problem SAT 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 (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.

• 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

By a classic result of Kuroda, the complexity class NSPACE[$n$] (also known as NLIN-SPACE) is precisely the class CSL of context-sensitive languages. The satisfiability problem SAT 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 (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

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