2-satisfacibilidad

En informática , la 2-satisfacibilidad , 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, para satisfacer un sistema de restricciones sobre pares de variables. Es un caso especial del problema general de satisfacibilidad booleana , que puede implicar restricciones sobre más de dos variables, y de los problemas de satisfacción de restricciones , que pueden permitir más de dos elecciones para el valor de cada variable. Pero a diferencia de esos problemas más generales, que son NP-completos , la 2-satisfacibilidad se puede resolver en tiempo polinomial .

Las instancias del problema de 2-satisfacibilidad se expresan típicamente como fórmulas booleanas de un tipo especial, llamadas fórmulas de forma normal conjuntiva (2-CNF) o fórmulas de Krom . Alternativamente, pueden expresarse como un tipo especial de gráfico dirigido , el gráfico de implicación , que expresa las variables de una instancia y sus negaciones como vértices en un gráfico, y restricciones en pares de variables como aristas dirigidas. Ambos tipos de entradas pueden resolverse en tiempo lineal , ya sea mediante un método basado en retroceso o utilizando los componentes fuertemente conectados del gráfico de implicación. La resolución , un método para combinar pares de restricciones para crear restricciones válidas adicionales, también conduce a una solución en tiempo polinomial. Los problemas de 2-satisfacibilidad proporcionan una de las dos subclases principales de las fórmulas de forma normal conjuntiva que se pueden resolver en tiempo polinomial; la otra de las dos subclases es la satisfacibilidad de Horn .

La 2-satisfacibilidad se puede aplicar a problemas de geometría y visualización en los que una colección de objetos tiene dos posibles ubicaciones y el objetivo es encontrar una ubicación para cada objeto que evite superposiciones 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-satisfacibilidad proporciona un ejemplo de un problema NL-completo , uno que se puede resolver de forma no determinista utilizando una cantidad logarítmica de almacenamiento y que está entre los problemas más difíciles de resolver en este límite de recursos. Al conjunto de todas las soluciones a una instancia de 2-satisfacibilidad se le puede dar la estructura de un gráfico mediano , pero contar estas soluciones es #P-completo y, por lo tanto, no se espera que tenga una solución de tiempo polinomial. Las instancias aleatorias experimentan una transición de fase aguda de instancias resolubles a instancias no resolubles a medida que la relación entre restricciones y variables aumenta más allá de 1, un fenómeno conjeturado pero no probado para formas más complicadas del problema de satisfacibilidad. Una variación computacionalmente difícil de la 2-satisfacibilidad, 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 caso de prueba importante para la complejidad parametrizada .

Un problema de 2-satisfacibilidad puede describirse utilizando una expresión booleana con una forma restringida especial. Es una conjunción (una operación booleana y ) de cláusulas , donde cada cláusula es una disyunción (una operación booleana o ) de dos variables o variables negadas. Las variables o sus negaciones que aparecen en esta fórmula se conocen como literales . ^[1] Por ejemplo, la siguiente fórmula está en forma normal conjuntiva, con siete variables, once cláusulas y 22 literales:$${\displaystyle {\begin{aligned}&(x_{0}\lor x_{2})\land (x_{0}\lor \lno x_{3})\land (x_{1}\lor \lno x_{3})\land (x_{1}\lor \lno x_{4})\land {}\\&(x_{2}\lor \lno x_{4})\land {}(x_{0}\lor \lno x_{5})\land (x_{1}\lor \lno x_{5})\land (x_{2}\lor \lno x_{5})\land {}\\&(x_{3}\lor x_{6})\land (x_{4}\lor x_{6})\land (x_{5}\lor x_{6}).\end{aligned}}}$$

El problema de 2-satisfacibilidad consiste en encontrar una asignación de verdad para estas variables que haga que toda la fórmula sea verdadera. Dicha asignación elige si cada una de las variables será verdadera o falsa, de modo que al menos un literal en cada cláusula se vuelva verdadero. Para la expresión que se muestra arriba, una posible asignación satisfactoria es la que establece las siete variables como verdaderas. Cada cláusula tiene al menos una variable no negada, por lo que esta asignación satisface cada cláusula. También hay otras 15 formas de establecer todas las variables para que la fórmula se vuelva verdadera. Por lo tanto, la instancia de 2-satisfacibilidad representada por esta expresión es satisfacible.

Las fórmulas en esta forma se conocen como fórmulas 2-CNF. El "2" en este nombre representa 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. ^[1] También se denominan fórmulas de Krom, en honor al 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 2-satisfacibilidad. ^[2]

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 cualquiera de las tres formas equivalentes: Debido a esta equivalencia entre estos diferentes tipos de operación, una instancia de 2-satisfacibilidad también puede escribirse en forma normal implicativa, en la que reemplazamos cada cláusula o en la forma normal conjuntiva por las dos implicaciones a las que es equivalente. ^[3]$${\displaystyle (x_{0}\lor \lno x_{3})\;\equiv \;(\lno x_{0}\Rightarrow \lno x_{3})\;\equiv \;(x_{3}\Rightarrow x_{0}).}$$

Una tercera forma, más gráfica, de describir una instancia de 2-satisfacibilidad es como un gráfico de implicación . Un gráfico de implicación es un gráfico 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 gráfico de implicación debe ser un gráfico antisimé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. ^[4]

Se conocen varios algoritmos para resolver el problema de 2-satisfacibilidad. El más eficiente de ellos requiere un tiempo lineal . ^{[2] [4] [5]}

