¿El SAT de ancho acotado se puede decidir en el espacio de registro?

Elberfeld, Jakoby y Tantau 2010 ( ECCC TR10-062 ) demostraron una versión eficiente del espacio del teorema de Bodlaender. Demostraron que para los gráficos con ancho de árbol como máximo , se puede encontrar una descomposición de árbol de ancho k usando espacio logarítmico. El factor constante en el espacio limitado depende de k . (El teorema de Bodlaender muestra un límite de tiempo lineal, con una dependencia exponencial de k en el factor constante).$k$$k$$k$$k$

SAT se vuelve fácil cuando el conjunto de cláusulas tiene poco ancho. Específicamente, Fischer, Makowsky y Ravve 2008 mostraron que la satisfacción de las fórmulas CNF con el ancho de árbol del gráfico de incidencia limitado por puede decidirse como máximo con 2 O ( k ) n operaciones aritméticas cuando se da la descomposición del árbol. Según el teorema de Bodlaender, calcular la descomposición del árbol del gráfico de incidencia para k fijo se puede hacer en tiempo lineal y, por lo tanto, se puede decidir SAT para fórmulas de ancho de árbol acotado en el tiempo que es un polinomio de bajo grado en el número de variables n .$k$$2^{O(k)} n$$k$$n$

Entonces se podría esperar que el SAT en realidad sea decidible usando el espacio logarítmico, para fórmulas con ancho de árbol acotado del gráfico de incidencia. No está claro cómo modificar Fischer et al. enfoque para decidir SAT en algo de espacio eficiente. El algoritmo funciona calculando una expresión para el número de soluciones, mediante inclusión-exclusión, y evaluando recursivamente el número de soluciones de fórmulas más pequeñas. Aunque el ancho de árbol acotado sí ayuda, las subformulas parecen ser demasiado grandes para computarlas en el espacio logarítmico.

Esto me lleva a preguntar:

¿Se sabe que SAT para fórmulas de ancho de árbol acotado está en o N L ?$\mathsf{L}$$\mathsf{NL}$

De hecho, utilizando los resultados en Elberfeld-Jakoby-Tantau-2010 se puede demostrar que el SAT se puede decidir en el espacio de registro en fórmulas cuyo gráfico de incidencia ha limitado el ancho del árbol. Aquí hay un bosquejo de cómo van los pasos principales de la prueba de este reclamo.

1. Las nociones de descomposición de árbol y ancho de árbol se pueden generalizar a estructuras relacionales arbitrarias. Véanse, por ejemplo, las secciones 2 y 3 de este documento de Dalmau, Kolaitis y Vardi.
2. El teorema de Courcelle establece que la lógica MSO se puede decidir en tiempo lineal en estructuras relacionales de ancho de árbol constante.
3. $t$$f(t)\cdot n$
4. $\tau$$F$$I$$\tau$$I$
5. $\tau$
6. Por lo tanto, según el teorema de Bodlander + Courcelle, uno puede decidir si una fórmula de ancho de árbol constante es satisfactoria en tiempo lineal.
7. Elberfeld-Jakoby-Tantau-2010 muestra que el "tiempo lineal" puede ser reemplazado por el "espacio logarítmico" tanto en el teorema de Bodlaender como en el de Courcelle.
8. $\varphi$$\tau$$\tau$$\varphi$
9. En particular, SAT se puede determinar en el espacio de registro en gráficos de ancho de árbol constante.