2-satisfacibilidad

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

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 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 satisfacerse siempre que las dos primeras cláusulas se satisfagan. Esto se llama resolución . Por ejemplo, podemos combinar las cláusulas${\displaystyle (a\lor b)}$y${\displaystyle (\lnot b\lor \lnot c)}$de esta manera producir la cláusula${\displaystyle (a\lor \lno c)}$En términos de la forma implicativa de una fórmula 2-CNF, esta regla equivale a encontrar dos implicaciones.${\displaystyle \lnot a\Rightarrow b}$y${\displaystyle b\Rightarrow \lnot c}$y deduciendo por transitividad una tercera implicación${\displaystyle \lnot a\Rightarrow \lnot c}$. ^{[ 3 ]}

Krom escribe que una fórmula es consistente si la aplicación repetida de esta regla de inferencia no puede generar ambas cláusulas.${\displaystyle (x\lor x)}$y${\displaystyle (\lnot x\lor \lnot x)}$, para cualquier variable${\displaystyle x}$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.${\displaystyle (x\lor x)}$y${\displaystyle (\lnot x\lor \lnot x)}$simultáneamente. Y, si es consistente, entonces la fórmula puede extenderse agregando repetidamente una cláusula de la forma${\displaystyle (x\lor x)}$o${\displaystyle (\lnot x\lor \lnot x)}$de una en una, 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 preservando la consistencia, ya que de lo contrario la otra cláusula podría generarse 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.${\displaystyle x}$verdadero si la fórmula contiene la cláusula${\displaystyle (x\lor x)}$y estableciéndolo en falso si la fórmula contiene la cláusula${\displaystyle (\lnot x\lor \lnot x)}$. ^{[ 3 ]}