Krom (1967) describió el siguiente procedimiento de decisión de tiempo polinomial para resolver instancias de 2-satisfacibilidad. ^[2]

Supongamos que una instancia de 2-satisfacibilidad contiene dos cláusulas que usan la misma variable x , pero que x se niega en una cláusula y no en la otra. Entonces las dos cláusulas pueden combinarse para producir una tercera cláusula, que tiene los otros dos literales en las dos cláusulas; esta tercera cláusula también debe satisfacerse siempre que se satisfagan las dos primeras cláusulas. Esto se llama resolución . Por ejemplo, podemos combinar las cláusulas y de esta manera para producir 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 . ^[2]${\displaystyle (a\lob)}$${\displaystyle (\lno b\lo \lno c)}$${\displaystyle (a\lor \lno c)}$${\displaystyle \lno es a\Flecha derecha b}$${\displaystyle b\Flecha derecha \lno c}$${\displaystyle \lno es a\Rightarrow \lno es c}$

Krom escribe que una fórmula es consistente si la aplicación repetida de esta regla de inferencia no puede generar ambas cláusulas y , para cualquier variable . Como demuestra, una fórmula 2-CNF es satisfacible si y solo si es consistente. Porque, si una fórmula no es consistente, no es posible satisfacer ambas cláusulas y simultáneamente. Y, si es consistente, entonces la fórmula puede extenderse agregando repetidamente una cláusula de la forma o a la vez, preservando la consistencia en cada paso, hasta que incluya dicha cláusula para cada variable. En cada uno de estos pasos de extensión, siempre se puede agregar una de estas dos cláusulas mientras se preserva la consistencia, porque si no, entonces la otra cláusula podría generarse usando 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 como verdadera si la fórmula contiene la cláusula y estableciéndola como falsa si la fórmula contiene la cláusula . ^[2]${\displaystyle (x\lor x)}$${\displaystyle (\lno x\lor \lno x)}$${\estilo de visualización x}$${\displaystyle (x\lor x)}$${\displaystyle (\lno x\lor \lno x)}$${\displaystyle (x\lor x)}$${\displaystyle (\lno x\lor \lno x)}$${\estilo de visualización x}$${\displaystyle (x\lor x)}$${\displaystyle (\lno x\lor \lno x)}$

Krom se interesó principalmente por la completitud de los sistemas de reglas de inferencia, más que por la eficiencia de los algoritmos. Sin embargo, su método conduce a un límite de tiempo polinomial para resolver problemas de 2-satisfacibilidad. Al agrupar todas las cláusulas que utilizan la misma variable y aplicar la regla de inferencia a cada par de cláusulas, es posible encontrar todas las inferencias que son posibles a partir de una instancia de 2-CNF dada, y comprobar si es consistente, en un tiempo total O( n ³ ) , donde n es el número de variables en la instancia. Esta fórmula proviene de multiplicar el número de variables por el número O( n ² ) de pares de cláusulas que involucran una variable dada, a los que se puede aplicar la regla de inferencia. Por lo tanto, es posible determinar si una instancia de 2-CNF dada es satisfacible en un tiempo O( n ³ ) . Dado que encontrar una asignación satisfactoria utilizando el método de Krom implica una secuencia de comprobaciones de consistencia O( n ) , llevaría tiempo O( n ⁴ ) . Incluso, Itai y Shamir (1976) citan un límite de tiempo más rápido de O( n ² ) 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 gráfico de implicación de la instancia de 2-satisfacibilidad, la regla de inferencia de Krom puede interpretarse como la construcción del cierre transitivo del gráfico. Como observa Cook (1971), también puede verse como una instancia del algoritmo de Davis-Putnam para resolver problemas de satisfacibilidad utilizando el principio de resolución . Su corrección se desprende de la corrección más general del algoritmo de Davis-Putnam. Su límite temporal polinomial se desprende del hecho de que cada paso de resolución aumenta el número de cláusulas en la instancia, que está acotado superiormente por una función cuadrática del número de variables. ^[6]

Incluso, Itai y Shamir (1976) describen una técnica que implica un retroceso limitado para resolver problemas de satisfacción de restricciones con variables binarias y restricciones por pares. Aplican esta técnica a un problema de programación de clases, pero también observan que se aplica a otros problemas, incluido el 2-SAT. ^[5]

La idea básica de su enfoque es construir una asignación de verdad parcial, una variable a la vez. Ciertos pasos de los algoritmos son "puntos de elección", puntos en los que a una variable se le puede dar cualquiera de dos valores de verdad diferentes, y pasos posteriores en el algoritmo pueden hacer que retroceda a uno de estos puntos de elección. Sin embargo, solo se puede retroceder a la elección más reciente. Todas las elecciones realizadas antes de la más reciente son permanentes. ^[5]

Inicialmente, no hay un punto de elección y todas las variables están sin asignar. En cada paso, el algoritmo elige la variable cuyo valor se va a establecer, de la siguiente manera:

• Si hay una cláusula cuyas variables ya están establecidas, de manera que se falsifica la cláusula, entonces el algoritmo retrocede hasta su punto de elección más reciente, deshaciendo las asignaciones que hizo desde esa elección y revierte la decisión tomada en esa elección. Si no hay punto de elección, o si el algoritmo ya ha retrocedido hasta el punto de elección más reciente, entonces aborta la búsqueda e informa que la fórmula 2-CNF de entrada no se puede satisfacer.
• Si hay una cláusula en la que una de las dos variables de la cláusula ya se ha establecido, y la cláusula aún podría volverse verdadera o falsa, entonces la otra variable se establece de una manera que fuerza a la cláusula a volverse verdadera.
• En el caso restante, se garantiza que cada cláusula será verdadera sin importar cómo se asignen las variables restantes, o bien ninguna de sus dos variables ha sido asignada aún. En este caso, el algoritmo crea un nuevo punto de elección y establece cualquiera de las variables no asignadas en un valor elegido arbitrariamente.

