Satisfacción

En lógica matemática , una fórmula es satisfactoria si es verdadera bajo alguna asignación de valores a sus variables . Por ejemplo, la fórmula es satisfactoria porque es verdadera cuando y , mientras que la fórmula no es satisfactoria para números enteros. El concepto dual de la satisfacibilidad es el de validez ; una fórmula es válida si cada asignación de valores a sus variables hace que la fórmula sea verdadera. Por ejemplo, es válido sobre números enteros, pero no lo es. $x+3=y$ $x=3$ $y=6$ $x+1=x$ $x+3=3+x$ $x+3=y$

Formalmente, la satisfacibilidad se estudia con respecto a una lógica fija que define la sintaxis de los símbolos permitidos, como la lógica de primer orden , la lógica de segundo orden o la lógica proposicional . Sin embargo, en lugar de ser sintáctica, la satisfacibilidad es una propiedad semántica porque se relaciona con el significado de los símbolos, por ejemplo, el significado de en una fórmula como . Formalmente, definimos una interpretación (o modelo ) como una asignación de valores a las variables y una asignación de significado a todos los demás símbolos no lógicos, y se dice que una fórmula es satisfactoria si hay alguna interpretación que la haga verdadera. ^[1] Si bien esto permite interpretaciones no estándar de símbolos como , se puede restringir su significado proporcionando axiomas adicionales . El problema de las teorías del módulo de satisfacibilidad considera la satisfacibilidad de una fórmula con respecto a una teoría formal , que es un conjunto (finito o infinito) de axiomas. $+$ $x+1=x$ $+$

La satisfacibilidad y la validez se definen para una única fórmula, pero pueden generalizarse a una teoría arbitraria o a un conjunto de fórmulas: una teoría es satisfactoria si al menos una interpretación hace verdaderas todas las fórmulas de la teoría, y válida si todas las fórmulas son verdaderas en todas las interpretaciones. . Por ejemplo, las teorías de la aritmética como la aritmética de Peano son satisfactorias porque son verdaderas en los números naturales. Este concepto está estrechamente relacionado con la consistencia de una teoría, y de hecho es equivalente a la consistencia para la lógica de primer orden, resultado conocido como teorema de completitud de Gödel . La negación de la satisfacibilidad es la insatisfacibilidad y la negación de la validez es la invalidez. Estos cuatro conceptos están relacionados entre sí de una manera exactamente análoga al cuadrado de oposición de Aristóteles .

El problema de determinar si una fórmula en lógica proposicional es satisfactible es decidible y se conoce como problema booleano de satisfacibilidad o SAT. En general, el problema de determinar si una oración de lógica de primer orden es satisfactoria no es decidible. En álgebra universal , teoría de ecuaciones y demostración automatizada de teoremas , los métodos de reescritura de términos , cierre de congruencias y unificación se utilizan para intentar decidir la satisfacibilidad. El que una teoría particular sea decidible o no depende de si la teoría está libre de variables y de otras condiciones. ^[2]

Reducción de la validez a la satisfacibilidad.

Para la lógica clásica con negación, generalmente es posible reexpresar la cuestión de la validez de una fórmula en una que implique satisfacibilidad, debido a las relaciones entre los conceptos expresados en el cuadrado de oposición anterior. En particular, φ es válida si y sólo si ¬φ es insatisfactible, es decir, es falso que ¬φ sea satisfacible. Dicho de otra manera, φ es satisfactoria si y sólo 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 satisfacible, mientras que el problema de validez es co-NP completo .

Satisfabilidad 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 .

Satisfacción en la lógica de primer orden

