Le SAT à largeur limitée est-il décidable dans l'espace de journal?

Elberfeld, Jakoby et Tantau 2010 ( ECCC TR10-062 ) se sont révélés une version peu encombrante du théorème de Bodlaender. Ils ont montré que pour les graphiques avec une largeur d'arbre au plus , une décomposition d'arbre de largeur k peut être trouvée en utilisant l'espace logarithmique. Le facteur constant dans l'espace lié dépend de k . (Le théorème de Bodlaender montre une limite de temps linéaire, avec une dépendance exponentielle de k dans le facteur constant.)$k$$k$$k$$k$

SAT devient facile lorsque l'ensemble des clauses a une faible largeur. Plus précisément, Fischer, Makowsky et Ravve 2008 ont montré que la satisfiabilité des formules CNF avec la largeur d'arbre du graphique d'incidence limité par peut être décidée avec au plus 2 O ( k ) n opérations arithmétiques lorsque la décomposition de l'arbre est donnée. Selon le théorème de Bodlaender, le calcul de la décomposition arborescente du graphique d'incidence pour k fixe peut être effectué en temps linéaire, et donc SAT peut être décidé pour des formules de largeur d'arbre bornées dans le temps qui est un polynôme de faible degré dans le nombre de variables n .$k$$2^{O(k)} n$$k$$n$

On pourrait alors s'attendre à ce que SAT soit réellement décidable en utilisant l'espace logarithmique, pour les formules avec une largeur d'arbre bornée du graphique d'incidence. On ne sait pas comment modifier Fischer et al. approche pour décider SAT en quelque chose d'espace-efficace. L'algorithme fonctionne en calculant une expression pour le nombre de solutions, via l'inclusion-exclusion, et en évaluant récursivement le nombre de solutions de formules plus petites. Bien que l'arborescence bornée aide, les sous-formules semblent être trop grandes pour être calculées dans l'espace logarithmique.

Cela m'amène à demander:

SAT est-il connu pour les formules de largeur d'arbre bornée en ou N L ?$\mathsf{L}$$\mathsf{NL}$

En effet, en utilisant les résultats d'Elberfeld-Jakoby-Tantau-2010, on peut montrer que la SAT peut être décidée dans l'espace logarithmique sur des formules dont le graphique d'incidence a limité la largeur d'arbre. Voici un aperçu du déroulement des principales étapes de la preuve de cette affirmation.

1. Les notions de décomposition d'arbre et de largeur d'arbre peuvent être généralisées à des structures relationnelles arbitraires. Voir par exemple les sections 2 et 3 de cet article de Dalmau, Kolaitis et Vardi.
2. Le théorème de Courcelle indique que la logique MSO peut être décidée en temps linéaire sur des structures relationnelles à largeur d'arbre constante.
3. $t$$f(t)\cdot n$
4. $\tau$$F$$I$$\tau$$I$
5. $\tau$
6. Par conséquent, par le théorème de Bodlander + Courcelle, on peut décider si une formule à largeur d'arbre constante est satisfaisable en temps linéaire.
7. Elberfeld-Jakoby-Tantau-2010 montre que le "temps linéaire" peut être remplacé par "l'espace logarithmique" à la fois sur le théorème de Bodlaender et de Courcelle.
8. $\varphi$$\tau$$\tau$$\varphi$
9. En particulier, SAT peut être déterminé dans l'espace de journal sur des graphiques à largeur d'arbre constante.