Intuitivamente, el algoritmo sigue todas las cadenas de inferencia después de hacer cada una de sus elecciones. Esto lleva a una contradicción y a un paso de retroceso o, si no se deriva ninguna contradicción, se deduce que la elección fue correcta y conduce a una asignación satisfactoria. Por lo tanto, el algoritmo encuentra correctamente una asignación satisfactoria o determina correctamente que la entrada es insatisfactoria. ^[5]

Even et al. no describieron en detalle cómo implementar este algoritmo de manera eficiente. Solamente afirman que al "utilizar estructuras de datos apropiadas para encontrar las implicaciones de cualquier decisión", cada paso del algoritmo (excepto el retroceso) puede realizarse rápidamente. Sin embargo, algunas entradas pueden hacer que el algoritmo retroceda muchas veces, y que cada vez realice muchos pasos antes de retroceder, por lo que su complejidad general puede ser no lineal. Para evitar este problema, modifican el algoritmo de manera que, después de alcanzar cada punto de elección, comience a probar simultáneamente ambas asignaciones para el conjunto de variables en el punto de elección, dedicando la misma cantidad de pasos a cada una de las dos asignaciones. Tan pronto como la prueba para una de estas dos asignaciones cree otro punto de elección, se detiene la otra prueba, de modo que en cualquier etapa del algoritmo solo hay dos ramas del árbol de retroceso que aún se están probando. De esta manera, el tiempo total dedicado a realizar las dos pruebas para cualquier variable es proporcional al número de variables y cláusulas de la fórmula de entrada cuyos valores están asignados de manera permanente. Como resultado, el algoritmo toma un tiempo lineal en total. ^[5]

Aspvall, Plass y Tarjan (1979) encontraron un procedimiento de tiempo lineal más simple para resolver instancias de 2-satisfacibilidad, basado en la noción de componentes fuertemente conectados de la teoría de grafos . ^[4]

Se dice que dos vértices en un grafo dirigido están fuertemente conectados entre sí si hay un camino dirigido de uno al otro y viceversa. Esta es una relación de equivalencia , y los vértices del grafo pueden dividirse en componentes fuertemente conectados, subconjuntos dentro de los cuales cada dos vértices están fuertemente conectados. Existen varios algoritmos de tiempo lineal eficientes para encontrar los componentes fuertemente conectados de un grafo, basados ​​en la búsqueda en profundidad : el algoritmo de componentes fuertemente conectados de Tarjan ^[7] y el algoritmo de componentes fuertes basado en caminos ^[8] realizan cada uno una única búsqueda en profundidad. El algoritmo de Kosaraju realiza dos búsquedas en profundidad, pero es muy simple.

En términos del gráfico de implicaciones, dos literales pertenecen al mismo componente fuertemente conectado siempre que existan cadenas de implicaciones de un literal al otro y viceversa. Por lo tanto, los dos literales deben tener el mismo valor en cualquier asignación satisfactoria a la instancia de 2-satisfacibilidad dada. En particular, si una variable y su negación pertenecen ambas al mismo componente fuertemente conectado, la instancia no puede satisfacerse, porque es imposible asignar a ambos literales el mismo valor. Como mostraron Aspvall et al., esta es una condición necesaria y suficiente : una fórmula 2-CNF es satisfacible si y solo si no hay una variable que pertenezca al mismo componente fuertemente conectado que su negación. ^[4]

Esto conduce inmediatamente a un algoritmo de tiempo lineal para probar la satisfacibilidad de las fórmulas 2-CNF: simplemente realice un análisis de conectividad fuerte en el gráfico de implicación y verifique que cada variable y su negación pertenecen a diferentes componentes. Sin embargo, como también demostraron Aspvall et al., también conduce a un algoritmo de tiempo lineal para encontrar una asignación satisfactoria, cuando existe una. Su algoritmo realiza los siguientes pasos:

• Construya el gráfico de implicación de la instancia y encuentre sus componentes fuertemente conectados utilizando cualquiera de los algoritmos de tiempo lineal conocidos para el análisis de conectividad fuerte.
• Comprueba si algún componente fuertemente conectado contiene tanto una variable como su negación. Si es así, informa que la instancia no es satisfacible y detén la ejecución.
• Construya la condensación del grafo de implicación, un grafo más pequeño que tiene un vértice para cada componente fuertemente conectado y una arista desde el componente i hasta el componente j siempre que el grafo de implicación contenga una arista uv tal que u pertenece al componente i y v pertenece al componente j . La condensación es automáticamente un grafo acíclico dirigido y, al igual que el grafo de implicación a partir del cual se formó, es antisimétrico .
• Ordenar topológicamente los vértices de la condensación. En la práctica, esto se puede lograr de manera eficiente como un efecto secundario del paso anterior, ya que los componentes se generan mediante el algoritmo de Kosaraju en orden topológico y mediante el algoritmo de Tarjan en orden topológico inverso. ^[9]
• Para cada componente en el orden topológico inverso, si sus variables aún no tienen asignaciones de verdad, establezca todos los literales en el componente como verdaderos. Esto también hace que todos los literales en el componente complementario se establezcan como falsos.

