En lógica matemática , satisfacibilidad y validez son conceptos elementales de semántica . Una fórmula es satisfactoria si es posible encontrar una interpretación ( modelo ) que la haga verdadera. [1] Una fórmula es válida si todas las interpretaciones hacen que la fórmula sea verdadera. Los opuestos de estos conceptos son insatisfacción e invalidez , es decir, una fórmula es insatisfactoria si ninguna de las interpretaciones hace que la fórmula sea verdadera e inválida.si tal interpretación hace que la fórmula sea falsa. Estos cuatro conceptos están relacionados entre sí de una manera exactamente análoga a Aristóteles 's cuadrado de oposición .
Los cuatro conceptos pueden plantearse para aplicarlos a teorías completas : una teoría es satisfactoria (válida) si una (todas) de las interpretaciones hace que cada uno de los axiomas de la teoría sea verdadero, y una teoría es insatisfactoria (inválida) si todos (una) de las interpretaciones hace que uno de los axiomas de la teoría sea falso.
También es posible considerar solo las interpretaciones que hacen verdaderos todos los axiomas de una segunda teoría. Esta generalización se denomina comúnmente teorías de módulo de satisfacibilidad .
La cuestión de si una oración en lógica proposicional es satisfactoria es un problema decidible . En general, la cuestión de si las oraciones en lógica de primer orden son satisfactorias no es decidible. En el álgebra universal y la teoría de ecuaciones , los métodos de reescritura de términos , cierre de congruencia y unificación se utilizan para intentar decidir la satisfacibilidad. El que una teoría en particular sea decidible o no depende de si la teoría está libre de variables o de otras condiciones. [2]
Reducción de la validez a la satisfacibilidad
Para la lógica clásica , generalmente es posible volver a expresar la cuestión de la validez de una fórmula a una que implique satisfacibilidad, debido a las relaciones entre los conceptos expresados en el cuadrado de oposición anterior. En particular, φ es válido si y sólo si ¬φ es insatisfactorio, lo que quiere decir que no es cierto que ¬ satisf sea satisfactorio. Dicho de otra manera, φ es satisfactorio si y solo si ¬φ no es válido.
Para las lógicas sin negación, como el cálculo proposicional positivo , las cuestiones de validez y satisfacibilidad pueden no estar relacionadas. En el caso del cálculo proposicional positivo , el problema de satisfacibilidad es trivial, ya que toda fórmula es satisfactoria, mientras que el problema de validez es co-NP completo .
Satisfacibilidad proposicional
En el caso de la lógica proposicional clásica , la satisfacibilidad es decidible para fórmulas proposicionales. En particular, la satisfacibilidad es un problema NP-completo y es uno de los problemas más estudiados en la teoría de la complejidad computacional .
Satisfabilidad en lógica de primer orden
La satisfacción es indecidible y, de hecho, ni siquiera es una propiedad semidecidible de las fórmulas en lógica de primer orden (FOL). [3] Este hecho tiene que ver con la indecidibilidad del problema de validez de FOL. La cuestión del estado del problema de validez fue planteada en primer lugar por David Hilbert , como el llamado problema de Entscheidung . La validez universal de una fórmula es un problema semidecidible. Si la satisfacibilidad fuera también un problema semidecidible, entonces el problema de la existencia de contramodelos también lo sería (una fórmula tiene contramodelos si su negación es satisfactoria). Entonces, el problema de la validez lógica sería decidible, lo que contradice el teorema de Church-Turing , un resultado que indica la respuesta negativa para el problema de Entscheidung.
Satisfabilidad en la teoría de modelos
En la teoría de modelos , una fórmula atómica es satisfactoria si hay una colección de elementos de una estructura que hacen que la fórmula sea verdadera. [4] Si A es una estructura, φ es una fórmula y a es una colección de elementos, tomados de la estructura, que satisfacen φ, entonces comúnmente se escribe que
- A ⊧ φ [a]
Si φ no tiene variables libres, es decir, si φ es una oración atómica , y A la satisface , entonces se escribe
- A ⊧ φ
En este caso, también se puede decir que A es un modelo para φ, o que φ es verdadera en una . Si T es una colección de oraciones atómicas (una teoría) satisfechas por A , se escribe
- A ⊧ T
Satisfacibilidad finita
Un problema relacionado con la satisfacibilidad es el de la satisfacibilidad finita , que es la cuestión de determinar si una fórmula admite un modelo finito que la hace verdadera. Para una lógica que tiene la propiedad de modelo finito , los problemas de satisfacibilidad y satisfacibilidad finita coinciden, ya que una fórmula de esa lógica tiene un modelo si y solo si tiene un modelo finito. Esta pregunta es importante en el campo matemático de la teoría de modelos finitos .
Sin embargo, la satisfacibilidad finita y la satisfacibilidad no tienen por qué coincidir en general. Por ejemplo, considere la fórmula lógica de primer orden obtenida como la conjunción de las siguientes oraciones, donde y son constantes :
La fórmula resultante tiene el modelo infinito , pero se puede demostrar que no tiene un modelo finito (comenzando por el hecho y siguiendo la cadena de átomos que deben existir por el tercer axioma, la finitud de un modelo requeriría la existencia de un bucle, lo que violaría el cuarto axioma, ya sea que vuelva en bucle o en un elemento diferente).
La complejidad computacional de decidir la satisfacibilidad para una fórmula de entrada en una lógica dada puede diferir de la de decidir la satisfacibilidad finita; de hecho, para algunas lógicas, solo una de ellas es decidible .
Restricciones numéricas
Las restricciones numéricas aparecen a menudo en el campo de la optimización matemática , donde normalmente se desea maximizar (o minimizar) una función objetivo sujeta a algunas restricciones. Sin embargo, dejando de lado la función objetivo, la cuestión básica de simplemente decidir si las restricciones son satisfactorias puede ser desafiante o indecidible en algunos entornos. La siguiente tabla resume los principales casos.
Restricciones | sobre reales | sobre enteros |
---|---|---|
Lineal | PTIME (ver programación lineal ) | NP-completo (ver programación de enteros ) |
No lineal | decidible | indecidible ( décimo problema de Hilbert ) |
Fuente de la tabla: Bockmayr y Weispfenning . [5] : 754
Para las restricciones lineales, la siguiente tabla proporciona una imagen más completa.
Restricciones sobre: | racionales | enteros | números naturales |
---|---|---|---|
Ecuaciones lineales | PTIME | PTIME | NP-completo |
Desigualdades lineales | PTIME | NP-completo | NP-completo |
Fuente de la tabla: Bockmayr y Weispfenning . [5] : 755
Ver también
- 2-satisfacibilidad
- Problema de satisfacibilidad booleano
- Satisfacción del circuito
- Los 21 problemas NP-completos de Karp
- Validez
- Satisfacción de restricciones
- Satisfactorio
Notas
- ^ Véase, por ejemplo, Boolos y Jeffrey, 1974, capítulo 11.
- ^ Franz Baader ; Tobias Nipkow (1998). Reescritura de términos y todo eso . Prensa de la Universidad de Cambridge. págs. 58–92. ISBN 0-521-77920-0.
- ^ Baier, Christel (2012). "Capítulo 1.3 Indecidibilidad de FOL" (PDF) . Notas de la clase - Lógica avanzada . Technische Universität Dresden - Instituto de Informática Técnica. págs. 28–32 . Consultado el 21 de julio de 2012 . CS1 maint: parámetro desalentado ( enlace )[ enlace muerto ]
- ^ Wilifrid Hodges (1997). Una teoría del modelo más corta . Prensa de la Universidad de Cambridge. pag. 12. ISBN 0-521-58713-1.
- ^ a b Alexander Bockmayr; Volker Weispfenning (2001). "Resolver restricciones numéricas". En John Alan Robinson; Andrei Voronkov (eds.). Manual de razonamiento automatizado Volumen I . Elsevier y MIT Press. ISBN 0-444-82949-0. (Elsevier) (MIT Press).
Referencias
- Boolos y Jeffrey, 1974. Computability and Logic . Prensa de la Universidad de Cambridge.
Otras lecturas
- Daniel Kroening ; Ofer Strichman (2008). Procedimientos de decisión: un punto de vista algorítmico . Springer Science & Business Media. ISBN 978-3-540-74104-6.
- A. Biere; M. Heule; H. van Maaren; T. Walsh, eds. (2009). Manual de satisfacción . IOS Press. ISBN 978-1-60750-376-7.