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 only uses its memory as a stack.