Debido al ordenamiento topológico inverso y a la simetría oblicua, cuando un literal se establece como verdadero, todos los literales a los que se puede llegar desde él a través de una cadena de implicaciones ya se habrán establecido como verdaderos. Simétricamente, cuando un literal x se establece como falso, todos los literales que conducen a él a través de una cadena de implicaciones ya se habrán establecido como falsos. Por lo tanto, la asignación de verdad construida por este procedimiento satisface la fórmula dada, lo que también completa la prueba de corrección de la condición necesaria y suficiente identificada por Aspvall et al. ^[4].

Como muestran Aspvall et al., un procedimiento similar que implica ordenar topológicamente los componentes fuertemente conectados del gráfico de implicación también se puede utilizar para evaluar fórmulas booleanas completamente cuantificadas en las que la fórmula que se cuantifica es una fórmula 2-CNF. ^[4]

Varios algoritmos exactos y aproximados para el problema de colocación automática de etiquetas se basan en la 2-satisfacibilidad. Este problema se refiere a la colocación de etiquetas textuales en las características de un diagrama o mapa. Normalmente, el conjunto de posibles ubicaciones para cada etiqueta está muy restringido, no solo por el mapa en sí (cada etiqueta debe estar cerca de la característica que etiqueta y no debe ocultar otras características), sino por cada una de las demás: cada dos etiquetas deben evitar superponerse entre sí, ya que de lo contrario se volverían ilegibles. En general, encontrar una ubicación de etiqueta que obedezca estas restricciones es un problema NP-hard . Sin embargo, si cada característica tiene solo dos ubicaciones posibles para su etiqueta (por ejemplo, extendiéndose hacia la izquierda y hacia la derecha de la característica), entonces la ubicación de la etiqueta se puede resolver en tiempo polinomial. Porque, en este caso, se puede crear una instancia de 2-satisfacibilidad que tenga una variable para cada etiqueta y que tenga una cláusula para cada par de etiquetas que podrían superponerse, evitando que se les asignen posiciones superpuestas. Si las etiquetas son todas rectángulos congruentes, se puede demostrar que la instancia de 2-satisfacibilidad correspondiente tiene solo una cantidad lineal de restricciones, lo que conduce a algoritmos de tiempo casi lineal para encontrar un etiquetado. ^[10] Poon, Zhu y Chin (1998) describen un problema de etiquetado de mapas en el que cada etiqueta es un rectángulo que puede colocarse en una de tres posiciones con respecto a un segmento de línea que etiqueta: puede tener el segmento como uno de sus lados o puede estar centrado en el segmento. Representan estas tres posiciones utilizando dos variables binarias de tal manera que, nuevamente, probar la existencia de un etiquetado válido se convierte en un problema de 2-satisfacibilidad. ^[11]

Formann y Wagner (1991) utilizan la 2-satisfacibilidad como parte de un algoritmo de aproximación para el problema de encontrar etiquetas cuadradas del mayor tamaño posible para un conjunto dado de puntos, con la restricción de que cada etiqueta tenga una de sus esquinas en el punto que etiqueta. Para encontrar una etiqueta con un tamaño dado, eliminan los cuadrados que, si se duplicaran, se superpondrían a otro punto, y eliminan los puntos que se pueden etiquetar de una manera que no es posible que se superpongan con la etiqueta de otro punto. Muestran que estas reglas de eliminación hacen que los puntos restantes tengan solo dos posibles ubicaciones de etiqueta por punto, lo que permite encontrar una ubicación de etiqueta válida (si existe una) como solución a una instancia de 2-satisfacibilidad. Al buscar el tamaño de etiqueta más grande que conduzca a una instancia de 2-satisfacibilidad solucionable, encuentran una ubicación de etiqueta válida cuyas etiquetas son al menos la mitad de grandes que la solución óptima. Es decir, la razón de aproximación de su algoritmo es como máximo dos. ^{[10] [12]} De manera similar, si cada etiqueta es rectangular y debe colocarse de tal manera que el punto que etiqueta esté en algún lugar a lo largo de su borde inferior, entonces usar la 2-satisfacibilidad para encontrar el tamaño de etiqueta más grande para el cual hay una solución en la que cada etiqueta tiene el punto en una esquina inferior conduce a una relación de aproximación de como máximo dos. ^[13]

Se han realizado aplicaciones similares de 2-satisfacibilidad para otros problemas de ubicación geométrica. En el dibujo de grafos , si las ubicaciones de los vértices son fijas y cada arista debe dibujarse como un arco circular con una de dos ubicaciones posibles (por ejemplo, como un diagrama de arcos ), entonces el problema de elegir qué arco usar para cada arista para evitar cruces es un problema de 2-satisfacibilidad con una variable para cada arista y una restricción para cada par de ubicaciones que llevarían a un cruce. Sin embargo, en este caso es posible acelerar la solución, en comparación con un algoritmo que construye y luego busca una representación explícita del grafo de implicación, buscando el grafo implícitamente . ^[14] En el diseño de circuitos integrados VLSI , si una colección de módulos debe estar conectada por cables que pueden doblarse cada uno como máximo una vez, entonces nuevamente hay dos rutas posibles para los cables, y el problema de elegir cuál de estas dos rutas usar, de tal manera que todos los cables puedan enrutarse en una sola capa del circuito, puede resolverse como una instancia de 2-satisfacibilidad. ^[15]

