Satisfacción del cuerno

En lógica formal , la satisfacibilidad de Horn , o HORNSAT , es el problema de decidir si un conjunto dado de cláusulas proposicionales de Horn es satisfacible o no. La satisfacibilidad de Horn y las cláusulas de Horn reciben su nombre de Alfred Horn .

Una cláusula de Horn es una cláusula con como máximo un literal positivo , llamado cabeza de la cláusula, y cualquier número de literales negativos, que forman el cuerpo de la cláusula. Una fórmula de Horn es una fórmula proposicional formada por la conjunción de cláusulas de Horn.

La satisfacibilidad de Horn es en realidad uno de los problemas "más difíciles" o "más expresivos" que se sabe que se pueden calcular en tiempo polinomial, en el sentido de que es un problema P -completo . ^[1]

El problema de satisfacibilidad de Horn también se puede plantear en lógicas proposicionales de múltiples valores . Los algoritmos no suelen ser lineales, pero algunos son polinómicos; véase Hähnle (2001 o 2003) para un estudio. ^[2]^[3]

Algoritmo

El problema de la satisfacibilidad de Horn se puede resolver en tiempo lineal . ^[4] El problema de decidir la verdad de las fórmulas de Horn cuantificadas también se puede resolver en tiempo polinomial. ^[5] Un algoritmo de tiempo polinomial para la satisfacibilidad de Horn es recursivo :

Una primera condición de terminación es una fórmula en la que todas las cláusulas existentes actualmente contienen literales negativos. En este caso, todas las variables que se encuentran actualmente en las cláusulas se pueden establecer como falsas.
Una segunda condición de terminación es una cláusula vacía. En este caso, la fórmula no tiene soluciones.
En los demás casos, la fórmula contiene una cláusula unitaria positiva , por lo que realizamos una propagación unitaria : el literal se establece como verdadero, se eliminan todas las cláusulas que lo contienen y se elimina este literal de todas las cláusulas que lo contienen. El resultado es una nueva fórmula de Horn, por lo que reiteramos. ${\estilo de visualización l}$ ${\estilo de visualización l}$ ${\estilo de visualización l}$ $\neg l$

Este algoritmo también permite determinar una asignación de verdad de fórmulas de Horn que se pueden satisfacer: todas las variables contenidas en una cláusula unitaria se establecen en el valor que satisface esa cláusula unitaria; todos los demás literales se establecen en falso. La asignación resultante es el modelo mínimo de la fórmula de Horn, es decir, la asignación que tiene un conjunto mínimo de variables asignadas a verdaderas, donde la comparación se realiza utilizando la contención de conjuntos.

Utilizando un algoritmo lineal para la propagación de unidades, el algoritmo es lineal en el tamaño de la fórmula.

Ejemplos

Caso trivial

En la fórmula de Horn

(\neg a \lor \neg b \lor c) \land

(\neg b \lor \neg c \lor d) \land

(\neg f \lor \neg a \lor b) \land

(\neg e \lor \neg c \lor a ​​) \land

(\neg e \lor f) \land

(\neg d \lor e) \land

(\neg b \lor \neg c)

,

Cada cláusula tiene un literal negado. Por lo tanto, establecer cada variable como falsa satisface todas las cláusulas, por lo que es una solución.

Caso solucionable

En la fórmula de Horn

(\neg a \lor \neg b \lor c) \land

(\neg b \lor \neg c \lor f) \land

(\neg f \lor b) \land

(\neg e \lor \neg c \lor a ​​) \land

(f) \land

(\neg d \lor e) \land

(\neg b \lor \neg c)

,

Una cláusula obliga a que f sea verdadera. Fijar f como verdadera y simplificar da como resultado

(\neg a \lor \neg b \lor c) \land

(b) \land

(\neg e \lor \neg c \lor a ​​) \land

(\neg d \lor e) \land

(\negb\lor\negc)

.

​

​

Ahora b debe ser verdadero. La simplificación da

