Satisfabilidad - Satisfiability

En lógica matemática , incluida, en particular, la lógica de primer orden y el cálculo proposicional , la satisfacibilidad y la validez son conceptos elementales de la semántica . Una fórmula es satisfactoria si existe una interpretación ( modelo ) que hace que la fórmula sea verdadera. 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 alguna de tales interpretaciones 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 ( problema de satisfacibilidad booleano ). En general, la cuestión de si una oración de lógica de primer orden es satisfactoria 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. Si una teoría en particular es decidible o no depende de si la teoría está libre de variables o de otras condiciones.

Reducción de validez a satisfacibilidad

Para las lógicas clásicas con negación, 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 es falso que ¬φ 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 para la lógica clásica

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

Para la lógica de primer orden (FOL), la satisfacibilidad es indecidible . Más específicamente, se trata de un problema co-RE-completo y, por tanto, no semidecidible . 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 por el teorema de completitud de Gödel . 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. 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 .

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 : ${\ Displaystyle a}$ ${\ Displaystyle b}$

${\ Displaystyle R (a_ {0}, a_ {0})}$
${\ Displaystyle R (a_ {0}, a_ {1})}$
${\ Displaystyle \ forall xy (R (x, y) \ rightarrow \ existe zR (y, z))}$
${\ Displaystyle \ forall xyz (R (y, x) \ wedge R (z, x) \ rightarrow x = z))}$

La fórmula resultante tiene el modelo infinito , pero se puede demostrar que no tiene un modelo finito (partiendo del hecho y siguiendo la cadena de átomos que debe 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 se repita en un elemento diferente o en otro). ${\ Displaystyle R (a_ {0}, a_ {0}), R (a_ {0}, a_ {1}), R (a_ {1}, a_ {2}), \ ldots}$ ${\ Displaystyle R (a, b)}$ ${\ Displaystyle R}$ ${\ Displaystyle a_ {0}}$

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 .

Para la lógica clásica de primer orden , la satisfacibilidad finita es recursivamente enumerable (en la clase RE ) e indecidible por el teorema de Trakhtenbrot aplicado a la negación de la fórmula.

Restricciones numéricas

Las restricciones numéricas a menudo aparecen en el campo de la optimización matemática , donde generalmente 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 )
Polinomio	Decidible mediante, por ejemplo, descomposición algebraica cilíndrica	indecidible ( décimo problema de Hilbert )

Fuente de la tabla: Bockmayr y Weispfenning .

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 .

Ver también

Notas

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.

Languages

In other projects