Estoy considerando el lenguaje de todas las fórmulas lógicas proposicionales satisfactorias, SAT (para asegurarnos de que tenga un alfabeto finito, codificaríamos las letras proposicionales de alguna manera adecuada [editar: las respuestas señalaron que la respuesta a la pregunta puede no ser sólida bajo codificaciones variables, por lo que uno debe ser más específico; consulte mis conclusiones a continuación] ). Mi simple pregunta es
¿ SAT es un lenguaje sin contexto?
Mi primera suposición fue que la respuesta de hoy (principios de 2017) debería ser "Nadie lo sabe, ya que esto se relaciona con preguntas no resueltas en la teoría de la complejidad". Sin embargo, esto no es realmente cierto (ver la respuesta a continuación), aunque tampoco es completamente falso. Aquí hay un breve resumen de las cosas que sabemos (comenzando con algunas cosas obvias).
- SAT no es regular (porque incluso la sintaxis de la lógica proposicional no es regular, debido a paréntesis coincidentes)
- SAT es sensible al contexto (no es difícil dar un LBA para ello)
- SAT es NP-completo (Cook / Levin), y en particular decidido por TM no deterministas en tiempo polinomial.
- SAT también puede ser reconocido por autómatas de pila no deterministas unidireccionales (1-NSA) (ver Rondas WC, Complejidad de reconocimiento en lenguajes de nivel intermedio , Teoría de conmutación y autómatas, 1973, 145-158 http://dx.doi.org/ 10.1109 / SWAT.1973.5 )
- El problema verbal para los lenguajes sin contexto tiene su propia clase de complejidad (ver https://complexityzoo.uwaterloo.ca/Complexity_Zoo:C#cfl )
- , donde LOGCFL es la clase de problemas de espacio de registro reducible a CFL (consultehttps://complexityzoo.uwaterloo.ca/Complexity_Zoo:L#logcfl). Se sabe que NL ⊆ LOGCFL .
Sin embargo, este último punto todavía deja la posibilidad de que se sepa que SAT no está en . En general, no pude encontrar mucho sobre la relación de con la jerarquía que podría ayudar a aclarar el estado epistémico de mi pregunta.
Observación (después de ver algunas respuestas iniciales): no espero que la fórmula esté en forma conjuntiva normal (esto no hará una diferencia en la esencia de la respuesta, y generalmente los argumentos aún se aplican ya que un CNF también es una fórmula. Pero afirme que la versión del número de variables constantes del problema es regular falla, ya que uno necesita paréntesis para la sintaxis).
Conclusión: Contrariamente a mi suposición inspirada en la teoría de la complejidad, uno puede mostrar directamente que SAT no está libre de contexto. La situación por lo tanto es:
- Se sabe que SAT no está libre de contexto (en otras palabras: SAT no está en ), bajo el supuesto de que uno usa una codificación "directa" de fórmulas donde las variables proposicionales se identifican por números binarios (y algunos otros símbolos se utilizan para operadores y separadores).
- No se sabe si SAT está en , pero "la mayoría de los expertos piensan" que no lo está, ya que esto implicaría . Esto también significa que se desconoce si otras codificaciones "razonables" de SAT están libres de contexto (suponiendo que consideremos que el espacio de registro es un esfuerzo de codificación aceptable para un problema NP-difícil).
Tenga en cuenta que estos dos puntos no implican . Esto se puede mostrar directamente al mostrar que hay idiomas en (por lo tanto, en ) que no están libres de contexto (por ejemplo, ).
Respuestas:
Solo una prueba alternativa con una mezcla de resultados bien conocidos
Suponer que:
Por ejemplo, se escribe como: (el operador tiene prioridad sobre ) .φ=(x1∨x2)∧−x3 sφ=+1∨+10∧−11∈S ∨ ∧
Suponga que st la fórmula correspondiente es satisfactoria es CF.L={sφ∈S∣ φ }
Si lo intersectamos con el lenguaje regular: todavía obtenemos un lenguaje CF. También podemos aplicar el homomorfismo: , y el lenguaje sigue siendo CF.R={+1a∧−1b∧−1c∣a,b,c>0} h(+)=ϵ h(−)=ϵ
Pero el lenguaje que obtenemos es: , porque si entonces la fórmula "fuente" es que es insatisfactorio (de manera similar si ). Pero es una conocida contradicción de lenguaje no CF .L′={1a∧1b∧1c∣a≠b,a≠c} a=b +xa∧−xa∧−xb a=c L′ ⇒
fuente
Si el número de variables es finito, también lo es el número de conjunciones satisfactorias, por lo que su lenguaje SAT es finito (y, por lo tanto, regular). [Editar: este reclamo asume el formulario CNFSAT.]
De lo contrario, aceptemos codificar fórmulas como por . Usaremos el lema de Ogden para demostrar que el lenguaje de todas las conjunciones satisfactorias no está libre de contexto.(x17∨¬x21)∧(x1∨x2∨x3) (17+~21)(1+2+3)
Sea la constante de "marcado" en el lema de Ogden, y considere una fórmula sat cuya primera cláusula consiste en , es decir, la codificación de , donde es el número decimal que consiste en unos. Marcamos los unos de y luego exigimos que todos los bombeos de la descomposición apropiada de (ver la conclusión del lema de Ogden) también sean satisfactorios. Pero podemos bloquear esto fácilmente al no requerir ninguna cláusula que contenga , donde es una secuencia de más corta quep w (1p) (xN) N p p 1p w xq q 1 p , ser satisfactoria, por ejemplo, asegurando que cualquier otra cláusula de tenga una negación de cada . Esto significa que falla la propiedad de "bombeo negativo" y concluimos que el lenguaje no está libre de contexto. [Nota: ignoré los casos triviales en los que el bombeo produce cuerdas mal formadas.]w xq w
fuente