Para la lógica de primer orden (FOL), la satisfacibilidad es indecidible . Más específicamente, es un problema co-RE-completo y, por lo tanto, no es semidecidible . ^[3] Este hecho tiene que ver con la indecidibilidad del problema de validez para FOL. La cuestión del estatus del problema de validez fue planteada por primera vez por David Hilbert , como el llamado Entscheidungsproblem . La validez universal de una fórmula es un problema semidecidible según 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 satisfactible). Por lo tanto, el problema de validez lógica sería decidible, lo que contradice el teorema de Church-Turing , un resultado que establece la respuesta negativa para el problema de Entscheidung.

Satisfacción 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 se escribe comúnmente que

Un ⊧ φ [un]

Si φ no tiene variables libres, es decir, si φ es una oración atómica y se satisface con A , entonces se escribe

Un ⊧ φ

En este caso , también se puede decir que A es un modelo para φ, o que φ es verdadera en A. Si T es una colección de oraciones atómicas (una teoría) satisfechas por A , se escribe

A⊧T

Satisfabilidad 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 haga verdadera. Para una lógica que tiene la propiedad del modelo finito , los problemas de satisfacibilidad y satisfacibilidad finita coinciden, ya que una fórmula de esa lógica tiene un modelo si y sólo 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_ {0}}$ ${\ Displaystyle a_ {1}}$

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

La fórmula resultante tiene el modelo infinito , pero se puede demostrar que no tiene modelo finito (a partir del hecho y siguiendo la cadena de átomos que debe existir según el segundo axioma, la finitud de un modelo requeriría la existencia de un bucle , lo que violaría los axiomas tercero y cuarto, ya sea que se repita sobre o sobre un elemento diferente). ${\ Displaystyle R (a_ {0}, a_ {1}), R (a_ {1}, a_ {2}), \ ldots}$ ${\ Displaystyle R (a_ {0}, a_ {1})}$ $R$ ${\ Displaystyle a_ {0}}$

La complejidad computacional de decidir la satisfacibilidad de 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, sólo 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 según el teorema de Trakhtenbrot aplicado a la negación de la fórmula.

Restricciones numéricas

Las restricciones numéricas ^{[ aclarar ]} aparecen a menudo en el campo de la optimización matemática , donde normalmente se quiere 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 satisfacibles puede ser desafiante o indecidible en algunos entornos. La siguiente tabla resume los principales casos.

Fuente de la tabla: Bockmayr y Weispfenning . ^[5]^{: 754}

Para las restricciones lineales, la siguiente tabla proporciona una imagen más completa.

Fuente de la tabla: Bockmayr y Weispfenning . ^[5]^{: 755}

Ver también

Notas

^ Boolos, Burgess y Jeffrey 2007, pág. 120: "Un conjunto de oraciones [...] es satisfacible si alguna interpretación [las hace verdaderas]".
^ Franz Baader ; Tobías 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". Apuntes de clase: lógica avanzada . Technische Universität Dresden - Instituto de Informática Técnica. págs. 28–32. Archivado desde el original (PDF) el 14 de octubre de 2020 . Consultado el 21 de julio de 2012 .
^ Wilifrid Hodges (1997). Una teoría del modelo más corto . Prensa de la Universidad de Cambridge. pag. 12.ISBN 0-521-58713-1.
^ ab Alexander Bockmayr; Volker Weispfenning (2001). "Resolver restricciones numéricas". En John Alan Robinson; Andréi Voronkov (eds.). Manual de razonamiento automatizado Volumen I. Elsevier y MIT Press. ISBN 0-444-82949-0. (Elsevier) (Prensa MIT).

Referencias

Boolos, George; Burgess, Juan; Jeffrey, Richard (2007). Computabilidad y Lógica (5ª ed.). Prensa de la Universidad de Cambridge.

Otras lecturas

Daniel Kröning ; Oferta Strichman (2008). Procedimientos de decisión: un punto de vista algorítmico . Medios de ciencia y negocios de Springer. ISBN 978-3-540-74104-6.
A. Biere; M. Heule; H. van Maaren; T. Walsh, eds. (2009). Manual de Satisfacibilidad . Prensa IOS. ISBN 978-1-60750-376-7.