En informática, la 2-satisfactibilidad, 2-SAT o simplemente 2SAT es un problema computacional de asignación de valores a variables, cada una de las cuales tiene dos valores posibles, con el fin de satisfacer un sistema de restricciones sobre pares de variables. Es un caso especial del problema general de satisfacción booleana, que puede incluir restricciones sobre más de dos variables, y de los problemas de satisfacción de restricciones, que pueden permitir más de dos opciones para el valor de cada variable. Pero a diferencia de estos problemas más generales, que son NP-completos, la 2-satisfacción puede resolverse en tiempo polinómico.
Las instancias del problema de la 2-satisfactibilidad se expresan normalmente como fórmulas booleanas de un tipo especial, llamadas forma normal conjuntiva (2-CNF) o fórmulas de Krom. También pueden expresarse como un tipo especial de grafo dirigido, el grafo de implicación, que expresa las variables de una instancia y sus negaciones como vértices de un grafo, y las restricciones sobre pares de variables como aristas dirigidas. Ambos tipos de entradas pueden resolverse en tiempo lineal, ya sea mediante un método basado en el backtracking o utilizando los componentes fuertemente conectados del grafo de implicación. La resolución, un método para combinar pares de restricciones con el fin de obtener restricciones válidas adicionales, también conduce a una solución en tiempo polinómico. Los problemas de 2-satisfactibilidad proporcionan una de las dos subclases principales de las fórmulas de forma normal conjuntiva que pueden resolverse en tiempo polinómico; la otra de las dos subclases es la Horn-satisfactibilidad.
La 2-satisfiability puede aplicarse a problemas de geometría y visualización en los que una colección de objetos tiene cada uno dos ubicaciones potenciales y el objetivo es encontrar una colocación para cada objeto que evite solapamientos con otros objetos. Otras aplicaciones incluyen la agrupación de datos para minimizar la suma de los diámetros de los grupos, la programación de clases y deportes, y la recuperación de formas a partir de información sobre sus secciones transversales.
En la teoría de la complejidad computacional, la 2-satisfactibilidad es un ejemplo de problema NL-completo, que puede resolverse de forma no determinista utilizando una cantidad logarítmica de almacenamiento y que se encuentra entre los problemas más difíciles de resolver con este límite de recursos. El conjunto de todas las soluciones a una instancia de 2 satisfacciones puede tener la estructura de un grafo mediano, pero contar estas soluciones es #P-completo y, por tanto, no se espera que tenga una solución en tiempo polinómico. Las instancias aleatorias experimentan una transición de fase brusca de instancias resolubles a instancias irresolubles a medida que la proporción entre restricciones y variables aumenta más allá de 1, un fenómeno conjeturado pero no demostrado para formas más complicadas del problema de la satisfacibilidad. Una variación computacionalmente difícil de la 2-satisfactibilidad, encontrar una asignación de verdad que maximice el número de restricciones satisfechas, tiene un algoritmo de aproximación cuya optimalidad depende de la conjetura de juegos únicos, y otra variación difícil, encontrar una asignación satisfactoria que minimice el número de variables verdaderas, es un importante caso de prueba para la complejidad parametrizada.
Representaciones del problema miniaturadeimagen|El gráfico de implicación para el ejemplo de 2-satisfacciones mostrado en esta sección. Un problema de 2 satisfacciones puede describirse mediante una expresión booleana con una forma restringida especial. Se trata de una conjunción (una operación booleana) de cláusulas, donde cada cláusula es una disyunción (una operación booleana) de dos variables o variables negadas. Las variables o sus negaciones que aparecen en esta fórmula se conocen como literales.Prestwich, Steven (2009), "2. Codificaciones CNF" , en Biere, Armin; Heule, Marijn ; van Maaren, Hans; Walsh, Toby (eds.), Manual de satisfacción , Fronteras en inteligencia artificial y aplicaciones, vol. 185, IOS Press, págs. 75 a 98, doi : 10.3233/978-1-58603-929-5-75 , , Número de identificación del sujeto 31666330 .Por ejemplo, la siguiente fórmula está en forma normal conjuntiva, con siete variables, once cláusulas y 22 literales:
El problema de la 2-satisfacción consiste en encontrar una asignación de verdad a estas variables que haga que toda la fórmula sea verdadera. Tal asignación elige si hacer cada una de las variables verdaderas o falsas, de modo que al menos un literal en cada cláusula se convierte en verdadero. Para la expresión mostrada arriba, una posible asignación satisfactoria es la que hace que las siete variables sean verdaderas. Cada cláusula tiene al menos una variable no negativa, por lo que esta asignación satisface todas las cláusulas. También hay otras 15 formas de asignar todas las variables para que la fórmula sea verdadera. Por lo tanto, la instancia de 2 satisfacciones representada por esta expresión es satisfactible.
Las fórmulas de esta forma se conocen como fórmulas 2-CNF. El "2" en este nombre significa el número de literales por cláusula, y "CNF" significa forma normal conjuntiva, un tipo de expresión booleana en forma de conjunción de disyunciones. También se llaman fórmulas Krom, por el trabajo del matemático de la UC Davis Melven R. Krom, cuyo artículo de 1967 fue uno de los primeros trabajos sobre el problema de la 2-satisfactibilidad.Krom, Melven R. (1967), "El problema de decisión para una clase de fórmulas de primer orden en las que todas las disyunciones son binarias", Zeitschrift für Mathematische Logik und Grundlagen der Mathematik , 13 ( 1– 2): 15– 20, doi : 10.1002/malq.19670130104.
Cada cláusula de una fórmula 2-CNF es lógicamente equivalente a una implicación de una variable o variable negada a la otra. Por ejemplo, la segunda cláusula del ejemplo puede escribirse de tres formas equivalentes:
Debido a esta equivalencia entre estos distintos tipos de operación, una instancia de 2-satisfactible también puede escribirse en forma normal implicativa, en la que sustituimos cada cláusula o de la forma normal conjuntiva por las dos implicaciones a las que es equivalente.Russell, Stuart Jonathan; Norvig, Peter (2010), Inteligencia artificial: un enfoque moderno , serie Prentice Hall sobre inteligencia artificial, Prentice Hall, pág. 282, .
Una tercera forma, más gráfica, de describir una instancia de 2-satisfactible es como un grafo de implicación. Un grafo de implicación es un grafo dirigido en el que hay un vértice por variable o variable negada, y una arista que conecta un vértice con otro siempre que las variables correspondientes estén relacionadas por una implicación en la forma normal implicativa de la instancia. Un grafo de implicación debe ser un grafo sesgado-simétrico, lo que significa que tiene una simetría que lleva cada variable a su negación e invierte las orientaciones de todas las aristas.Aspvall, Bengt; Plass, Michael F.; Tarjan, Robert E. (1979), "Un algoritmo de tiempo lineal para probar la verdad de ciertas fórmulas booleanas cuantificadas" (PDF) , Information Processing Letters , 8 (3): 121– 123, doi : 10.1016/0020-0190(79)90002-4.
Algoritmos Se conocen varios algoritmos para resolver el problema de la 2-satisfacción. Los más eficientes tardan un tiempo lineal.Even, S .; Itai, A.; Shamir, A. (1976), "Sobre la complejidad de los problemas de flujo de múltiples productos y tablas de tiempos", SIAM Journal on Computing , 5 (4): 691– 703, doi : 10.1137/0205048.
Resolución y cierre transitivo Krom (1967) describió el siguiente procedimiento de decisión en tiempo polinómico para resolver instancias de 2-satisfactibilidad.
Supongamos que una instancia de 2 satisfacciones contiene dos cláusulas que utilizan la misma variable x, pero que x está negada en una cláusula y no en la otra. Entonces las dos cláusulas se pueden combinar para producir una tercera cláusula, que tiene los otros dos literales en las dos cláusulas; esta tercera cláusula también debe ser satisfecha siempre que las dos primeras cláusulas sean satisfechas. Esto se llama resolución. Por ejemplo, podemos combinar las cláusulas y para obtener la cláusula , En términos de la forma implicativa de una fórmula 2-CNF, esta regla equivale a encontrar dos implicaciones y e inferir por transitividad una tercera implicación .
Krom escribe que una fórmula es consistente si la aplicación repetida de esta regla de inferencia no puede generar las dos cláusulas y para cualquier variable . Como él demuestra, una fórmula 2-CNF es satisfacible si y sólo si es consistente. Porque, si una fórmula no es consistente, no es posible satisfacer las dos cláusulas y simultáneamente. Y, si es coherente, entonces la fórmula puede ampliarse añadiendo repetidamente una cláusula de la forma o cada vez, manteniendo la coherencia en cada paso, hasta que incluya una cláusula de este tipo para cada variable. En cada uno de estos pasos de ampliación, siempre se puede añadir una de estas dos cláusulas preservando la coherencia, ya que si no, la otra cláusula se podría generar utilizando la regla de inferencia. Una vez que todas las variables tienen una cláusula de esta forma en la fórmula, se puede generar una asignación satisfactoria de todas las variables estableciendo una variable a verdadero si la fórmula contiene la cláusula y poniéndola en falso si la fórmula contiene la cláusula .
Krom se ocupaba principalmente de la completitud de los sistemas de reglas de inferencia, más que de la eficacia de los algoritmos. Sin embargo, su método lleva a un límite de tiempo polinómico para resolver problemas de 2 satisfacciones. Agrupando todas las cláusulas que utilizan la misma variable y aplicando la regla de inferencia a cada par de cláusulas, es posible encontrar todas las inferencias posibles a partir de una instancia 2-CNF dada, y comprobar si es consistente, en un tiempo total , donde es el número de variables de la instancia. Esta fórmula resulta de multiplicar el número de variables por el número de pares de cláusulas que implican una variable dada, a los que se puede aplicar la regla de inferencia. Así, es posible determinar si una instancia 2-CNF dada es satisfacible en tiempo . Dado que encontrar una asignación satisfactoria utilizando el método de Krom implica una secuencia de comprobaciones de consistencia , llevaría un tiempo . Incluso, Itai & Shamir (1976) citan un límite de tiempo más rápido de para este algoritmo, basado en un ordenamiento más cuidadoso de sus operaciones. Sin embargo, incluso este límite de tiempo más pequeño fue mejorado en gran medida por los algoritmos de tiempo lineal posteriores de Even, Itai y Shamir (1976) y Aspvall, Plass y Tarjan (1979).
En términos del grafo de implicación de la instancia de 2-satisfacciones, la regla de inferencia de Krom puede interpretarse como la construcción del cierre transitivo del grafo. Como observa Cook (1971), también puede verse como una instancia del algoritmo Davis-Putnam para resolver problemas de satisfacibilidad utilizando el principio de resolución. Su corrección se deduce de la corrección más general del algoritmo de Davis-Putnam. Su límite de tiempo polinómico se deriva del hecho de que cada paso de resolución aumenta el número de cláusulas de la instancia, que está limitado superiormente por una función cuadrática del número de variables.Cook, Stephen A. (1971), "La complejidad de los procedimientos de demostración de teoremas", Proc. 3rd ACM Symp. Theory of Computing (STOC) , págs. 151– 158, doi : 10.1145/800157.805047 , S2CID 7573663
Backtracking limitado