Boros et al. (1999) consideran otro problema de diseño VLSI: la cuestión de si se debe o no invertir en espejo cada módulo en un diseño de circuito. Esta inversión en espejo deja sin cambios las operaciones del módulo, pero cambia el orden de los puntos en los que las señales de entrada y salida del módulo se conectan a él, posiblemente cambiando lo bien que el módulo encaja en el resto del diseño. Boros et al. consideran una versión simplificada del problema en la que los módulos ya se han colocado a lo largo de un único canal lineal, en el que los cables entre los módulos deben enrutarse y hay un límite fijo en la densidad del canal (el número máximo de señales que deben pasar a través de cualquier sección transversal del canal). Observan que esta versión del problema puede resolverse como una instancia de 2-satisfacibilidad, en la que las restricciones relacionan las orientaciones de pares de módulos que están directamente uno frente al otro en el canal. Como consecuencia, la densidad óptima también puede calcularse de manera eficiente, realizando una búsqueda binaria en la que cada paso implica la solución de una instancia de 2-satisfacibilidad. ^[16]

Una forma de agrupar un conjunto de puntos de datos en un espacio métrico en dos grupos es elegir los grupos de tal manera que se minimice la suma de los diámetros de los grupos, donde el diámetro de cualquier grupo individual es la distancia más grande entre dos de sus puntos. Esto es preferible a minimizar el tamaño máximo del grupo, lo que puede llevar a que puntos muy similares se asignen a diferentes grupos. Si se conocen los diámetros objetivo de los dos grupos, se puede encontrar un agrupamiento que logre esos objetivos resolviendo una instancia de 2-satisfacibilidad. La instancia tiene una variable por punto, que indica si ese punto pertenece al primer grupo o al segundo grupo. Siempre que dos puntos estén demasiado separados entre sí para que ambos pertenezcan al mismo grupo, se agrega una cláusula a la instancia que impide esta asignación.

El mismo método también se puede utilizar como una subrutina cuando se desconocen los diámetros de los grupos individuales. Para probar si se puede lograr una suma dada de diámetros sin conocer los diámetros de los grupos individuales, se pueden probar todos los pares máximos de diámetros objetivo que sumen como máximo la suma dada, representando cada par de diámetros como una instancia de 2-satisfacibilidad y utilizando un algoritmo de 2-satisfacibilidad para determinar si ese par se puede realizar mediante un agrupamiento. Para encontrar la suma óptima de diámetros, se puede realizar una búsqueda binaria en la que cada paso es una prueba de viabilidad de este tipo. El mismo enfoque también funciona para encontrar agrupamientos que optimicen otras combinaciones que no sean las sumas de los diámetros de los grupos, y que utilicen números de disimilitud arbitrarios (en lugar de distancias en un espacio métrico) para medir el tamaño de un grupo. ^[17] El límite de tiempo para este algoritmo está dominado por el tiempo para resolver una secuencia de instancias de 2-satisfacibilidad que están estrechamente relacionadas entre sí, y Ramnath (2004) muestra cómo resolver estas instancias relacionadas más rápidamente que si se resolvieran independientemente una de otra, lo que conduce a un límite de tiempo total de O ( n ³ ) para el problema de agrupamiento de suma de diámetros. ^[18]

Incluso, Itai y Shamir (1976) consideran un modelo de programación de aulas en el que un conjunto de n profesores debe programarse para enseñar a cada una de las m cohortes de estudiantes. El número de horas por semana que el profesor pasa con la cohorte se describe mediante la entrada de una matriz dada como entrada al problema, y ​​cada profesor también tiene un conjunto de horas durante las cuales él o ella está disponible para ser programado. Como muestran, el problema es NP-completo , incluso cuando cada profesor tiene como máximo tres horas disponibles, pero se puede resolver como un caso de 2-satisfacibilidad cuando cada profesor solo tiene dos horas disponibles. (Los profesores con sólo una hora disponible pueden ser fácilmente eliminados del problema.) En este problema, cada variable corresponde a una hora que el profesor debe pasar con la cohorte , la asignación a la variable especifica si esa hora es la primera o la segunda de las horas disponibles del profesor, y hay una cláusula de 2-satisfacibilidad que evita cualquier conflicto de cualquiera de los dos tipos: dos cohortes asignadas a un profesor al mismo tiempo entre sí, o una cohorte asignada a dos profesores al mismo tiempo. ^[5]${\estilo de visualización i}$${\estilo de visualización j}$$Estilo de visualización R_{ij}}$${\estilo de visualización R}$$estilo de visualización v_ {ij}}$${\estilo de visualización i}$${\estilo de visualización j}$

