Satisfacción

En lógica matemática , una fórmula es satisfacible si es verdadera bajo alguna asignación de valores a sus variables . Por ejemplo, la fórmula es satisfacible porque es verdadera cuando y , mientras que la fórmula no es satisfacible sobre los números enteros. El concepto dual de satisfacibilidad es 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álida sobre los 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 satisfacible si hay alguna interpretación que la hace verdadera. ^[1] Si bien esto permite interpretaciones no estándar de símbolos como , uno puede restringir su significado proporcionando axiomas adicionales . El problema de satisfacibilidad módulo teorías considera la satisfacibilidad de una fórmula con respecto a una teoría formal , que es un conjunto (finito o infinito) de axiomas. ${\estilo de visualización +}$ $x+1=x$ ${\estilo de visualización +}$

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 satisfacible si al menos una interpretación hace que cada fórmula de la teoría sea verdadera, y válida si cada fórmula es verdadera en cada interpretación. Por ejemplo, las teorías de la aritmética como la aritmética de Peano son satisfacibles 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, un resultado conocido como el 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 satisfacible es decidible y se conoce como el problema de satisfacibilidad booleano o SAT. En general, el problema de determinar si una oración de lógica de primer orden es satisfacible no es decidible. En álgebra universal , teoría de ecuaciones y demostración automática de teoremas , se utilizan los métodos de reescritura de términos , cierre de congruencia y unificación para intentar decidir la satisfacibilidad. Si una teoría particular es 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

En el caso de las lógicas clásicas 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álido si y solo si ¬φ es insatisfacible, lo que quiere decir que es falso que ¬φ sea satisfacible. Dicho de otro modo, φ es satisfacible si y solo si ¬φ es inválido.

En el caso de 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 .

Satisfacción 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 lógica de primer orden

Para la lógica de primer orden (LPO), la satisfacibilidad es indecidible . Más específicamente, es un problema co-RE-completo y, por lo tanto, no semidecidible . ^[3] Este hecho tiene que ver con la indecidibilidad del problema de validez para la LPO. La cuestión del estatus del problema de validez fue planteada en primer lugar 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 también fuera un problema semidecidible, entonces el problema de la existencia de contramodelos también lo sería (una fórmula tiene contramodelos si y solo si su negación es satisfacible). Por lo tanto, el problema de la validez lógica sería decidible, lo que contradice el teorema de Church-Turing , un resultado que establece la respuesta negativa para el Entscheidungsproblem.

Satisfacción en la teoría de modelos

En la teoría de modelos , una fórmula atómica es satisfacible 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

A ⊧ φ [a]

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

A ⊧ φ

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

A ⊧ T

Satisfacción 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 de modelo finito , los problemas de satisfacibilidad y satisfacibilidad finita coinciden, pues una fórmula de esa lógica tiene un modelo si y solo si tiene un modelo finito. Esta cuestión es importante en el campo matemático de la teoría de modelos finitos .

En general, la satisfacibilidad finita y la satisfacibilidad no tienen por qué coincidir. Por ejemplo, considere la fórmula lógica de primer orden obtenida como la conjunción de las siguientes oraciones, donde y son constantes : $estilo de visualización a_{0}$ $estilo de visualización a_{1}$

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

La fórmula resultante tiene el modelo infinito , pero se puede demostrar que no tiene modelo finito (empezando por el hecho y siguiendo la cadena de átomos que debe existir por 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 retroceda sobre o sobre un elemento diferente). $R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ $R(a_{0},a_{1})$ ${\estilo de visualización R}$ $estilo de visualización 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, 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 mediante 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 desea maximizar (o minimizar) una función objetivo sujeta a ciertas 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 casos principales.

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

Para las restricciones lineales, la siguiente tabla proporciona una visión más completa.

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

Véase también

Notas

^ Boolos, Burgess y Jeffrey 2007, p. 120: "Un conjunto de oraciones [...] es satisfacible si alguna interpretación [lo hace verdadero]".
^ Franz Baader y Tobias Nipkow (1998). Term Rewriting and All That [Reescritura de términos y todo eso]. Cambridge University Press. 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. pp. 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 de modelos más breve . Cambridge University Press. pág. 12. ISBN 0-521-58713-1.
^ de Alexander Bockmayr; Volker Weispfenning (2001). "Resolución de 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, George; Burgess, John; Jeffrey, Richard (2007). Computabilidad y lógica (5.ª ed.). Cambridge University Press.

Lectura adicional

Daniel Kroening y 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 satisfacibilidad . IOS Press. ISBN 978-1-60750-376-7.