Krom se centró principalmente en la completitud de los sistemas de reglas de inferencia, más que en la eficiencia de los algoritmos. Sin embargo, su método conduce a una cota de tiempo polinomial para resolver problemas de 2-satisfacibilidad. Al agrupar todas las cláusulas que usan la misma variable y aplicar 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 ^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 las que se puede aplicar la regla de inferencia. Por lo tanto, es posible determinar si una instancia 2-CNF dada es satisfacible en un tiempo O ( ^n³ ) . Dado que encontrar una asignación satisfactoria usando ^el método de Krom implica una secuencia de O( n ) comprobaciones de consistencia, tomaría un tiempo O( n⁴ ⁾ . Even, 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. ^{[ 7 ]} Sin embargo, incluso este límite de tiempo menor fue mejorado notablemente por los algoritmos de tiempo lineal posteriores de Even, Itai y Shamir (1976) y Aspvall, Plass y Tarjan (1979) . ^{[ 8 ]}

En términos del grafo 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 grafo. 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 deriva de la corrección más general del algoritmo de Davis-Putnam. Su límite de tiempo polinomial se deriva 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. ^{[ 9 ]}

Even, Itai y Shamir (1976) describen una técnica que implica 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 aulas, pero también observan que se aplica a otros problemas, incluido el 2-SAT. ^{[ 6 ]}

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 decisión", puntos en los que a una variable se le puede asignar cualquiera de dos valores de verdad diferentes, y los pasos posteriores del algoritmo pueden hacer que retroceda a uno de estos puntos de decisión. Sin embargo, solo se puede retroceder a la decisión más reciente. Todas las decisiones tomadas antes de la más reciente son permanentes. ^{[ 6 ]}

Inicialmente, no hay ningún punto de decisión y todas las variables están sin asignar. En cada paso, el algoritmo elige la variable cuyo valor establecer, como sigue: ^{[ 6 ]}

• Si existe una cláusula cuyas variables ya están definidas de forma que la invalida, el algoritmo retrocede hasta su punto de elección más reciente, deshaciendo las asignaciones realizadas desde entonces, y revierte la decisión tomada en ese punto. Si no hay ningún punto de elección, o si el algoritmo ya ha retrocedido hasta el punto de elección más reciente, aborta la búsqueda e informa que la fórmula 2-CNF de entrada es insatisfacible. ^{[ 6 ]}
• Si existe una cláusula en la que una de las dos variables ya ha sido definida, y la cláusula aún podría ser verdadera o falsa, entonces la otra variable se define de manera que la cláusula se convierta en verdadera. ^{[ 6 ]}
• En el caso restante, se garantiza que cada cláusula se vuelva verdadera independientemente de cómo se asignen las variables restantes, o bien ninguna de sus dos variables ha sido asignada todavía. En este caso, el algoritmo crea un nuevo punto de decisión y asigna un valor arbitrario a cualquiera de las variables no asignadas. ^{[ 6 ]}

Intuitivamente, el algoritmo sigue todas las cadenas de inferencia después de cada una de sus elecciones. Esto conduce 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 que conduce a una asignación satisfactoria. Por lo tanto, el algoritmo encuentra correctamente una asignación satisfactoria o determina correctamente que la entrada es insatisfacible. ^{[ 6 ]}

Even et al. no describieron en detalle cómo implementar este algoritmo de manera eficiente. Solo afirman que, al "utilizar estructuras de datos apropiadas para encontrar las implicaciones de cada decisión", cada paso del algoritmo (excepto el retroceso) se puede realizar rápidamente. Sin embargo, algunas entradas pueden provocar que el algoritmo retroceda muchas veces, realizando cada vez 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 llegar a cada punto de decisión, comience a probar simultáneamente ambas asignaciones para el conjunto de variables en dicho punto, dedicando el mismo número de pasos a cada una. Tan pronto como la prueba para una de estas dos asignaciones crearía otro punto de decisión, la otra prueba se detiene, 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 empleado en 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 permanentemente. Como resultado, el algoritmo tiene un tiempo total lineal . ^{[ 6 ]} En comparaciones experimentales en instancias generadas aleatoriamente, una versión de este algoritmo de retroceso fue más rápida que otros algoritmos de tiempo lineal. ^{[ 2 ]}

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 conectadas de la teoría de grafos . ^{[ 5 ]}

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

En términos del grafo de implicación, dos literales pertenecen al mismo componente fuertemente conexo 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 que satisfaga la instancia de 2-satisfacibilidad dada. En particular, si una variable y su negación pertenecen al mismo componente fuertemente conexo, la instancia no puede ser satisfecha, porque es imposible asignar el mismo valor a ambos literales. Como demostraron Aspvall et al., esta es una condición necesaria y suficiente : una fórmula 2-CNF es satisfacible si y solo si no hay ninguna variable que pertenezca al mismo componente fuertemente conexo que su negación. ^{[ 5 ]}

Esto conduce inmediatamente a un algoritmo de tiempo lineal para probar la satisfacibilidad de fórmulas 2-CNF: simplemente se realiza un análisis de conectividad fuerte en el grafo de implicación y se comprueba que cada variable y su negación pertenecen a componentes diferentes. 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. Su algoritmo realiza los siguientes pasos: ^{[ 5 ]}

• Construya el grafo de implicación de la instancia y encuentre sus componentes fuertemente conexas utilizando cualquiera de los algoritmos conocidos de tiempo lineal para el análisis de conectividad fuerte. ^{[ 5 ]}
• 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 detente. ^{[ 5 ]}
• Construye la condensación del grafo de implicación, un grafo más pequeño que tiene un vértice por cada componente fuertemente conexa, y una arista del componente i al 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 dirigido acíclico y, al igual que el grafo de implicación del que se formó, es antisimétrico . ^{[ 5 ]}
• Ordenar topológicamente los vértices de la condensación. ^{[ 5 ]} En la práctica, esto puede lograrse eficientemente 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. ^{[ 12 ] [ 13 ]}
• Para cada componente en el orden topológico inverso, si sus variables no tienen ya asignaciones de verdad, establezca todos los literales del componente como verdaderos. Esto también hace que todos los literales del componente complementario se establezcan como falsos. ^{[ 5 ]}

Debido al orden topológico inverso y a la antisimetría, cuando un literal se establece como verdadero, todos los literales que se pueden alcanzar desde él a través de una cadena de implicaciones ya se habrán establecido como verdaderos. De forma simétrica, 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 mediante 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. ^{[ 5 ].}

Como muestran Aspvall et al., un procedimiento similar que implica el ordenamiento topológico de los componentes fuertemente conectados del grafo de implicación también puede utilizarse para evaluar fórmulas booleanas totalmente cuantificadas en las que la fórmula que se cuantifica es una fórmula 2-CNF. ^{[ 5 ]}

Varios algoritmos exactos y aproximados para el problema de la colocación automática de etiquetas se basan en la 2-satisfacibilidad. Este problema consiste en colocar etiquetas de texto en las características de un diagrama o mapa. Normalmente, el conjunto de ubicaciones posibles 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), sino también entre sí: cada par de etiquetas debe evitar superponerse, ya que de lo contrario se volverían ilegibles. En general, encontrar una ubicación de etiquetas que cumpla con estas restricciones es un problema NP-difícil . Sin embargo, si cada característica tiene solo dos ubicaciones posibles para su etiqueta (por ejemplo, extendiéndose a la izquierda y a la derecha de la característica), entonces la colocación de etiquetas puede resolverse en tiempo polinomial. En este caso, se puede crear una instancia de 2-satisfacibilidad que tenga una variable para cada etiqueta y una cláusula para cada par de etiquetas que podrían superponerse, impidiendo que se les asignen posiciones superpuestas. Si todas las etiquetas son rectángulos congruentes, se puede demostrar que la instancia de 2-satisfacibilidad correspondiente tiene solo una cantidad lineal de restricciones, lo que lleva a algoritmos de tiempo casi lineal para encontrar un etiquetado. ^{[ 14 ]} 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 usando dos variables binarias de tal manera que, nuevamente, probar la existencia de un etiquetado válido se convierte en un problema de 2-satisfacibilidad. ^{[ 15 ]}

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 sobre el punto que etiqueta. Para encontrar un etiquetado con un tamaño dado, eliminan los cuadrados que, si se duplicaran, se superpondrían con otro punto, y eliminan los puntos que pueden etiquetarse de forma que no puedan superponerse con la etiqueta de otro punto. Demuestran que estas reglas de eliminación hacen que los puntos restantes tengan solo dos posibles ubicaciones de etiquetas por punto, lo que permite encontrar una ubicación de etiqueta válida (si existe) como solución a una instancia de 2-satisfacibilidad. Al buscar el mayor tamaño de etiqueta que conduce a una instancia de 2-satisfacibilidad resoluble, 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. ^{[ 14 ] [ 16 ]} De manera similar, si cada etiqueta es rectangular y debe colocarse de tal forma que el punto que etiqueta esté en algún lugar de su borde inferior, entonces usar la 2-satisfacibilidad para encontrar el tamaño de etiqueta más grande para el cual existe una solución en la que cada etiqueta tiene el punto en una esquina inferior conduce a una razón de aproximación de como máximo dos. ^{[ 17 ]}