Miyashiro y Matsui (2005) aplican la 2-satisfactibilidad a un problema de programación deportiva, en el que ya se han elegido los emparejamientos de un torneo de todos contra todos y los partidos deben asignarse a los estadios de los equipos. En este problema, es deseable alternar partidos de local y de visitante en la medida de lo posible, evitando "descansos" en los que un equipo juega dos partidos de local seguidos o dos partidos de visitante seguidos. Como máximo, dos equipos pueden evitar los descansos por completo, alternando entre partidos de local y de visitante; ningún otro equipo puede tener el mismo calendario de local-de visitante que estos dos, porque entonces no podría jugar con el equipo con el que tenía el mismo calendario. Por lo tanto, un calendario óptimo tiene dos equipos sin descansos y un solo descanso para cada uno de los demás equipos. Una vez que se elige uno de los equipos sin descanso, se puede plantear un problema de 2-satisfacibilidad en el que cada variable representa la asignación de local-visitante para un solo equipo en un solo partido, y las restricciones imponen las propiedades de que dos equipos cualesquiera tienen una asignación consistente para sus partidos, que cada equipo tiene como máximo un descanso antes y como máximo un descanso después del partido con el equipo sin descanso, y que ningún equipo tiene dos descansos. Por lo tanto, comprobar si un calendario admite una solución con el número óptimo de descansos se puede hacer resolviendo un número lineal de problemas de 2-satisfacibilidad, uno para cada elección del equipo sin descanso. Una técnica similar también permite encontrar calendarios en los que cada equipo tiene un solo descanso, y maximizar en lugar de minimizar el número de descansos (para reducir el kilometraje total recorrido por los equipos). ^[19]

La tomografía es el proceso de recuperar formas a partir de sus secciones transversales. En la tomografía discreta , una versión simplificada del problema que se ha estudiado con frecuencia, la forma que se va a recuperar es un poliominó (un subconjunto de los cuadrados en la red cuadrada bidimensional ), y las secciones transversales proporcionan información agregada sobre los conjuntos de cuadrados en filas y columnas individuales de la red. Por ejemplo, en los populares rompecabezas de nonogramas , también conocidos como pintar por números o cuadrículas, el conjunto de cuadrados que se va a determinar representa los píxeles oscuros en una imagen binaria , y la entrada proporcionada al solucionador del rompecabezas le dice cuántos bloques consecutivos de píxeles oscuros incluir en cada fila o columna de la imagen, y qué longitud debe tener cada uno de esos bloques. En otras formas de tomografía digital, se proporciona incluso menos información sobre cada fila o columna: solo el número total de cuadrados, en lugar del número y la longitud de los bloques de cuadrados. Una versión equivalente del problema es que debemos recuperar una matriz 0-1 dada dadas sólo las sumas de los valores en cada fila y en cada columna de la matriz.

Aunque existen algoritmos de tiempo polinomial para encontrar una matriz que tiene sumas dadas de filas y columnas, ^[20] la solución puede estar lejos de ser única: cualquier submatriz en forma de una matriz identidad 2 × 2 puede complementarse sin afectar la corrección de la solución. Por lo tanto, los investigadores han buscado restricciones en la forma a reconstruir que puedan usarse para restringir el espacio de soluciones. Por ejemplo, uno podría asumir que la forma es conexa; sin embargo, probar si existe una solución conexa es NP-completo. ^[21] Una versión aún más restringida que es más fácil de resolver es que la forma es ortogonalmente convexa : tiene un solo bloque contiguo de cuadrados en cada fila y columna. Mejorando varias soluciones anteriores, Chrobak y Dürr (1999) mostraron cómo reconstruir formas convexas ortogonalmente conectadas de manera eficiente, utilizando 2-SAT. ^[22] La idea de su solución es adivinar los índices de las filas que contienen las celdas más a la izquierda y más a la derecha de la forma que se va a reconstruir, y luego plantear un problema de 2-satisfacibilidad que prueba si existe una forma consistente con estas suposiciones y con las sumas de filas y columnas dadas. Utilizan cuatro variables de 2-satisfacibilidad para cada cuadrado que podría ser parte de la forma dada, una para indicar si pertenece a cada una de las cuatro posibles "regiones de esquina" de la forma, y ​​utilizan restricciones que obligan a estas regiones a ser disjuntas, a tener las formas deseadas, a formar una forma general con filas y columnas contiguas, y a tener las sumas de filas y columnas deseadas. Su algoritmo lleva tiempo O( m ³ n ) donde m es la menor de las dos dimensiones de la forma de entrada y n es la mayor de las dos dimensiones. El mismo método se extendió más tarde a formas ortogonalmente convexas que podrían estar conectadas solo en diagonal en lugar de requerir conectividad ortogonal. ^[23]

Como parte de un solucionador de acertijos de nonogramas completos, Batenburg y Kosters (2008, 2009) utilizaron la 2-satisfacibilidad para combinar la información obtenida de varias otras heurísticas . Dada una solución parcial al acertijo, utilizan programación dinámica dentro de cada fila o columna para determinar si las restricciones de esa fila o columna fuerzan a que alguno de sus cuadrados sea blanco o negro, y si dos cuadrados cualesquiera en la misma fila o columna pueden conectarse mediante una relación de implicación. También transforman el nonograma en un problema de tomografía digital reemplazando la secuencia de longitudes de bloque en cada fila y columna por su suma, y ​​utilizan una formulación de flujo máximo para determinar si este problema de tomografía digital que combina todas las filas y columnas tiene cuadrados cuyo estado puede determinarse o pares de cuadrados que pueden conectarse mediante una relación de implicación. Si cualquiera de estas dos heurísticas determina el valor de uno de los cuadrados, se incluye en la solución parcial y se repiten los mismos cálculos. Sin embargo, si ambas heurísticas no logran establecer ningún cuadrado, las implicaciones encontradas por ambas se combinan en un problema de 2-satisfacibilidad y se utiliza un solucionador de 2-satisfacibilidad para encontrar cuadrados cuyo valor esté fijado por el problema, después de lo cual se repite nuevamente el procedimiento. Este procedimiento puede o no lograr encontrar una solución, pero se garantiza que se ejecutará en tiempo polinomial. Batenburg y Kosters informan que, aunque la mayoría de los acertijos de periódicos no necesitan toda su potencia, tanto este procedimiento como un procedimiento más poderoso pero más lento que combina este enfoque de 2-satisfacibilidad con el retroceso limitado de Even, Itai y Shamir (1976) ^[5] son ​​significativamente más efectivos que la programación dinámica y las heurísticas de flujo sin 2-satisfacibilidad cuando se aplican a nonogramas generados aleatoriamente más difíciles. ^[24]