(\neg a \lor c) \land

(\neg e \lor \neg c \lor a ​​) \land

(\neg d \lor e) \land

(\neg c)

.

Ahora es un caso trivial, por lo que las variables restantes se pueden establecer en falso. Por lo tanto, una asignación satisfactoria es

a = falso

,

b = verdadero

,

c = falso

,

d = falso

,

e = falso

,

f = verdadero

.

Caso sin solución

En la fórmula de Horn

(\neg a \lor \neg b \lor c) \land

(\neg b \lor \neg c \lor f) \land

(\neg f \lor b) \land

(\neg e \lor \neg c \lor a ​​) \land

(f) \land

(\neg d \lor e) \land

(\neg b)

,

Una cláusula obliga a que f sea verdadera. La simplificación posterior da

(\neg a \lor \neg b \lor c) \land

(b) \land

(\neg e \lor \neg c \lor a ​​) \land

(\neg d \lor e) \land

(\negb)

.

Ahora b tiene que ser verdadero. La simplificación da

(\neg a \lor c) \land

(\neg e \lor \neg c \lor a ​​) \land

(\neg d \lor e) \land

()

.

Obtuvimos una cláusula vacía, por lo tanto la fórmula es insatisfacible.

Generalización

Una generalización de la clase de fórmulas de Horn es la de fórmulas de Horn renombrables, que es el conjunto de fórmulas que se pueden poner en forma de Horn reemplazando algunas variables con su respectiva negación. La comprobación de la existencia de dicho reemplazo se puede realizar en tiempo lineal; por lo tanto, la satisfacibilidad de dichas fórmulas está en P, ya que se puede resolver realizando primero este reemplazo y luego comprobando la satisfacibilidad de la fórmula de Horn resultante. ^[6]^[7]^[8]^[9] La satisfacibilidad de Horn y la satisfacibilidad de Horn renombrable proporcionan una de las dos subclases importantes de satisfacibilidad que se pueden resolver en tiempo polinomial; la otra subclase de este tipo es la 2-satisfacibilidad .

SAT de doble bocina

Una variante dual de Horn SAT es Dual-Horn SAT , en la que cada cláusula tiene como máximo un literal negativo. La negación de todas las variables transforma una instancia de Dual-Horn SAT en Horn SAT. En 1951, Horn demostró que Dual-Horn SAT está en P . ^{[ cita requerida ]}

Véase también

Referencias

^ Stephen Cook; Phuong Nguyen (2010). Fundamentos lógicos de la complejidad de las pruebas. Cambridge University Press. pág. 224. ISBN 978-0-521-51729-4.(Versión borrador del autor de 2008, véase p. 213f)
^ Reiner Hähnle (2001). "Lógicas polivalentes avanzadas". En Dov M. Gabbay, Franz Günthner (ed.). Manual de lógica filosófica. Vol. 2 (2.ª ed.). Springer. pág. 373. ISBN 978-0-7923-7126-7.
^ Reiner Hähnle (2003). "Complejidad de las lógicas multivaluadas". En Melvin Fitting, Ewa Orłowska (ed.). Más allá de dos: teoría y aplicaciones de la lógica multivaluada . Springer. ISBN 978-3-7908-1541-2.
^ Dowling, William F.; Gallier, Jean H. (1984), "Algoritmos de tiempo lineal para probar la satisfacibilidad de fórmulas proposicionales de Horn", Journal of Logic Programming , 1 (3): 267–284, doi : 10.1016/0743-1066(84)90014-1 , MR 0770156
^ Buning, HK; Karpinski, Marek; Flogel, A. (1995). "Resolución para fórmulas booleanas cuantificadas". Información y computación . 117 (1). Elsevier: 12–18. doi : 10.1006/inco.1995.1025 .
^ Lewis, Harry R. (1978). "Renombrar un conjunto de cláusulas como un conjunto de Horn". Revista de la ACM . 25 (1): 134–135. doi : 10.1145/322047.322059 . MR 0468315..
^ Aspvall, Bengt (1980). "Reconocimiento de instancias NR(1) disfrazadas del problema de satisfacibilidad". Journal of Algorithms . 1 (1): 97–103. doi :10.1016/0196-6774(80)90007-3. MR 0578079.
^ Hébrard, Jean-Jacques (1994). "Un algoritmo lineal para renombrar un conjunto de cláusulas como un conjunto de Horn". Ciencias de la Computación Teórica . 124 (2): 343–350. doi :10.1016/0304-3975(94)90015-9. MR 1260003..
^ Chandru, Vijaya; Collette R. Coullard ; Peter L. Hammer; Miguel Montañez; Xiaorong Sun (2005). "Sobre funciones Horn renombrables y funciones Horn generalizadas". Anales de Matemáticas e Inteligencia Artificial . 1 (1–4): 33–47. doi :10.1007/BF01531069.

