Núcleo insatisfactorio

En lógica matemática , dada una fórmula proposicional booleana insatisfacible en forma normal conjuntiva , un subconjunto de cláusulas cuya conjunción todavía es insatisfacible se denomina núcleo insatisfacible de la fórmula original.

Muchos solucionadores SAT pueden generar un gráfico de resolución que demuestra la insatisfacción del problema original. Esto se puede analizar para generar un núcleo insatisfactorio más pequeño.

Un núcleo insatisfactorio se denomina núcleo insatisfactorio mínimo si cada subconjunto propio (permitiendo la eliminación de cualquier cláusula o cláusulas arbitrarias) del mismo es satisfacible. Por lo tanto, dicho núcleo es un mínimo local , aunque no necesariamente global. Existen varios métodos prácticos para calcular núcleos insatisfactorios mínimos. ^[1]^[2]

Un núcleo mínimo insatisfactorio contiene el menor número de cláusulas originales que se requieren para que sigan siendo insatisfactorias. No se conocen algoritmos prácticos para calcular el núcleo mínimo insatisfactorio, ^[3] y calcular un núcleo mínimo insatisfactorio de una fórmula de entrada en forma normal conjuntiva es un problema completo. ^[4] Nótese la terminología: mientras que el núcleo mínimo insatisfactorio era un problema local con una solución fácil, el núcleo mínimo insatisfactorio es un problema global sin una solución fácil conocida. $\Sigma _{2}^{\mathsf {P}}$

Referencias

^ Dershowitz, N.; Hanna, Z.; Nadel, A. (2006). "Un algoritmo escalable para la extracción mínima de núcleos insatisfactorios" (PDF) . En Biere, A.; Gomes, CP (eds.). Teoría y aplicaciones de las pruebas de satisfacibilidad — SAT 2006. Apuntes de clase en informática. Vol. 4121. Springer. págs. 36–41. arXiv : cs/0605085 . CiteSeerX 10.1.1.101.5209 . doi :10.1007/11814948_5. ISBN . 978-3-540-37207-3. Número de identificación del sujeto 2845982.
^ Szeider, Stefan (diciembre de 2004). "Las fórmulas mínimas insatisfactorias con una diferencia entre cláusulas y variables acotadas son manejables con parámetros fijos". Journal of Computer and System Sciences . 69 (4): 656–674. CiteSeerX 10.1.1.634.5311 . doi :10.1016/j.jcss.2004.04.009.
^ Liffiton, MH; Sakallah, KA (2008). "Algoritmos para calcular subconjuntos mínimos insatisfactorios de restricciones" (PDF) . J Autom Reason . 40 : 1–33. CiteSeerX 10.1.1.79.1304 . doi :10.1007/s10817-007-9084-z. S2CID 11106131.
^ "Complejidad de cálculo del núcleo mínimo insatisfactorio". Theoretical Computer Science Stack Exchange . Consultado el 24 de septiembre de 2024 .

[1] Dershowitz, N.; Hanna, Z.; Nadel, A. (2006). "Un algoritmo escalable para la extracción mínima de núcleos insatisfactorios" (PDF) . En Biere, A.; Gomes, CP (eds.). Teoría y aplicaciones de las pruebas de satisfacibilidad — SAT 2006. Apuntes de clase en informática. Vol. 4121. Springer. págs. 36–41. arXiv : cs/0605085 . CiteSeerX 10.1.1.101.5209 . doi :10.1007/11814948_5. ISBN . 978-3-540-37207-3. Número de identificación del sujeto 2845982.

[2] Szeider, Stefan (diciembre de 2004). "Las fórmulas mínimas insatisfactorias con una diferencia entre cláusulas y variables acotadas son manejables con parámetros fijos". Journal of Computer and System Sciences . 69 (4): 656–674. CiteSeerX 10.1.1.634.5311 . doi :10.1016/j.jcss.2004.04.009.

[3] Liffiton, MH; Sakallah, KA (2008). "Algoritmos para calcular subconjuntos mínimos insatisfactorios de restricciones" (PDF) . J Autom Reason . 40 : 1–33. CiteSeerX 10.1.1.79.1304 . doi :10.1007/s10817-007-9084-z. S2CID 11106131.

[4] "Complejidad de cálculo del núcleo mínimo insatisfactorio". Theoretical Computer Science Stack Exchange . Consultado el 24 de septiembre de 2024 .