Grammaire contextuelle pour SAT?

Par un résultat classique de Kuroda, la classe de complexité NSPACE [ ]$n$ (également connue sous le nom de NLIN-SPACE) est précisément la classe CSL des langages contextuels . Le problème de satisfiabilité SAT est dans NSPACE [ ], car une estimation de taille linéaire pour une solution peut être vérifiée avec au plus une quantité linéaire de frais généraux pour la comptabilité. Cela signifie que SAT doit avoir une grammaire contextuelle (CSG).$n$

Quelqu'un a-t-il tenté de fournir un CSG pour SAT?

Je me rends compte que de nombreuses questions liées aux CSL sont indécidables (par exemple, décider si un CSG donné génère le langage vide). Même étant donné un CSG pour SAT, il faudrait encore surmonter l'obstacle que la décision d'appartenir à la langue donnée par un CSG soit en général PSPACE-complete. Mais il se peut que le problème d'appartenance au CSG qui définit SAT soit dans NP, en raison d'une structure particulière du langage. Reformulation, pour répondre au commentaire de MCH: Mais il se pourrait que le problème d'appartenance au CSG qui définit SAT puisse être démontré comme NP en raison d'une structure particulière de la grammaire, et non parce que nous savons déjà qu'il doit être en NP.

• S.-Y. Kuroda, Classes de langues et automates linéaires , Information et contrôle 7 (2) 207–223, 1964. doi: 10.1016 / S0019-9958 (64) 90120-2

Clarification:

L'objectif visé ici est la particularité de la grammaire de SAT qui lui permet d'être reconnue par une machine NTIME [poly ( )], plutôt que par la borne NSPACE [ n ] ⊆ DTIME [ 2 O ( n ) ].$n$$n$$\subseteq$$2^{O(n)}$

La preuve du théorème 3 dans l'article de Landweber de 1963 construit un CSG à partir d'un automate borné linéaire. (Kuroda a fourni l'inverse, construisant un automate borné linéaire pour n'importe quel CSG.) Cependant, la procédure de Landweber ne semble pas produire une grammaire pour SAT qui soit de forme spéciale: tous les reconnaisseurs NSPACE [ ] sont traités de la même manière générique. En d'autres termes, il n'est pas clair pourquoi le SAT CSG devrait avoir un problème d'adhésion NP, plutôt que d'être PSPACE-complete. J'espérais une construction plus explicite qui utilise le NP-ness de SAT d'une manière essentielle.$n$

Peut-être une meilleure question, plus précise, est de savoir si:

1. il existe un automate borné linéaire qui reconnaît SAT,
2. dont on peut extraire un CSG,
3. de sorte que le langage défini par le CSG est en NP en raison d'une caractéristique de la grammaire (et non parce que nous savons déjà qu'il est en NP)?

Au cours des cinq décennies qui ont suivi, quelqu'un a sûrement essayé de le faire! Comme je ne trouve rien de publié dans ce sens, je serais intéressé à comprendre pourquoi cette approche n'a pas fonctionné, ou un pointeur vers un travail que j'ai manqué.

• Peter S. Landweber, Trois théorèmes sur les grammaires de structure de phrases de type 1 , Information et contrôle 6 (2) 131–136, 1963. doi: 10.1016 / S0019-9958 (63) 90169-4

Bien qu'il ne construise pas directement une grammaire contextuelle pour SAT, l'article suivant pourrait apporter un éclairage.

WC Rounds, Complexity of Recognition in Intermediate Languages , Switching and Automata Theory, 1973, 145-158 http://dx.doi.org/10.1109/SWAT.1973.5

L'article de Rounds donne un automate de pile non déterministe unidirectionnel (1-NSA) reconnaissant SAT, puis montre le problème d'appartenance de 1-NSA (et son sur-ensemble approprié, la grammaire indexée d'Aho) est en général dans NP. En d'autres termes, SAT en tant qu'automate CSL / linéaire limité est spécial dans le sens où il utilise sa mémoire uniquement comme une pile.