Lectura adicional

Grädel, Erich; Kolaitis, Phokion G.; Libkin, Leonid; Maarten, Marx; Spencer, Joel ; Vardi, Moshe Y .; Venema, Yde; Weinstein, Scott (2007). Teoría de modelos finitos y sus aplicaciones . Textos en informática teórica. Una serie EATCS. Berlín: Springer-Verlag . ISBN. 978-3-540-00428-8.Zbl 1133.03001 .

[CookNguyen2010-1] Stephen Cook; Phuong Nguyen (2010). Fundamentos lógicos de la complejidad de las pruebas. Cambridge University Press. pág. 224. ISBN 978-0-521-51729-4.(Versión borrador del autor de 2008, véase p. 213f)

[2] Reiner Hähnle (2001). "Lógicas polivalentes avanzadas". En Dov M. Gabbay, Franz Günthner (ed.). Manual de lógica filosófica. Vol. 2 (2.ª ed.). Springer. pág. 373. ISBN 978-0-7923-7126-7.

[FittingOrlowska2003-3] Reiner Hähnle (2003). "Complejidad de las lógicas multivaluadas". En Melvin Fitting, Ewa Orłowska (ed.). Más allá de dos: teoría y aplicaciones de la lógica multivaluada . Springer. ISBN 978-3-7908-1541-2.

[4] Dowling, William F.; Gallier, Jean H. (1984), "Algoritmos de tiempo lineal para probar la satisfacibilidad de fórmulas proposicionales de Horn", Journal of Logic Programming , 1 (3): 267–284, doi : 10.1016/0743-1066(84)90014-1 , MR 0770156

[buningkarpinski-5] Buning, HK; Karpinski, Marek; Flogel, A. (1995). "Resolución para fórmulas booleanas cuantificadas". Información y computación . 117 (1). Elsevier: 12–18. doi : 10.1006/inco.1995.1025 .

[6] Lewis, Harry R. (1978). "Renombrar un conjunto de cláusulas como un conjunto de Horn". Revista de la ACM . 25 (1): 134–135. doi : 10.1145/322047.322059 . MR 0468315..

[7] Aspvall, Bengt (1980). "Reconocimiento de instancias NR(1) disfrazadas del problema de satisfacibilidad". Journal of Algorithms . 1 (1): 97–103. doi :10.1016/0196-6774(80)90007-3. MR 0578079.

[8] Hébrard, Jean-Jacques (1994). "Un algoritmo lineal para renombrar un conjunto de cláusulas como un conjunto de Horn". Ciencias de la Computación Teórica . 124 (2): 343–350. doi :10.1016/0304-3975(94)90015-9. MR 1260003..

[9] Chandru, Vijaya; Collette R. Coullard ; Peter L. Hammer; Miguel Montañez; Xiaorong Sun (2005). "Sobre funciones Horn renombrables y funciones Horn generalizadas". Anales de Matemáticas e Inteligencia Artificial . 1 (1–4): 33–47. doi :10.1007/BF01531069.