Junto a la 2-satisfacibilidad, la otra subclase principal de problemas de satisfacibilidad que se pueden resolver en tiempo polinomial es la satisfacibilidad de Horn . En esta clase de problemas de satisfacibilidad, la entrada es nuevamente una fórmula en forma normal conjuntiva. Puede tener arbitrariamente muchos literales por cláusula, pero como máximo un literal positivo. Lewis (1978) encontró una generalización de esta clase, la satisfacibilidad de Horn renombrable , que aún se puede resolver en tiempo polinomial por medio de una instancia auxiliar de 2-satisfacibilidad. Una fórmula es Horn renombrable cuando es posible ponerla en forma de Horn reemplazando algunas variables por sus negaciones. Para hacer esto, Lewis establece una instancia de 2-satisfacibilidad con una variable para cada variable de la instancia de Horn renombrable, donde las variables de 2-satisfacibilidad indican si se deben negar o no las variables de Horn renombrables correspondientes. Para producir una instancia de Horn, no deben aparecer dos variables que aparezcan en la misma cláusula de la instancia de Horn renombrable de manera positiva en esa cláusula; Esta restricción sobre un par de variables es una restricción de 2-satisfacibilidad. Al encontrar una asignación satisfactoria a la instancia de 2-satisfacibilidad resultante, Lewis muestra cómo convertir cualquier instancia de Horn renombrable en una instancia de Horn en tiempo polinomial. ^[25] Al dividir cláusulas largas en múltiples cláusulas más pequeñas y aplicar un algoritmo de 2-satisfacibilidad en tiempo lineal, es posible reducir esto a tiempo lineal. ^[26]

La 2-satisfacibilidad también se ha aplicado a problemas de reconocimiento de gráficos no dirigidos que se pueden dividir en un conjunto independiente y un pequeño número de subgráficos bipartitos completos , ^[27] infiriendo relaciones comerciales entre subsistemas autónomos de Internet, ^[28] y reconstrucción de árboles evolutivos . ^[29]

Un algoritmo no determinista para determinar si una instancia de 2-satisfacibilidad no es satisfacible, utilizando solo una cantidad logarítmica de memoria escribible, es fácil de describir: simplemente elija (de manera no determinista) una variable v y busque (de manera no determinista) una cadena de implicaciones que conduzca de v a su negación y luego regrese a v . Si se encuentra dicha cadena, la instancia no puede ser satisfacible. Por el teorema de Immerman–Szelepcsényi , también es posible en el espacio logarítmico no determinista verificar que una instancia de 2-satisfacibilidad satisfacible es satisfacible.

La 2-satisfacibilidad es NL-completa , ^[30] lo que significa que es uno de los problemas "más difíciles" o "más expresivos" en la clase de complejidad NL de problemas resolubles de forma no determinista en el espacio logarítmico. Completitud aquí significa que una máquina de Turing determinista que use solo el espacio logarítmico puede transformar cualquier otro problema en NL en un problema de 2-satisfacibilidad equivalente. De manera análoga a resultados similares para la clase de complejidad más conocida NP , esta transformación junto con el teorema de Immerman–Szelepcsényi permiten que cualquier problema en NL se represente como una fórmula lógica de segundo orden con un solo predicado cuantificado existencialmente con cláusulas limitadas a una longitud de 2. Dichas fórmulas se conocen como SO-Krom. ^[31] De manera similar, la forma normal implicativa se puede expresar en lógica de primer orden con la adición de un operador para el cierre transitivo . ^[31]

El conjunto de todas las soluciones de una instancia de 2-satisfacibilidad tiene la estructura de un grafo de medianas , en el que una arista corresponde a la operación de invertir los valores de un conjunto de variables que están todas restringidas a ser iguales o desiguales entre sí. En particular, al seguir las aristas de esta manera se puede llegar de cualquier solución a cualquier otra solución. A la inversa, cualquier grafo de medianas se puede representar como el conjunto de soluciones de una instancia de 2-satisfacibilidad de esta manera. La mediana de tres soluciones cualesquiera se forma fijando cada variable en el valor que tiene en la mayoría de las tres soluciones. Esta mediana siempre forma otra solución para la instancia. ^[32]

Feder (1994) describe un algoritmo para enumerar eficientemente todas las soluciones a una instancia dada de 2-satisfacibilidad, y para resolver varios problemas relacionados. ^[33] También existen algoritmos para encontrar dos asignaciones satisfactorias que tengan la distancia de Hamming máxima entre sí. ^[34]

#2SAT es el problema de contar la cantidad de asignaciones satisfactorias a una fórmula 2-CNF dada. Este problema de conteo es #P-completo , ^[35] lo que implica que no es solucionable en tiempo polinomial a menos que P = NP . Además, no existe un esquema de aproximación aleatoria completamente polinomial para #2SAT a menos que NP = RP y esto se cumple incluso cuando la entrada está restringida a fórmulas 2-CNF monótonas, es decir, fórmulas 2-CNF en las que cada literal es una ocurrencia positiva de una variable. ^[36]

