En lógica formal , la satisfacibilidad de Horn , o HORNSAT , es el problema de decidir si un conjunto dado de cláusulas de Horn proposicionales es satisfactorio o no. Las cláusulas Horn-satisfiability y Horn llevan el nombre de Alfred Horn .
Definiciones y terminología básicas
Una cláusula de Horn es una cláusula con como máximo un literal positivo , llamado el encabezado 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.
El problema de la satisfacibilidad de Horn se puede resolver en tiempo lineal . [1] El problema de decidir la verdad de las fórmulas de Horn cuantificadas también se puede resolver en tiempo polinomial. [2] Un algoritmo de tiempo polinomial para la satisfacibilidad de Horn se basa en la regla de la propagación unitaria : si la fórmula contiene una cláusula compuesta por un solo literal (una cláusula unitaria), luego todas las cláusulas que contienen (excepto la cláusula de unidad en sí) se eliminan, y todas las cláusulas que contienen tener este literal eliminado. El resultado de la segunda regla puede ser una cláusula unitaria, que se propaga de la misma manera. Si no hay cláusulas unitarias, la fórmula puede satisfacerse simplemente estableciendo todas las variables restantes en negativas. La fórmula no es satisfactoria si esta transformación genera un par de cláusulas unitarias opuestas y . La satisfacibilidad de Horn es en realidad uno de los problemas "más difíciles" o "más expresivos" que se sabe que es computable en tiempo polinomial, en el sentido de que es un problema P -completo . [3]
Este algoritmo también permite determinar una asignación de verdad de fórmulas de Horn satisfactorias: 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 verdadero, donde la comparación se realiza utilizando la contención de conjuntos.
Usando un algoritmo lineal para la propagación unitaria, el algoritmo es lineal en el tamaño de la fórmula.
Una generalización de la clase de fórmulas de Horn es la de las fórmulas de Horn renombrables, que es el conjunto de fórmulas que se pueden colocar en forma de Horn reemplazando algunas variables con su respectiva negación. La verificación de la existencia de tal reemplazo se puede hacer en tiempo lineal; por lo tanto, la satisfacibilidad de tales fórmulas está en P, ya que se puede resolver realizando primero este reemplazo y luego verificando la satisfacibilidad de la fórmula de Horn resultante. [4] [5] [6] [7] La satisfacibilidad de Horn y la satisfacibilidad de Horn renombrable proporcionan una de las dos importantes subclases de satisfacibilidad que se pueden resolver en tiempo polinomial; la otra subclase es 2-satisfacibilidad .
También se puede plantear el problema de satisfacibilidad de Horn para lógicas proposicionales de muchos valores . Los algoritmos no suelen ser lineales, pero algunos son polinomiales; ver Hähnle (2001 o 2003) para una encuesta. [8] [9]
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. Negar todas las variables transforma una instancia de Dual-Horn SAT en Horn SAT. Fue probado en 1951 por el cuerno que dual-Horn SAT está en P .
Ver también
Referencias
- ^ Dowling, William F .; Gallier, Jean H. (1984), "Algoritmos de tiempo lineal para probar la satisfacibilidad de las 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 de fórmulas booleanas cuantificadas". Información y Computación . Elsevier. 117 (1): 12–18. doi : 10.1006 / inco.1995.1025 .
- ^ Stephen Cook; Phuong Nguyen (2010). Fundamentos lógicos de la complejidad de la prueba . Prensa de la Universidad de Cambridge. pag. 224. ISBN 978-0-521-51729-4.
- ^ Lewis, Harry R. (1978). "Cambiar el nombre de un conjunto de cláusulas como un conjunto de cuerno". Revista de la ACM . 25 (1): 134-135. doi : 10.1145 / 322047.322059 . Señor 0468315 ..
- ^ Aspvall, Bengt (1980). "Reconociendo instancias NR (1) disfrazadas del problema de satisfacibilidad". Revista de algoritmos . 1 (1): 97–103. doi : 10.1016 / 0196-6774 (80) 90007-3 . Señor 0578079 .
- ^ Hébrard, Jean-Jacques (1994). "Un algoritmo lineal para cambiar el nombre de un conjunto de cláusulas como un conjunto de Horn". Informática Teórica . 124 (2): 343–350. doi : 10.1016 / 0304-3975 (94) 90015-9 . Señor 1260003 ..
- ^ Chandru, Vijaya; Collette R. Coullard ; Peter L. Hammer; Miguel Montañez; Xiaorong Sun (2005). "Sobre las funciones de Horn renombrables y Horn generalizadas". Anales de Matemáticas e Inteligencia Artificial . 1 (1–4): 33–47. doi : 10.1007 / BF01531069 .
- ^ Reiner Hähnle (2001). "Lógicas avanzadas de muchos valores". En Dov M. Gabbay, Franz Günthner (ed.). Manual de lógica filosófica . 2 (2ª ed.). Saltador. pag. 373. ISBN 978-0-7923-7126-7.
- ^ Reiner Hähnle (2003). "Complejidad de las lógicas multivalentes". En Melvin Fitting, Ewa Orłowska (ed.). Más allá de dos: teoría y aplicaciones de la lógica de valores múltiples . Saltador. ISBN 978-3-7908-1541-2.
Otras lecturas
- 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 .