SAT en teoría de modelos finitos sin orden

Es bien sabido en la teoría de modelos finitos que sin un orden en la entrada, la expresividad es muy limitada. Por ejemplo, se sabe que es igual a PSPACE , y F O ( PFP ) (sin ningún orden en la entrada) es solo PSPACE -relacional, una noción definida por Abiteboul y Vianu cuando demostraron su teorema : F O ( IFP , < ) = F O ( PFP , < ) iff F O ( $FO(<,\textit{PFP})$$FO(\textit{PFP})$$FO(\textit{IFP},<)=FO(\textit{PFP},<)$ . (EquivalentementeP=PSPACEsifP-relacional=PSÄCE-relacional).$FO(\textit{IFP})=FO(\textit{PFP})$

Las máquinas relacionales son máquinas de Turing con un número finito de relaciones. Como en una base de datos, una relación es un conjunto de tuplas de elementos de un universo finito. La máquina puede verificar si una relación está vacía (si una tabla está vacía), realizar operaciones booleanas sobre las relaciones (unión, intersección, unión, proyección) y las operaciones habituales de la máquina de Turing. Tenga en cuenta que la entrada de máquinas relacionales se da en las relaciones y no en la cinta. Es bien sabido que PSPACE -relacional ( ) ni siquiera puede calcular la paridad, por lo tanto, es menos expresivo que PSPACE .$FO(\textit{PFP})$

Se pueden definir consultas con máquinas relacionales, pero también se pueden definir funciones, siendo la respuesta de una función el contenido de algunas relaciones y de la cinta al final del cálculo. Tal máquina tiene la propiedad de que si hay dos elementos y b de la entrada de tal manera que no es un isomorfismo φ el envío de un a b y b a una , entonces nunca es posible distinguir una de b . En particular en cada relación R de la salida, si R ( a , ¯ x ) es verdadero, entonces $a$$b$$\phi$$a$$b$$b$$a$$a$$b$$R$$R(a,\overline x)$ también lo es.$R(b,\phi(\overline x))$

La razón de esto es que las operaciones permitidas (unión, intersección, proyección y unión) respetan el isomorfismo. Por lo tanto, la salida respeta cada isomorfismo respetado por la entrada.

En , un y b son simétricas, y la función φ de conmutación de una y b es claramente un isomorfismo de la entrada. Suponga que existe una función para calcular asignaciones satisfactorias para instancias 3 - S A T , y cuya salida es P (el conjunto de variables asignadas a verdadero en una asignación correcta). Entonces nos gustaría tener P = { a } o $(a\lor b)\land(\neg a\lor\neg b)$$a$$b$$\phi$$a$$b$$3-SAT$$P$$P=\{a\}$ . Sin embargo, el isomorfismo significa que P contiene tanto a como b , o ninguno.$P=\{b\}$$P$$a$$b$

Por lo tanto, hemos demostrado que no existe una función relacional PSPACE que pueda generar una asignación a una instancia de 3-SAT.

Mi pregunta es: ¿cómo demuestra que no hay un PSPACE -relacional (es decir, ) que acepta solo la entrada que tiene una asignación satisfactoria? La cuestión es diferente, ya que no tengo la intención de calcular la asignación y no pido para ver una o B en la salida, sólo quiero ver "aceptar" o "rechazar. Y, contrariamente al mundo habitual de las máquinas de Turing , no es equivalente saber si existe una respuesta y encontrar la respuesta, porque no hay forma de que usemos nuestra máquina relacional para la pregunta "¿hay una respuesta con a = t r u e " porque no podemos diferenciar $FO(\textit{PFP})$$a$$b$$a=true$$a$de .$b$

El método estándar para mostrar resultados de inexpresibilidad para FO (PFP) (y para FO (LFP), por cierto) es utilizar el hecho de que FO (PFP) está incrustado en la lógica infinita de variable finita . Aquí L ω ∞ ω es el fragmento de variable finita de L ∞ ω , donde este último es la clase de fórmulas (infinitarias) construidas a partir de los átomos mediante negaciones, disyunciones finitarias o infinitarias y conjunciones del tipo ⋁ i ϕ i y ⋀ i ϕ i , y cuantificación existencial y universal. La lógica L k ∞ $\mathrm{L}^\omega_{\infty\omega}$$\mathrm{L}^\omega_{\infty\omega}$$\mathrm{L}_{\infty\omega}$$\bigvee_i \phi_i$$\bigwedge_i \phi_i$$\mathrm{L}^k_{\infty\omega}$es la colección de todas las fórmulas en que involucran a lo sumo k variables (cuantificadas o no), y L ω ∞ ω = ⋃ k L k ∞ ω .$\mathrm{L}_{\infty\omega}$$k$$\mathrm{L}^\omega_{\infty\omega} = \bigcup_k \mathrm{L}^k_{\infty\omega}$

Se sabe que FO (PFP) (ver Teorema 7.4.2 en el libro "Teoría de modelos finitos" de Ebbinghaus y Flum). Por lo tanto, si demuestra que algo no es expresable en L k ∞ ω para cualquier k , entonces también demuestra que no es expresable en FO (PFP).$\subseteq \mathrm{L}^\omega_{\infty\omega}$$\mathrm{L}^k_{\infty\omega}$$k$

Ahora, ¿cómo se prueban los resultados de inexpresibilidad para ? Al jugar los juegos de k- pebble. Estos son juegos de tipo Ehrenfeucht-Fraissé donde el número de rondas es ilimitado pero cada jugador tiene como máximo k guijarros que puede reutilizar (vea el libro Ebbinghaus y Flum nuevamente para más detalles).$\mathrm{L}^k_{\infty\omega}$$k$$k$

Después de todos estos antecedentes, ahora podemos mostrar que CNF-SAT no es expresable en para ninguna k . Para cada k fija , necesitamos encontrar una fórmula CNF satisfactoria F k y una fórmula CNF insatisfactoria G k tal que F k ≡ k ∞ ω G k , donde A ≡ k ∞ ω B significa que el Duplicador tiene una estrategia ganadora para ganar el juego k- pebble en las estructuras A y $\mathrm{L}^k_{\infty\omega}$$k$$k$$F_k$$G_k$$F_k \equiv^k_{\infty\omega} G_k$$A \equiv^k_{\infty\omega} B$$k$$A$$B$(aquí necesitamos arreglar alguna forma sensata de codificar fórmulas CNF como estructuras finitas: digamos que las codificamos como su gráfico de incidencia bipartita con elementos que representan cláusulas en un lado, elementos que representan variables en el otro y 2 tipos de relaciones binarias que indican qué las variables aparecen en qué cláusulas y bajo qué signo). REIVINDICACIONES que una elección explícita de y G k es posible. Pero en cambio, te daré una prueba indirecta.$F_k$$G_k$

$K_k \equiv^k_{\infty\omega} K_{k+1}$$K_a$$a$$\mathrm{L}^\omega_{\infty\omega}$$\mathrm{L}^\omega_{\infty\omega}$