El algoritmo más rápido conocido para calcular el número exacto de asignaciones satisfactorias a una fórmula 2SAT se ejecuta en el tiempo . ^{[37] [38] [39]}$Estilo de visualización O(1,2377^{n})}$

Se puede formar una instancia de 2-satisfacibilidad al azar, para un número dado n de variables y m de cláusulas, eligiendo cada cláusula de manera uniforme al azar del conjunto de todas las cláusulas de dos variables posibles. Cuando m es pequeño en relación con n , tal instancia probablemente será satisfacible, pero valores mayores de m tienen probabilidades menores de ser satisfacibles. Más precisamente, si m / n se fija como una constante α ≠ 1, la probabilidad de satisfacibilidad tiende a un límite cuando n tiende a infinito: si α < 1, el límite es uno, mientras que si α > 1, el límite es cero. Por lo tanto, el problema exhibe una transición de fase en α = 1. ^[40]

En el problema de máxima satisfacibilidad 2 ( MAX-2-SAT ), la entrada es una fórmula en forma normal conjuntiva con dos literales por cláusula, y la tarea es determinar el número máximo de cláusulas que pueden satisfacerse simultáneamente mediante una asignación. Al igual que el problema de máxima satisfacibilidad más general , MAX-2-SAT es NP-hard . La prueba es por reducción a partir de 3SAT . ^[41]

Al formular MAX-2-SAT como un problema de búsqueda de un corte (es decir, una partición de los vértices en dos subconjuntos) que maximice el número de aristas que tienen un punto final en el primer subconjunto y un punto final en el segundo, en un grafo relacionado con el grafo de implicación, y aplicar métodos de programación semidefinida a este problema de corte, es posible encontrar en tiempo polinomial una solución aproximada que satisface al menos 0,940... veces el número óptimo de cláusulas. ^[42] Una instancia de MAX 2-SAT balanceada es una instancia de MAX 2-SAT donde cada variable aparece positiva y negativamente con igual peso. Para este problema, Austrin ha mejorado la relación de aproximación a . ^[43]${\displaystyle \min \left\{(3-\cos \theta )^{-1}(2+(2/\pi )\theta )\,:\,\pi /2\leq \theta \leq \pi \right\}=0,943...}$

Si la conjetura de los juegos únicos es verdadera, entonces es imposible aproximar MAX 2-SAT, balanceado o no, con una constante de aproximación mejor que 0,943... en tiempo polinomial. ^[44] Bajo el supuesto más débil de que P ≠ NP , solo se sabe que el problema es inaproximable dentro de una constante mejor que 21/22 = 0,95454... ^[45]

Varios autores también han explorado los límites de tiempo exponenciales del peor caso para la solución exacta de instancias MAX-2-SAT. ^[46]

En el problema de 2-satisfacibilidad ponderada ( W2SAT ), la entrada es una instancia 2SAT de una variable y un entero k , y el problema es decidir si existe una asignación satisfactoria en la que exactamente k de las variables sean verdaderas. ^[47]${\estilo de visualización n}$

El problema W2SAT incluye como caso especial el problema de cobertura de vértices , de encontrar un conjunto de k vértices que juntos toquen todas las aristas de un grafo no dirigido dado. Para cualquier instancia dada del problema de cobertura de vértices, se puede construir un problema W2SAT equivalente con una variable para cada vértice de un grafo. Cada arista uv del grafo puede representarse mediante una cláusula 2SAT u ∨ v que puede satisfacerse solo incluyendo u o v entre las variables verdaderas de la solución. Entonces, las instancias satisfactorias de la fórmula 2SAT resultante codifican soluciones al problema de cobertura de vértices, y hay una asignación satisfactoria con k variables verdaderas si y solo si hay una cobertura de vértices con k vértices. Por lo tanto, al igual que la cobertura de vértices, W2SAT es NP-completo .

Además, en la complejidad parametrizada, W2SAT proporciona un problema W[1]-completo natural, ^[47] lo que implica que W2SAT no es manejable con parámetros fijos a menos que esto se cumpla para todos los problemas en W[1] . Es decir, es poco probable que exista un algoritmo para W2SAT cuyo tiempo de ejecución tome la forma f ( k )· n ^{O (1)} . Aún más fuertemente, W2SAT no puede resolverse en el tiempo n ^{o ( k )} a menos que la hipótesis del tiempo exponencial falle. ^[48]

Además de encontrar el primer algoritmo de tiempo polinómico para la 2-satisfacibilidad, Krom (1967) también formuló el problema de evaluar fórmulas booleanas completamente cuantificadas en las que la fórmula que se cuantifica es una fórmula 2-CNF. El problema de la 2-satisfacibilidad es el caso especial de este problema 2-CNF cuantificado, en el que todos los cuantificadores son existenciales . Krom también desarrolló un procedimiento de decisión eficaz para estas fórmulas. Aspvall, Plass y Tarjan (1979) demostraron que se puede resolver en tiempo lineal, mediante una extensión de su técnica de componentes fuertemente conectados y ordenamiento topológico. ^{[2] [4]}

El problema de 2-satisfacibilidad también puede plantearse en el caso de lógicas proposicionales polivalentes . Los algoritmos no suelen ser lineales y, en el caso de algunas lógicas, el problema es incluso NP-completo. Véase Hähnle (2001, 2003) para consultar los estudios al respecto. ^[49]