Se han realizado aplicaciones similares de la 2-satisfacibilidad para otros problemas de colocació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 colocaciones que conducirí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 en el grafo implícitamente . ^{[ 18 ]} En el diseño de circuitos integrados VLSI , si un conjunto de módulos debe conectarse mediante cables que pueden doblarse 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 manera que todos los cables puedan enrutarse en una sola capa del circuito, puede resolverse como una instancia de 2-satisfacibilidad. ^{[ 19 ]}

Boros et al. (1999) consideran otro problema de diseño VLSI: la cuestión de si invertir o no la simetría de cada módulo en un diseño de circuito. Esta inversión simétrica no altera 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, lo que podría modificar su integración 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 se deben enrutar los cables entre los módulos, y existe un límite fijo en la densidad del canal (el número máximo de señales que deben pasar por 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 se encuentran directamente uno frente al otro en el canal. En consecuencia, la densidad óptima también puede calcularse de forma eficiente, realizando una búsqueda binaria en la que cada paso implica la solución de una instancia de 2-satisfacibilidad. ^{[ 20 ]}

Una forma de agrupar un conjunto de puntos de datos en un espacio métrico en dos clústeres es elegirlos de manera que se minimice la suma de sus diámetros , donde el diámetro de cualquier clúster es la mayor distancia entre dos de sus puntos. Esto es preferible a minimizar el tamaño máximo del clúster, lo que podría resultar en la asignación de puntos muy similares a clústeres diferentes. Si se conocen los diámetros objetivo de los dos clústeres, se puede encontrar una agrupación que cumpla con dichos objetivos resolviendo una instancia de 2-satisfacibilidad. La instancia tiene una variable por punto, que indica si ese punto pertenece al primer o al segundo clúster. Si dos puntos están demasiado alejados entre sí como para pertenecer ambos al mismo clúster, se agrega una cláusula a la instancia que impide esta asignación. ^{[ 21 ]}

El mismo método también puede utilizarse como subrutina cuando se desconocen los diámetros de los clústeres individuales. Para comprobar si se puede alcanzar una suma de diámetros determinada sin conocer los diámetros de los clústeres 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 dicho par puede realizarse mediante una agrupación. Para hallar la suma óptima de diámetros, se puede realizar una búsqueda binaria en la que cada paso sea una prueba de viabilidad de este tipo. El mismo enfoque también funciona para encontrar agrupaciones que optimicen otras combinaciones distintas a las sumas de los diámetros de los clústeres, y que utilicen números de disimilitud arbitrarios (en lugar de distancias en un espacio métrico) para medir el tamaño de un clúster. ^{[ 21 ]} 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 unas de otras, lo que lleva a un límite de tiempo total de O ( n ³ ) para el problema de agrupamiento de suma de diámetros. ^{[ 22 ]}

Incluso, Itai y Shamir (1976) consideran un modelo de programación de aulas en el que un conjunto de n profesores deben ser programados para enseñar a cada uno de los m grupos de estudiantes. El número de horas por semana que el profesor${\displaystyle i}$gasta con el grupo${\displaystyle j}$se describe mediante entrada${\displaystyle R_{ij}}$de una matriz${\displaystyle R}$Se proporciona como entrada al problema, y ​​cada profesor también tiene un conjunto de horas durante las cuales 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 una instancia de 2-satisfacibilidad cuando cada profesor solo tiene dos horas disponibles. (Los profesores con solo una hora disponible pueden eliminarse fácilmente del problema). En este problema, cada variable${\displaystyle v_{ij}}$corresponde a una hora que el profesor${\displaystyle i}$debe pasar con el grupo${\displaystyle j}$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 satisfacibilidad 2 que impide cualquier conflicto de dos tipos: dos cohortes asignadas a un profesor al mismo tiempo, o una cohorte asignada a dos profesores al mismo tiempo. ^{[ 6 ]}

Miyashiro y Matsui (2005) aplican la 2-satisfacibilidad a un problema de programación deportiva, en el que los emparejamientos de un torneo de todos contra todos ya han sido elegidos y los partidos deben asignarse a los estadios de los equipos. En este problema, es deseable alternar partidos de local y visitante en la medida de lo posible, evitando "descansos" en los que un equipo juegue 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 visitante; ningún otro equipo puede tener el mismo calendario de local y visitante que estos dos, porque entonces no podría jugar contra el equipo con el que tuviera 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 elegido 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 cualesquiera dos equipos tengan una asignación consistente para sus partidos, que cada equipo tenga 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 tenga dos descansos. Por lo tanto, se puede comprobar si un calendario admite una solución con el número óptimo de descansos 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 tenga un solo descanso, y maximizar en lugar de minimizar el número de descansos (para reducir el kilometraje total recorrido por los equipos). ^{[ 23 ]}

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 a recuperar es un poliomino (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. ^{[ 24 ]} Por ejemplo, en los populares rompecabezas nonogramas , también conocidos como pintar por números o cuadrículas, el conjunto de cuadrados a determinar representa los píxeles oscuros en una imagen binaria , y la entrada que se le da al que resuelve el rompecabezas le dice cuántos bloques consecutivos de píxeles oscuros debe incluir en cada fila o columna de la imagen, y qué tan largo debe ser cada uno de esos bloques. ^{[ 25 ]} En otras formas de tomografía digital, se da 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 binaria dada a partir únicamente de las sumas de los valores en cada fila y en cada columna de la matriz. ^{[ 24 ]}

Aunque existen algoritmos de tiempo polinomial para encontrar una matriz con sumas de filas y columnas dadas, ^{[ 26 ]} la solución puede estar lejos de ser única: cualquier submatriz en forma de una matriz identidad de  2 ×  2 puede ser complementada 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, se podría suponer que la forma es conexa; sin embargo, probar si existe una solución conexa es NP-completo. ^{[ 27 ]} Una versión aún más restringida y más fácil de resolver es que la forma sea ortogonalmente convexa : tener un único bloque contiguo de cuadrados en cada fila y columna. Mejorando varias soluciones anteriores, Chrobak y Dürr (1999) mostraron cómo reconstruir formas conexas ortogonales conexas de manera eficiente, usando 2-SAT. ^{[ 24 ]} 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 a reconstruir, y luego establecer un problema de 2-satisfacibilidad que prueba si existe una forma consistente con estas adivinaciones 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 que estas regiones sean disjuntas, tengan las formas deseadas, formen una forma general con filas y columnas contiguas, y tengan las sumas de filas y columnas deseadas. Su algoritmo toma un 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ó posteriormente a formas ortogonalmente convexas que podrían estar conectadas solo diagonalmente en lugar de requerir conectividad ortogonal. ^{[ 28 ]}

Como parte de un solucionador de puzles de nonogramas completos, Batenburg y Kosters ( 2008 , 2009 ) utilizaron la 2-satisfacibilidad para combinar información obtenida de varias heurísticas . Dada una solución parcial del puzle, emplean programación dinámica dentro de cada fila o columna para determinar si las restricciones de dicha fila o columna obligan a que alguno de sus cuadrados sea blanco o negro, y si dos cuadrados cualesquiera de 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 bloques 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 alguna de estas dos heurísticas determina el valor de uno de los cuadrados, este 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 el procedimiento se repite. Este procedimiento puede o no tener éxito en encontrar una solución, pero se garantiza que se ejecutará en tiempo polinomial. Batenburg y Kosters informan que, aunque la mayoría de los rompecabezas de periódicos no necesitan toda su potencia, tanto este procedimiento como un procedimiento más potente pero más lento que combina este enfoque de 2-satisfacibilidad con el retroceso limitado de Even, Itai y Shamir (1976) ^{[ 6 ]} 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. ^{[ 25 ]} 

Además de 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 mediante una instancia auxiliar de 2-satisfacibilidad. Una fórmula es de Horn renombrable cuando es posible ponerla en forma de Horn reemplazando algunas variables por sus negaciones. Para ello, Lewis establece una instancia de 2-satisfacibilidad con una variable por 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 debe haber dos variables que aparezcan en la misma cláusula de la instancia de Horn renombrable que aparezcan positivamente 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 para la instancia de 2-satisfacibilidad resultante, Lewis muestra cómo convertir cualquier instancia de Horn renombrable en una instancia de Horn en tiempo polinomial. ^{[ 29 ]} Al dividir cláusulas largas en múltiples cláusulas más pequeñas y aplicar un algoritmo de 2-satisfacibilidad de tiempo lineal, es posible reducir esto a tiempo lineal. ^{[ 30 ]}

La 2-satisfacibilidad también se ha aplicado a problemas de reconocimiento de grafos no dirigidos que pueden particionarse en un conjunto independiente y un pequeño número de subgrafos bipartitos completos , ^{[ 31 ]} inferir relaciones comerciales entre subsistemas autónomos de Internet, ^{[ 32 ]} y reconstrucción de árboles evolutivos . ^{[ 33 ]}

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 se elige (de forma no determinista) una variable v y se busca (de forma no determinista) una cadena de implicaciones que conduzca de v a su negación y luego de vuelta a v . Si se encuentra dicha cadena, la instancia no puede ser satisfacible. ^{[ 34 ]} 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. ^{[ 35 ]}

La 2-satisfacibilidad es NL-completa , ^{[ 34 ]} 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 espacio logarítmico. La completitud aquí significa que una máquina de Turing determinista que utilice solo espacio logarítmico puede transformar cualquier otro problema en NL en un problema de 2-satisfacibilidad equivalente. De forma 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 permite que cualquier problema en NL se represente como una fórmula de lógica de segundo orden con un único predicado cuantificado existencialmente con cláusulas limitadas a longitud 2. Dichas fórmulas se conocen como SO-Krom. ^{[ 36 ]} 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 . ^{[ 36 ]}

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

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

#2SAT es el problema de contar el número de asignaciones satisfactorias a una fórmula 2-CNF dada. Este problema de conteo es #P-completo , ^{[ 40 ]} lo que implica que no es resoluble en tiempo polinomial a menos que P  =  NP . Además, no existe un esquema de aproximación aleatoria totalmente polinomial para #2SAT a menos que NP = RP , e incluso esto se cumple cuando la entrada se restringe 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. ^{[ 41 ]}

El algoritmo más rápido conocido para calcular el número exacto de asignaciones satisfactorias a una fórmula 2SAT se ejecuta en tiempo${\displaystyle O(1.2377^{n})}$. ^{[ 42 ] [ 43 ] [ 44 ]}

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 uniformemente al azar del conjunto de todas las posibles cláusulas de dos variables. Cuando m es pequeño en relación con n , es probable que dicha instancia sea satisfacible, pero valores mayores de m tienen menores probabilidades de serlo. 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 presenta una transición de fase en α  =  1. ^{[ 45 ]}

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 consiste en determinar el número máximo de cláusulas que pueden ser satisfechas simultáneamente por una asignación. Al igual que el problema de máxima satisfacibilidad más general , MAX-2-SAT es NP-difícil . La demostración se realiza mediante reducción a partir de 3SAT . ^{[ 46 ]}

Al formular MAX-2-SAT como un problema de encontrar un corte (es decir, una partición de los vértices en dos subconjuntos) que maximice el número de aristas que tienen un extremo en el primer subconjunto y un extremo en el segundo, en un grafo relacionado con el grafo de implicación, y aplicando métodos de programación semidefinida a este problema de corte, es posible encontrar en tiempo polinomial una solución aproximada que satisfaga al menos 0,940... veces el número óptimo de cláusulas. ^{[ 47 ]} 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 razón de aproximación a${\displaystyle \min \left\{(3-\cos \theta )^{-1}(2+(2/\pi )\theta )\,:\,\pi /2\leq \theta \leq \pi \right\}=0.943...}$. ^{[ 48 ]}

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

Varios autores también han explorado límites de tiempo exponenciales en el peor de los casos para la solución exacta de instancias MAX-2-SAT. ^{[ 51 ]}

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

El problema W2SAT incluye como caso especial el problema de cobertura de vértices , que consiste en encontrar un conjunto de k vértices que, en conjunto, 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 del grafo. Cada arista uv del grafo puede representarse mediante una cláusula 2SAT u ∨ v que solo puede satisfacerse incluyendo u o v entre las variables verdaderas de la solución. Entonces, las instancias que satisfacen la fórmula 2SAT resultante codifican soluciones al problema de cobertura de vértices, y existe una asignación satisfactoria con k variables verdaderas si y solo si existe una cobertura de vértices con k vértices. Por lo tanto, al igual que la cobertura de vértices, W2SAT es NP-completo . ^{[ 53 ]}

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

Además de encontrar el primer algoritmo de tiempo polinomial para la 2-satisfacibilidad, Krom (1967) también formuló el problema de evaluar fórmulas booleanas totalmente 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 puede resolverse en tiempo lineal, mediante una extensión de su técnica de componentes fuertemente conexas y ordenamiento topológico. ^{[ 3 ] [ 5 ]}

El problema de 2-satisfacibilidad también puede plantearse para lógicas multivaluadas proposicionales . Los algoritmos no suelen ser lineales, y para algunas lógicas el problema es incluso NP-completo. Véase Hähnle ( 2001 , 2003 ) para revisiones. ^{[ 55 ]}