Problema de satisfacibilidad booleano

Problema de determinar si una fórmula booleana podría hacerse verdadera

En lógica e informática , el problema de satisfacibilidad booleano (a veces llamado problema de satisfacibilidad proposicional y abreviado SATISFIABILIDAD , SAT o B-SAT ) es el problema de determinar si existe una interpretación que satisface una fórmula booleana dada . En otras palabras, pregunta si las variables de una fórmula booleana dada pueden ser reemplazadas consistentemente por los valores VERDADERO o FALSO de tal manera que la fórmula se evalúe como VERDADERA . Si este es el caso, la fórmula se llama satisfactoria. Por otro lado, si no existe tal asignación, la función expresada por la fórmula es FALSA para todas las posibles asignaciones de variables y la fórmula es insatisfactoria . Por ejemplo, la fórmula " a Y NO b " es satisfactoria porque uno puede encontrar los valores a  = VERDADERO yb  = FALSO, que hacen ( a Y NO b ) = VERDADERO. Por el contrario, " a AND NOT a " es insatisfactorio.

SAT es el primer problema que demostró ser NP-completo ; consulte el teorema de Cook-Levin . Esto significa que todos los problemas de la clase de complejidad NP , que incluye una amplia gama de problemas naturales de decisión y optimización, son a lo sumo tan difíciles de resolver como SAT. No existe un algoritmo conocido que resuelva de manera eficiente cada problema de SAT, y generalmente se cree que no existe tal algoritmo; sin embargo, esta creencia no ha sido probada matemáticamente, y resolver la cuestión de si SAT tiene un algoritmo de tiempo polinomial es equivalente al problema P versus NP , que es un famoso problema abierto en la teoría de la computación.

Sin embargo, a partir de 2007, los algoritmos heurísticos SAT pueden resolver casos de problemas que involucran decenas de miles de variables y fórmulas que constan de millones de símbolos, ^{[1] lo} cual es suficiente para muchos problemas prácticos SAT de, por ejemplo, inteligencia artificial , diseño de circuitos. , ^[2] y demostración automática de teoremas .

Definiciones y terminología básicas

Una fórmula lógica proposicional , también llamada expresión booleana , se construye a partir de variables , operadores AND ( conjunción , también denotada por ∧), OR ( disyunción , ∨), NOT ( negación , ¬) y paréntesis. Se dice que una fórmula es satisfactoria si se puede convertir en VERDADERA asignando valores lógicos apropiados (es decir, VERDADERO, FALSO) a sus variables. El problema de satisfacibilidad booleano (SAT) es, dada una fórmula, para verificar si es satisfactorio. Este problema de decisión es de vital importancia en muchas áreas de la informática , incluyendoinformática teórica , teoría de la complejidad , ^{[3] [4]} algoritmos , criptografía ^{[5] [6]} e inteligencia artificial . ^{[7] [se necesitan citas adicionales ]}

Hay varios casos especiales del problema de satisfacibilidad booleano en los que se requiere que las fórmulas tengan una estructura particular. Un literal es una variable, llamada literal positiva , o la negación de una variable, llamada literal negativa . Una cláusula es una disyunción de literales (o un solo literal). Una cláusula se denomina cláusula Horn si contiene como máximo un literal positivo. Una fórmula está en forma conjuntiva normal (CNF) si es una conjunción de cláusulas (o una sola cláusula). Por ejemplo, x ₁ es un literal positivo, ¬ x ₂ es un literal negativo, x ₁∨ ¬ x ₂ es una cláusula. La fórmula ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ está en forma normal conjuntiva; su primera y tercera cláusulas son cláusulas Horn, pero su segunda cláusula no lo es. La fórmula es satisfactoria, eligiendo x ₁  = FALSO, x ₂  = FALSO y x ₃ arbitrariamente, ya que (FALSO ∨ ¬FALSO) ∧ (¬FALSO ∨ FALSO ∨ x ₃ ) ∧ ¬FALSO se evalúa como (FALSO ∨ VERDADERO) ∧ (VERDADERO ∨ FALSO ∨ x ₃) ∧ VERDADERO, y a su vez a VERDADERO ∧ VERDADERO ∧ VERDADERO (es decir, a VERDADERO). Por el contrario, la fórmula CNF a ∧ ¬ a , que consta de dos cláusulas de un literal, no es satisfactoria, ya que para a = TRUE o a = FALSE se evalúa como TRUE ∧ ¬TRUE (es decir, FALSE) o FALSE ∧ ¬FALSE (es decir , nuevamente FALSO), respectivamente.

Para algunas versiones del problema SAT, es útil definir la noción de una fórmula de forma normal conjuntiva generalizada , a saber. como una conjunción de muchas cláusulas generalizadas arbitrariamente , siendo la última de la forma R ( l ₁ , ..., l _n ) para algún operador booleano R y literales (ordinarios) l _i . Diferentes conjuntos de operadores booleanos permitidos conducen a diferentes versiones de problemas. Por ejemplo, R (¬ x , a , b ) es una cláusula generalizada y R (¬ x , a ,b ) ∧ R ( b , y , c ) ∧ R ( c , d , ¬ z ) es una forma normal conjuntiva generalizada. Esta fórmula se usa a continuación , siendo R el operador ternario que es VERDADERO justo cuando exactamente uno de sus argumentos lo es.

Usando las leyes del álgebra de Boole , cada fórmula lógica proposicional se puede transformar en una forma normal conjuntiva equivalente, que puede, sin embargo, ser exponencialmente más larga. Por ejemplo, transformar la fórmula ( x ₁ ∧ y ₁ ) ∨ ( x ₂ ∧ y ₂ ) ∨ ... ∨ ( x _n ∧ y _n ) en forma normal conjuntiva produce

( X ₁  ∨  x ₂  ∨ ... ∨  x _n ) ∧

( y ₁  ∨  x ₂  ∨… ∨  x _n ) ∧

( x ₁  ∨  y ₂  ∨… ∨  x _n ) ∧

( y ₁  ∨  y ₂  ∨… ∨  x _n ) ∧ ... ∧

( x ₁  ∨  x ₂  ∨… ∨  y _n ) ∧

( y ₁  ∨  x ₂  ∨… ∨  y _n ) ∧

( x ₁  ∨  y ₂  ∨… ∨  y _n ) ∧

( y ₁  ∨  y ₂  ∨… ∨  y _n ) ;

mientras que la primera es una disyunción de n conjunciones de 2 variables, la última consta de 2 ⁿ cláusulas de n variables.

Complejidad y versiones restringidas

Satisfacibilidad sin restricciones (SAT)

SAT fue el primer problema NP-completo conocido , como lo demostró Stephen Cook en la Universidad de Toronto en 1971 ^[8] e independientemente por Leonid Levin en la Academia Nacional de Ciencias en 1973. ^[9] Hasta ese momento, el concepto de un El problema NP-completo ni siquiera existía. La prueba muestra cómo cada problema de decisión en la clase de complejidad NP se puede reducir al problema SAT para fórmulas CNF ^{[nota 1]} , a veces llamado CNFSAT. Una propiedad útil de la reducción de Cook es que conserva el número de respuestas aceptadas. Por ejemplo, decidir si una gráfica dada tiene 3 colores es otro problema en NP; si una gráfica tiene 17 3 colores válidos, la fórmula SAT producida por la reducción de Cook-Levin tendrá 17 asignaciones satisfactorias.

NP-completeness solo se refiere al tiempo de ejecución de las peores instancias. Muchos de los casos que ocurren en aplicaciones prácticas pueden resolverse mucho más rápidamente. Consulte Algoritmos para resolver SAT a continuación.

SAT es trivial si las fórmulas se restringen a aquellas en forma disyuntiva normal , es decir, son una disyunción de conjunciones de literales. Tal fórmula es de hecho satisfactoria si y solo si al menos una de sus conjunciones es satisfactoria, y una conjunción es satisfactoria si y solo si no contiene tanto x como NO x para alguna variable x . Esto se puede comprobar en tiempo lineal. Además, si están restringidos a estar en forma normal disyuntiva completa, en el que cada variable aparece exactamente una vez en cada conjunción, se pueden verificar en tiempo constante (cada conjunción representa una asignación satisfactoria). Pero puede llevar tiempo y espacio exponencial convertir un problema general de SAT a una forma normal disyuntiva; para un ejemplo, intercambie "∧" y "∨" en el ejemplo de explosión exponencial anterior por formas conjuntivas normales.

3-satisfacibilidad

La instancia de 3-SAT ( x ∨ x ∨ y ) ∧ (¬ x ∨ ¬ y ∨ ¬ y ) ∧ (¬ x ∨ y ∨ y ) se reduce a un problema de camarilla . Los vértices verdes forman una camarilla de 3 y corresponden a la asignación satisfactoria x = FALSO, y = VERDADERO.

Al igual que el problema de satisfacibilidad para fórmulas arbitrarias, determinar la satisfacibilidad de una fórmula en forma normal conjuntiva donde cada cláusula está limitada a un máximo de tres literales también es NP-completo; este problema se denomina 3-SAT , 3CNFSAT o 3-satisfacibilidad . Para reducir el problema de SAT sin restricciones a 3-SAT, transforme cada cláusula l ₁ ∨ ⋯ ∨ l _n en una conjunción de n - 2 cláusulas

( l ₁ ∨ l ₂ ∨ x ₂ ) ∧

(¬ x ₂ ∨ l ₃ ∨ x ₃ ) ∧

(¬ x ₃ ∨ l ₄ ∨ x ₄ ) ∧ ⋯ ∧

(¬ x _{norte - 3} ∨ l _{norte - 2} ∨ x _{norte - 2} ) ∧

(¬ x _{norte - 2} ∨ l _{norte - 1} ∨ l _norte )

donde x ₂ , ⋯,  x _{n - 2} son variables nuevas que no ocurren en ningún otro lugar. Aunque las dos fórmulas no son lógicamente equivalentes , son igualmente satisfactorias . La fórmula resultante de la transformación de todas las cláusulas es como máximo 3 veces más larga que su original, es decir, el crecimiento de la longitud es polinomial. ^[10]

3-SAT es uno de los 21 problemas NP-completos de Karp , y se utiliza como punto de partida para demostrar que otros problemas también son NP-difíciles . ^{[nota 2]} Esto se hace mediante la reducción del tiempo polinomial de 3-SAT al otro problema. Un ejemplo de un problema en el que se ha utilizado este método es el problema de la camarilla : dada una fórmula CNF que consta de cláusulas c , el gráfico correspondiente consta de un vértice para cada literal y un borde entre cada dos literales no contradictorios ^{[nota 3]} de diferentes cláusulas, cf. imagen. La gráfica tiene un c -clique si y solo si la fórmula es satisfactoria. ^[11]

Existe un algoritmo aleatorio simple de Schöning (1999) que se ejecuta en el tiempo (4/3) ⁿ donde n es el número de variables en la proposición 3-SAT, y tiene éxito con alta probabilidad para decidir correctamente 3-SAT. ^[12]

La hipótesis del tiempo exponencial afirma que ningún algoritmo puede resolver 3-SAT (o de hecho k -SAT para cualquier${\displaystyle k>2}$) en exp ( o ( n )) tiempo (es decir, fundamentalmente más rápido que exponencial en n ).

Selman, Mitchell y Levesque (1996) proporcionan datos empíricos sobre la dificultad de las fórmulas 3-SAT generadas al azar, dependiendo de sus parámetros de tamaño. La dificultad se mide en el número de llamadas recursivas realizadas por un algoritmo DPLL . ^[13]

3-satisfacibilidad se puede generalizar a k-satisfacibilidad ( k-SAT , también k-CNF-SAT ), cuando las fórmulas en CNF se consideran con cada cláusula que contiene hasta k literales. ^{[ cita requerida ]} Sin embargo, dado que para cualquier k ≥ 3, este problema no puede ser más fácil que el 3-SAT ni más difícil que el SAT, y los dos últimos son NP-completos, por lo que debe ser k-SAT.

Algunos autores restringen k-SAT a fórmulas CNF con exactamente k literales . ^{[ cita requerida ]} Esto tampoco conduce a una clase de complejidad diferente, ya que cada cláusula l ₁ ∨ ⋯ ∨ l _j con j < k literales se puede rellenar con variables ficticias fijas a l ₁ ∨ ⋯ ∨ l _j ∨ d _{j + 1} ∨ ⋯ ∨ d _k . Después de rellenar todas las cláusulas, se deben agregar 2 ^k -1 cláusulas adicionales ^{[nota 4]} para garantizar que solo d ₁ = ⋯ =d _k = FALSE puede conducir a una asignación satisfactoria. Dado que k no depende de la longitud de la fórmula, las cláusulas adicionales conducen a un aumento constante de la longitud. Por la misma razón, no importa sise permiten literales duplicados en las cláusulas, como en ¬ x ∨ ¬ y ∨ ¬ y .

Exactly-1 3-satisfiability

Izquierda: reducción de Schaefer de una cláusula 3-SAT x ∨ y ∨ z . El resultado de R es VERDADERO (1) si exactamente uno de sus argumentos es VERDADERO y FALSO (0) en caso contrario. Se examinan las 8 combinaciones de valores para x , y , z , una por línea. Las variables nuevas a , ..., f se pueden elegir para satisfacer todas las cláusulas (exactamente un argumento verde para cada R ) en todas las líneas excepto la primera, donde x ∨ y ∨ z es FALSO. Correcto: Una reducción más simple con las mismas propiedades.

Una variante del problema de satisfacibilidad de 3 es el 3-SAT de uno en tres (también conocido como 1-en-3-SAT y exactamente 1 3-SAT ). Dada una forma normal conjuntiva con tres literales por cláusula, el problema es determinar si existe una asignación de verdad a las variables de modo que cada cláusula tenga exactamente un literal VERDADERO (y por lo tanto exactamente dos literales FALSOS). En contraste, el 3-SAT ordinario requiere que cada cláusula tenga al menos un literal TRUE. Formalmente, un problema de 3-SAT de uno en tres se da como una forma normal conjuntiva generalizada con todas las cláusulas generalizadas usando un operador ternario Reso es VERDADERO solo si exactamente uno de sus argumentos lo es. Cuando todos los literales de una fórmula 3-SAT de uno de cada tres son positivos, el problema de satisfacibilidad se denomina 3-SAT positivo de uno de cada tres .

Uno de cada tres 3-SAT, junto con su caso positivo, aparece como problema NP-completo "LO4" en la referencia estándar, Computadoras e intratabilidad: una guía para la teoría de NP-Completitud por Michael R. Garey y David S. Johnson . Thomas Jerome Schaefer demostró que uno de cada tres 3-SAT es NP-completo como un caso especial del teorema de dicotomía de Schaefer , que afirma que cualquier problema que generalice la satisfacibilidad booleana de cierta manera está en la clase P o es NP- completo. ^[14]

Schaefer ofrece una construcción que permite una fácil reducción del tiempo polinomial de 3-SAT a uno de cada tres 3-SAT. Deje "( x o y o z )" haber una cláusula en una fórmula 3CNF. Agregue seis variables booleanas nuevas a , b , c , d , e y f , que se usarán para simular esta cláusula y ninguna otra. Entonces la fórmula R ( x , a , d ) ∧ R ( y , b , d ) ∧ R ( a , b , e) ∧ R ( c , d , f ) ∧ R ( z , c , FALSE) es satisfactorio por algún ajuste de las variables nuevas si y solo si al menos una de x , y , o z es VERDADERA, vea la imagen (izquierda) . Por lo tanto, cualquier instancia de 3-SAT con m cláusulas yn variables se puede convertir en una instancia de 3-SAT equisatisfactable de una de cada tres con 5 cláusulas my n +6 m variables. ^[15] Otra reducción implica solo cuatro variables nuevas y tres cláusulas: R(¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d , ¬ z ), vea la imagen (derecha).

3-satisfacibilidad no todos iguales

Otra variante es el problema de satisfacibilidad de 3 no todos iguales (también llamado NAE3SAT ). Dada una forma normal conjuntiva con tres literales por cláusula, el problema es determinar si existe una asignación a las variables de manera que en ninguna cláusula los tres literales tengan el mismo valor de verdad. Este problema también es NP-completo, incluso si no se admiten símbolos de negación, según el teorema de dicotomía de Schaefer. ^[14]

SAT lineal

Una fórmula 3-SAT es SAT lineal ( LSAT ) si cada cláusula (vista como un conjunto de literales) se cruza como máximo con otra cláusula y, además, si dos cláusulas se cruzan, entonces tienen exactamente un literal en común. Una fórmula LSAT se puede representar como un conjunto de intervalos semicerrados disjuntos en una línea. Decidir si una fórmula LSAT es satisfactoria o no es NP-completo. ^[dieciséis]

2-satisfacibilidad

SAT es más fácil si el número de literales en una cláusula se limita como máximo a 2, en cuyo caso el problema se denomina 2-SAT . Este problema puede resolverse en tiempo polinomial, y de hecho está completo para la clase de complejidad NL . Si, además, la totalidad o las operaciones en los literales se cambian a XOR operaciones, el resultado se llama exclusiva-o 2-satisfacibilidad , que es un completo problema para la clase de complejidad SL = L .

Satisfacción del cuerno

El problema de decidir la satisfacibilidad de una conjunción dada de cláusulas de Horn se llama satisfacibilidad de Horn , o HORN-SAT . Puede resolverse en tiempo polinomial mediante un solo paso del algoritmo de propagación Unit , que produce el modelo mínimo único del conjunto de cláusulas de Horn (es decir, el conjunto de literales asignados a TRUE). La satisfacción del cuerno es P-completa . Puede verse como la versión de P del problema de satisfacibilidad booleano. Además, se puede decidir la verdad de las fórmulas de Horn cuantificadas en tiempo polinomial. ^[17]

Las cláusulas de Horn son de interés porque pueden expresar la implicación de una variable de un conjunto de otras variables. De hecho, una de esas cláusulas ¬ x ₁ ∨ ... ∨ ¬ x _n ∨ y puede reescribirse como x ₁ ∧ ... ∧ x _n → y , es decir, si x ₁ , ..., x _n son todas VERDADERAS , entonces y también debe ser VERDADERO.

Una generalización de la clase de fórmulas de Horn es la de las fórmulas de Horn renombrables, que es el conjunto de fórmulas que se pueden colocar en forma de Horn reemplazando algunas variables con su respectiva negación. Por ejemplo, ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ no es una fórmula de Horn, pero se puede cambiar el nombre a la fórmula de Horn ( x ₁ ∨ ¬ x ₂ ) ∧ (¬ x ₁ ∨ x ₂ ∨ ¬ y ₃ ) ∧ ¬ x ₁ introduciendoy ₃ como negación de x ₃ . Por el contrario, ningún cambio de nombre de ( x ₁ ∨ ¬ x ₂ ∨ ¬ x ₃ ) ∧ (¬ x ₁ ∨ x ₂ ∨ x ₃ ) ∧ ¬ x ₁ conduce a una fórmula de Horn. La verificación de la existencia de tal reemplazo se puede hacer en tiempo lineal; por lo tanto, la satisfacibilidad de tales fórmulas está en P, ya que se puede resolver realizando primero este reemplazo y luego verificando la satisfacibilidad de la fórmula de Horn resultante.

Una fórmula con 2 cláusulas puede estar insatisfecha (rojo), 3-satisfecho (verde), xo-3-satisfecho (azul) o / y 1-en-3-satisfecho (amarillo), según el recuento de TRUE-literal en la cláusula 1st (hor) y 2nd (vert).

Satisfacción XOR

Resolviendo un ejemplo de XOR-SAT por eliminación gaussiana
Fórmula dada ("⊕" significa XOR, la cláusula roja es opcional) ( Un ⊕ c ⊕ d ) ∧ ( b ⊕¬ c ⊕ d ) ∧ ( un ⊕ b ⊕¬ d ) ∧ ( un ⊕¬ b ⊕¬ c ) ∧ (¬ un ⊕ b ⊕ c )
Sistema de ecuaciones ("1" significa VERDADERO, "0" significa FALSO) Cada cláusula conduce a una ecuación. a ⊕ C ⊕ D = 1 B ⊕ ¬ C ⊕ D = 1 a ⊕ B ⊕ ¬ D = 1 a ⊕ ¬ B ⊕ ¬ C = 1 ¬ a ⊕ B ⊕ C ≃ 1
Sistema de ecuaciones normalizadas using properties of Boolean rings (¬x=1⊕x, x⊕x=0) a ⊕ c ⊕ d = 1 b ⊕ c ⊕ d = 0 a ⊕ b ⊕ d = 0 a ⊕ b ⊕ c = 1 a ⊕ b ⊕ c ≃ 0 (If the red equation is present, it contradicts the last black one, so the system is unsolvable. Therefore, Gauss' algorithm is used only for the black equations.)
Associated coefficient matrix   a b c d line   1 0 1 1 1 A 0 1 1 1 0 B 1 1 0 1 0 C 1 1 1 0 1 D
Transforming to echelon form   a b c d operation   1 0 1 1 1 A 1 1 0 1 0 C 1 1 1 0 1 D 0 1 1 1 0 B (swapped)   1 0 1 1 1 A 0 1 1 0 1 E = C⊕A 0 1 0 1 0 F = D⊕A 0 1 1 1 0 B   1 0 1 1 1 A 0 1 1 0 1 E 0 0 1 1 1 G = F⊕E 0 0 0 1 1 H = B⊕E
Transforming to diagonal form   a b c d operation   1 0 1 0 0 I = A⊕H 0 1 1 0 1 E 0 0 1 0 0 J = G⊕H 0 0 0 1 1 H   1 0 0 0 0 K = I⊕J 0 1 0 0 1 L = E⊕J 0 0 1 0 0 J 0 0 0 1 1 H
Solution: If the red clause is present: Unsolvable Else: a = 0 = FALSE b = 1 = TRUE c = 0 = FALSE d = 1 = TRUE As a consequence: R(a,c,d) ∧ R(b,¬c,d) ∧ R(a,b,¬d) ∧ R(a,¬b,¬c) ∧ R(¬a,b,c) is not 1-in-3-satisfiable, while (a ∨ c ∨ d) ∧ (b ∨ ¬c ∨ d) ∧ (a ∨ b ∨ ¬d) ∧ (a ∨ ¬b ∨ ¬c) is 3-satisfiable with a=c=FALSE and b=d=TRUE.

Otro caso especial es la clase de problemas donde cada cláusula contiene operadores XOR (es decir, exclusivos o ) en lugar de operadores OR (simples). ^{[nota 5]} Esto está en P , ya que una fórmula XOR-SAT también puede verse como un sistema de ecuaciones lineales mod 2, y puede resolverse en tiempo cúbico por eliminación gaussiana ; ^[18] vea el recuadro para ver un ejemplo. Esta refundición se basa en el parentesco entre las álgebras booleanas y los anillos booleanos , y el hecho de que el módulo aritmético dos forma un campo finito . Dado que a XOR b XOR c se evalúa como VERDADERO si y solo si exactamente 1 o 3 miembros de { a ,b , c } son VERDADERAS, cada solución del problema 1-en-3-SAT para una fórmula CNF dada es también una solución del problema XOR-3-SAT y, a su vez, cada solución de XOR-3-SAT es una solución de 3-SAT, cf. imagen. Como consecuencia, para cada fórmula CNF, es posible resolver el problema XOR-3-SAT definido por la fórmula, y con base en el resultado inferir que el problema 3-SAT se puede resolver o que el 1-en-3- El problema del SAT no tiene solución.

Siempre que las clases de complejidad P y NP no sean iguales , ni 2-, ni Horn-, ni XOR-satisfiability es NP-complete, a diferencia de SAT.

Teorema de la dicotomía de Schaefer

Las restricciones anteriores (CNF, 2CNF, 3CNF, Horn, XOR-SAT) unieron las fórmulas consideradas como conjunciones de subfórmulas; cada restricción establece una forma específica para todas las subfórmulas: por ejemplo, solo las cláusulas binarias pueden ser subfórmulas en 2CNF.

El teorema de la dicotomía de Schaefer establece que, para cualquier restricción a los operadores booleanos que se puedan usar para formar estas subfórmulas, el problema de satisfacibilidad correspondiente está en P o NP-completo. La pertenencia a P de la satisfacibilidad de las fórmulas 2CNF, Horn y XOR-SAT son casos especiales de este teorema. ^[14]

La siguiente tabla resume algunas variantes comunes de SAT.

Código	Nombre	Restricciones	Requisitos	Clase
3SAT	3-satisfacibilidad	Cada cláusula contiene 3 literales.	Al menos un literal debe ser verdadero.	NPC
2SAT	2-satisfacibilidad	Cada cláusula contiene 2 literales.	Al menos un literal debe ser verdadero.	PAG
1 en 3 SAT	Exactamente 1 3-SAT	Cada cláusula contiene 3 literales.	Exactamente un literal debe ser verdadero.	NPC
1 en 3 SAT +	Exactamente-1 positivo 3-SAT	Cada cláusula contiene 3 literales positivos.	Exactamente un literal debe ser verdadero.	NPC
NAE3SAT	No todos iguales 3-satisfacibilidad	Cada cláusula contiene 3 literales.	Uno o dos literales deben ser verdaderos.	NPC
NAE3SAT +	3-SAT positivo no todos iguales	Cada cláusula contiene 3 literales positivos.	Uno o dos literales deben ser verdaderos.	NPC
PL-SAT	Planar SAT	El gráfico de incidencia (gráfico de cláusula variable) es plano .	Al menos un literal debe ser verdadero.	NPC
L3SAT	Lineal 3-SAT	Cada cláusula se cruza como máximo con otra cláusula, y la intersección es exactamente un literal.	Al menos un literal debe ser verdadero.	NPC
HORN-SAT	Satisfacción del cuerno	Cláusulas Horn (como máximo un literal positivo).	Al menos un literal debe ser verdadero.	PAG
XOR-SAT	Xor satisfacibilidad	Cada cláusula contiene operaciones XOR en lugar de OR.	El XOR de todos los literales debe ser verdadero.	PAG

Extensiones de SAT

Una extensión que ha ganado una popularidad significativa desde 2003 son las teorías de módulo de satisfacibilidad ( SMT ) que pueden enriquecer las fórmulas CNF con restricciones lineales, matrices, restricciones totalmente diferentes, funciones no interpretadas , ^[19] etc. Tales extensiones generalmente permanecen NP-completas, pero muy Ahora hay disponibles solucionadores eficientes que pueden manejar muchos de estos tipos de restricciones.

El problema de la satisfacibilidad se vuelve más difícil si se permite que tanto los cuantificadores "para todos" ( ∀ ) como "existe" ( ∃ ) enlacen las variables booleanas. Un ejemplo de tal expresión sería ∀ x ∀ y ∃ z ( x ∨ y ∨ z ) ∧ (¬ x ∨ ¬ y ∨ ¬ z ) ; es válida, ya que para todos los valores de x y y , un valor apropiado de z se puede encontrar, a saber. z = VERDADERO si tanto x como yson FALSE, yz = FALSE si no. El propio SAT (tácitamente) utiliza solo ∃ cuantificadores. Si en su lugar solo se permiten ∀ cuantificadores, se obtiene el llamado problema de tautología , que es co-NP-completo . Si se permiten ambos cuantificadores, el problema se denomina problema de fórmula booleana cuantificada ( QBF ), que puede demostrarse que es PSPACE completo . Se cree ampliamente que los problemas completos de PSPACE son estrictamente más difíciles que cualquier problema en NP, aunque esto aún no se ha demostrado. Utilizando sistemas P altamente paralelos , los problemas QBF-SAT se pueden resolver en tiempo lineal. ^[20]

El SAT ordinario pregunta si hay al menos una asignación de variable que hace que la fórmula sea verdadera. Una variedad de variantes se ocupan del número de tales asignaciones:

• MAJ-SAT pregunta si la mayoría de las asignaciones hacen que la fórmula sea VERDADERA. Se sabe que está completo para PP , una clase probabilística.
• #SAT , el problema de contar cuántas asignaciones de variables satisfacen una fórmula, es un problema de conteo, no un problema de decisión, y es # P-completo .
• UNIQUE SAT ^[21] es el problema de determinar si una fórmula tiene exactamente una asignación. Es completo para EE . UU. , ^[22] la clase de complejidad que describe problemas que se pueden resolver mediante una máquina de Turing de tiempo polinomial no determinista que acepta cuando hay exactamente una ruta de aceptación no determinista y rechaza de otro modo.
• UNAMBIGUOUS-SAT es el nombre que se le da al problema de satisfacibilidad cuando la entrada se restringe a fórmulas que tienen como máximo una asignación satisfactoria. El problema también se llama USAT . ^[23] Se permite que un algoritmo de resolución para UNAMBIGUOUS-SAT muestre cualquier comportamiento, incluido el bucle sin fin, en una fórmula que tiene varias asignaciones satisfactorias. Aunque este problema parece más fácil, Valiant y Vazirani han demostrado ^[24] que si existe un algoritmo práctico (es decir, polinomial-tiempo aleatorio ) para resolverlo, entonces todos los problemas en NP pueden resolverse con la misma facilidad.
• MAX-SAT , el problema de máxima satisfacibilidad , es una generalización FNP de SAT. Pregunta el número máximo de cláusulas que puede satisfacer cualquier cesión. Tiene algoritmos de aproximación eficientes , pero es NP-difícil de resolver exactamente. Peor aún, es APX -completo, lo que significa que no hay un esquema de aproximación de tiempo polinómico (PTAS) para este problema a menos que P = NP.
• WMSAT es el problema de encontrar una asignación de peso mínimo que satisfaga una fórmula booleana monótona (es decir, una fórmula sin ninguna negación). Los pesos de las variables proposicionales se dan en la entrada del problema. El peso de una asignación es la suma de los pesos de las variables verdaderas. Ese problema es NP-completo (ver Th. 1 de ^[25] ).

Otras generalizaciones incluyen la satisfacibilidad para la lógica de primer y segundo orden , problemas de satisfacción de restricciones , programación de enteros 0-1 .

Autorreductibilidad

El problema de SAT es autorreducible , es decir, cada algoritmo que responde correctamente si una instancia de SAT tiene solución se puede utilizar para encontrar una asignación satisfactoria. Primero, la pregunta se hace con la fórmula dada Φ. Si la respuesta es "no", la fórmula no es satisfactoria. De lo contrario, la pregunta se hace en la fórmula parcialmente instanciada Φ { x 1 = VERDADERO} , es decir, Φ con la primera variable x ₁ reemplazada por VERDADERA, y simplificada en consecuencia. Si la respuesta es "sí", entonces x ₁ = VERDADERO, de lo contrario x ₁ = FALSO. Los valores de otras variables se pueden encontrar posteriormente de la misma manera. En total, se requieren n +1 ejecuciones del algoritmo, donden es el número de variables distintas en Φ.

Esta propiedad de autorreductibilidad se utiliza en varios teoremas de la teoría de la complejidad:

NP ⊆ P / poli ⇒ PH = Σ 2   ( teorema de Karp-Lipton )

NP ⊆ BPP ⇒ NP = RP

P = NP ⇒ FP = FNP

Algoritmos para resolver SAT

Dado que el problema SAT es NP-completo, solo se conocen los algoritmos con complejidad exponencial en el peor de los casos. A pesar de esto, se desarrollaron algoritmos eficientes y escalables para SAT durante la década de 2000 y han contribuido a avances dramáticos en nuestra capacidad para resolver automáticamente casos de problemas que involucran decenas de miles de variables y millones de restricciones (es decir, cláusulas). ^[1] Ejemplos de tales problemas en la automatización del diseño electrónico (EDA) incluyen verificación de equivalencia formal , verificación de modelo , verificación formal de microprocesadores en cadena , ^[19] generación automática de patrones de prueba , enrutamiento de FPGA, ^[26] de planificación y programación de problemas , y así sucesivamente. Un motor de resolución de SAT ahora se considera un componente esencial en la caja de herramientas de EDA .

Un solucionador de DPLL SAT emplea un procedimiento de búsqueda de retroceso sistemático para explorar el espacio (de tamaño exponencial) de asignaciones de variables en busca de asignaciones satisfactorias. El procedimiento de búsqueda básico se propuso en dos artículos seminales a principios de la década de 1960 (véanse las referencias a continuación) y ahora se lo conoce comúnmente como el algoritmo Davis-Putnam-Logemann-Loveland ("DPLL" o "DLL"). ^{[27] [28]} Muchos enfoques modernos para la resolución práctica de SAT se derivan del algoritmo DPLL y comparten la misma estructura. A menudo, solo mejoran la eficiencia de ciertas clases de problemas de SAT, como instancias que aparecen en aplicaciones industriales o instancias generadas aleatoriamente. ^[29] Teóricamente, se han demostrado límites inferiores exponenciales para la familia de algoritmos DPLL.^{[ cita requerida ]}

Los algoritmos que no forman parte de la familia DPLL incluyen algoritmos de búsqueda local estocástica . Un ejemplo es WalkSAT . Los métodos estocásticos intentan encontrar una interpretación satisfactoria, pero no pueden deducir que una instancia de SAT no sea satisfactoria, a diferencia de los algoritmos completos, como DPLL. ^[29]

Por el contrario, los algoritmos aleatorios como el algoritmo PPSZ de Paturi, Pudlak, Saks y Zane establecen las variables en un orden aleatorio de acuerdo con algunas heurísticas, por ejemplo, la resolución de ancho acotado . Si la heurística no puede encontrar la configuración correcta, la variable se asigna al azar. El algoritmo PPSZ tiene un tiempo de ejecución ^{[ aclarar ]} de${\displaystyle O(1.308^{n})}$para 3-SAT. Este fue el tiempo de ejecución más conocido para este problema hasta una mejora reciente de Hansen, Kaplan, Zamir y Zwick que tiene un tiempo de ejecución de${\displaystyle O(1.307^{n})}$para 3-SAT y actualmente el tiempo de ejecución más conocido para k-SAT, para todos los valores de k. En el entorno con muchas asignaciones satisfactorias, el algoritmo aleatorio de Schöning tiene un mejor límite. ^{[12] [30] [31]}

Los solucionadores de SAT modernos (desarrollados en la década de 2000) vienen en dos versiones: "impulsados ​​por conflictos" y "anticipados". Ambos enfoques descienden de DPLL. ^[29] solucionadores impulsadas por el conflicto, como el conflicto impulsado por la cláusula de aprendizaje (CDCl), aumentar el algoritmo de búsqueda DPLL básico con el análisis de conflictos eficiente, el aprendizaje cláusula, no retroceso cronológico (también conocido como backjumping ), así como de "dos watched- propagación de unidades de literales " , ramificación adaptativa y reinicios aleatorios. Se ha demostrado empíricamente que estos "extras" de la búsqueda sistemática básica son esenciales para manejar las grandes instancias de SAT que surgen en la automatización del diseño electrónico (EDA). ^[32]Las implementaciones bien conocidas incluyen Chaff ^[33] y GRASP . ^[34] Los solucionadores de anticipación han fortalecido especialmente las reducciones (que van más allá de la propagación de cláusulas unitarias) y la heurística, y generalmente son más fuertes que los solucionadores de conflictos en instancias difíciles (mientras que los solucionadores de conflictos pueden ser mucho mejores en instancias grandes que en realidad tiene una instancia fácil en el interior).

Los solucionadores de SAT modernos también están teniendo un impacto significativo en los campos de verificación de software, resolución de restricciones en inteligencia artificial e investigación de operaciones, entre otros. Los potentes solucionadores están disponibles como software gratuito y de código abierto . En particular, el MiniSAT impulsado por conflictos , que fue relativamente exitoso en la competencia SAT de 2005 , solo tiene alrededor de 600 líneas de código. Un solucionador moderno de Parallel SAT es ManySAT. ^[35] Puede lograr aceleraciones súper lineales en clases importantes de problemas. Un ejemplo de solucionadores anticipados es march_dl , que ganó un premio en la competencia SAT de 2007 .

Ciertos tipos de grandes instancias aleatorias satisfactorias de SAT pueden resolverse mediante la propagación de encuestas (SP). Particularmente en aplicaciones de verificación y diseño de hardware , la satisfacibilidad y otras propiedades lógicas de una fórmula proposicional dada a veces se deciden basándose en una representación de la fórmula como un diagrama de decisión binario (BDD).

Casi todos los solucionadores de SAT incluyen tiempos de espera, por lo que finalizarán en un tiempo razonable incluso si no pueden encontrar una solución. Los diferentes solucionadores de SAT encontrarán diferentes instancias fáciles o difíciles, y algunos sobresalen en demostrar insatisfacción y otros en encontrar soluciones. Todos estos comportamientos se pueden ver en los concursos de resolución de SAT. ^[36]

Resolución de SAT en paralelo

Los solucionadores SAT paralelos vienen en tres categorías: cartera, divide y vencerás y algoritmos de búsqueda local paralela . Con carteras paralelas, varios solucionadores SAT diferentes se ejecutan al mismo tiempo. Cada uno de ellos resuelve una copia de la instancia SAT, mientras que los algoritmos de divide y vencerás dividen el problema entre los procesadores. Existen diferentes enfoques para paralelizar los algoritmos de búsqueda local.

El Concurso Internacional de SAT Solver tiene una pista paralela que refleja los avances recientes en la resolución de SAT en paralelo. En 2016, ^[37] 2017 ^[38] y 2018, ^[39] los puntos de referencia se ejecutaron en un sistema de memoria compartida con 24 núcleos de procesamiento , por lo tanto, los solucionadores destinados a la memoria distribuida o los procesadores de muchos núcleos podrían haberse quedado cortos.

Portafolios

En general, no hay un solucionador SAT que funcione mejor que todos los demás solucionadores en todos los problemas SAT. Un algoritmo puede funcionar bien para casos de problemas con los que otros luchan, pero lo hará peor con otros casos. Además, dada una instancia de SAT, no existe una forma confiable de predecir qué algoritmo resolverá esta instancia de manera particularmente rápida. Estas limitaciones motivan el enfoque de cartera paralela. Una cartera es un conjunto de diferentes algoritmos o diferentes configuraciones del mismo algoritmo. Todos los solucionadores de una cartera paralela se ejecutan en diferentes procesadores para resolver el mismo problema. Si un solucionador termina, el solucionador de cartera informa que el problema es satisfactorio o insatisfactorio según este solucionador. Todos los demás solucionadores finalizan. Diversificar carteras al incluir una variedad de solucionadores,cada uno con un buen desempeño en un conjunto diferente de problemas, aumenta la solidez del solucionador.^[40]

Muchos solucionadores utilizan internamente un generador de números aleatorios . Diversificar sus semillas es una forma sencilla de diversificar una cartera. Otras estrategias de diversificación implican habilitar, deshabilitar o diversificar ciertas heurísticas en el solucionador secuencial. ^[41]

Un inconveniente de las carteras paralelas es la cantidad de trabajo duplicado. Si se utiliza el aprendizaje de cláusulas en los solucionadores secuenciales, compartir las cláusulas aprendidas entre los solucionadores que se ejecutan en paralelo puede reducir el trabajo duplicado y aumentar el rendimiento. Sin embargo, incluso simplemente ejecutar una cartera de los mejores solucionadores en paralelo lo convierte en un solucionador paralelo competitivo. Un ejemplo de un solucionador de este tipo es PPfolio. ^{[42] [43]} Fue diseñado para encontrar un límite inferior para el rendimiento que un solucionador SAT paralelo debería poder ofrecer. A pesar de la gran cantidad de trabajo duplicado debido a la falta de optimizaciones, funcionó bien en una máquina de memoria compartida. HordeSat ^[44]es un solucionador de carteras paralelo para grandes grupos de nodos informáticos. Utiliza instancias configuradas de manera diferente del mismo solucionador secuencial en su núcleo. Particularmente para instancias de SAT difíciles, HordeSat puede producir aceleraciones lineales y, por lo tanto, reducir significativamente el tiempo de ejecución.

En los últimos años, los solucionadores SAT de cartera paralela han dominado la pista paralela de las competiciones internacionales de solucionadores SAT . Ejemplos notables de tales solucionadores incluyen Plingeling y painless-mcomsps. ^[45]

Divide y vencerás

A diferencia de los portafolios paralelos, el sistema divide y vencerás en paralelo intenta dividir el espacio de búsqueda entre los elementos de procesamiento. Los algoritmos de divide y vencerás, como el DPLL secuencial, ya aplican la técnica de dividir el espacio de búsqueda, por lo que su extensión hacia un algoritmo paralelo es sencilla. Sin embargo, debido a técnicas como la propagación unitaria, después de una división, los problemas parciales pueden diferir significativamente en complejidad. Por lo tanto, el algoritmo DPLL generalmente no procesa cada parte del espacio de búsqueda en la misma cantidad de tiempo, lo que genera un problema de equilibrio de carga desafiante . ^[40]

Fase de cubo para la fórmula ${\displaystyle F}$. La heurística de decisión elige qué variables (círculos) asignar. Después de que la heurística de corte decide detener la ramificación adicional, los problemas parciales (rectángulos) se resuelven de forma independiente utilizando CDCL.

Debido al retroceso no cronológico, la paralelización del aprendizaje de cláusulas impulsado por conflictos es más difícil. Una forma de superar esto es el paradigma Cube-and-Conquer . ^[46] Sugiere resolver en dos fases. En la fase "cubo", el Problema se divide en varios miles, hasta millones, de secciones. Esto lo hace un solucionador de anticipación, que encuentra un conjunto de configuraciones parciales llamadas "cubos". Un cubo también puede verse como una conjunción de un subconjunto de variables de la fórmula original. Junto con la fórmula, cada uno de los cubos forma una nueva fórmula. Estas fórmulas se pueden resolver de forma independiente y simultánea mediante solucionadores de conflictos. Como la disyunción de estas fórmulas es equivalenteSegún la fórmula original, se informa que el problema es satisfactorio, si una de las fórmulas es satisfactoria. El solucionador de anticipación es favorable para problemas pequeños pero difíciles, ^[47]por lo que se utiliza para dividir gradualmente el problema en múltiples subproblemas. Estos subproblemas son más fáciles pero aún grandes, que es la forma ideal para un solucionador impulsado por conflictos. Además, los solucionadores anticipados consideran todo el problema, mientras que los solucionadores impulsados ​​por conflictos toman decisiones basadas en información que es mucho más local. Hay tres heurísticas involucradas en la fase del cubo. Las variables de los cubos se eligen mediante la heurística de decisión. La heurística de dirección decide qué asignación de variable (verdadera o falsa) explorar primero. En casos de problemas satisfactorios, es beneficioso elegir primero una rama satisfactoria. La heurística de corte decide cuándo dejar de expandir un cubo y, en su lugar, reenviarlo a un solucionador secuencial basado en conflictos. Preferiblemente, los cubos son igualmente complejos de resolver. ^[46]

Treengeling es un ejemplo de un solucionador paralelo que aplica el paradigma Cube-and-Conquer. Desde su introducción en 2012, ha tenido múltiples éxitos en el Concurso Internacional SAT Solver . Cube-and-Conquer se utilizó para resolver el problema de los triples booleanos pitagóricos . ^[48]

Búsqueda local

Una estrategia hacia un algoritmo de búsqueda local paralelo para la resolución de SAT es probar múltiples cambios de variable simultáneamente en diferentes unidades de procesamiento. ^[49] Otra es aplicar el enfoque de cartera mencionado anteriormente, sin embargo, no es posible compartir cláusulas ya que los solucionadores de búsquedas locales no producen cláusulas. Alternativamente, es posible compartir las configuraciones que se producen localmente. Estas configuraciones se pueden utilizar para guiar la producción de una nueva configuración inicial cuando un solucionador local decide reiniciar su búsqueda. ^[50]

Ver también

• Núcleo insatisfactorio
• Teorías del módulo de satisfacción
• Contando SAT
• Planar SAT
• Algoritmo de Karloff-Zwick
• Satisfacción del circuito

Notas

1. El problema de SAT parafórmulas arbitrarias también es NP-completo, ya que se muestra fácilmente que está en NP, y no puede ser más fácil que SAT para fórmulas CNF.
2. es decir, al menos tan difícil como cualquier otro problema en NP. Un problema de decisión es NP-completo si y solo si está en NP y es NP-difícil.
3. es decir, tal que un literal no es la negación del otro
4. saber. todos los maxterms que se pueden construir con d ₁ , ⋯, d _k , excepto d ₁ ∨ ⋯ ∨ d _k
5. Formalmente,se empleanformas normales conjuntivas generalizadas con un operador booleano ternario R , que es VERDADERO solo si 1 o 3 de sus argumentos lo es. Una cláusula de entrada con más de 3 literales se puede transformar en una conjunción equisatisfactable de cláusulas á 3 literales similar a la anterior ; es decir, XOR-SAT se puede reducir a XOR-3-SAT.

Referencias

1. Ohrimenko, Olga; Stuckey, Peter J .; Codish, Michael (2007), "Propagation = Lazy Clause Generation", Principles and Practice of Constraint Programming - CP 2007 , Lecture Notes in Computer Science, 4741 , págs. 544–558, CiteSeerX  10.1.1.70.5471 , doi : 10.1007 / 978-3-540-74970-7_39 , los solucionadores de SAT modernos a menudo pueden manejar problemas con millones de restricciones y cientos de miles de variables.
2. Hong, Ted; Li, Yanjing; Park, Sung-Boem; Mui, Diana; Lin, David; Kaleq, Ziyad Abdel; Hakim, Nagib; Naeimi, Helia; Gardner, Donald S .; Mitra, Subhasish (noviembre de 2010). "QED: Pruebas de detección rápida de errores para una validación posterior al silicio eficaz". Conferencia internacional de pruebas IEEE 2010 : 1–10. doi : 10.1109 / TEST.2010.5699215 . ISBN 978-1-4244-7206-2. S2CID  7909084 .
3. Karp, Richard M. (1972). "Reducibilidad entre problemas combinatorios" (PDF) . En Raymond E. Miller; James W. Thatcher (eds.). Complejidad de los cálculos informáticos . Nueva York: Pleno. págs. 85-103. ISBN  0-306-30707-3. Archivado desde el original (PDF) el 29 de junio de 2011 . Consultado el 7 de mayo de 2020 . Aquí: p.86
4. Alfred V. Aho y John E. Hopcroft y Jeffrey D. Ullman (1974). El diseño y análisis de algoritmos informáticos . Lectura / MA: Addison-Wesley. ISBN 0-201-00029-6. Aquí: p.403
5. Massacci, Fabio; Marraro, Laura (1 de febrero de 2000). "Criptoanálisis lógico como problema SAT" . Revista de razonamiento automatizado . 24 (1): 165-203. doi : 10.1023 / A: 1006326723002 . ISSN 1573-0670 . 
6. Mironov, Ilya; Zhang, Lintao (2006). Biere, Armin; Gomes, Carla P. (eds.). "Aplicaciones de SAT Solvers al criptoanálisis de funciones hash" . Teoría y aplicaciones de las pruebas de satisfacción - SAT 2006 . Apuntes de conferencias en Ciencias de la Computación. Berlín, Heidelberg: Springer. 4121 : 102-115. doi : 10.1007 / 11814948_13 . ISBN 978-3-540-37207-3.
7. Vizel, Y .; Weissenbacher, G .; Malik, S. (2015). "Solucionadores de satisfacción booleana y sus aplicaciones en la comprobación de modelos". Actas del IEEE . 103 (11): 2021-2035. doi : 10.1109 / JPROC.2015.2455034 . S2CID 10190144 . 
8. Cook, Stephen A. (1971). "La complejidad de los procedimientos de demostración de teoremas" (PDF) . Actas del 3er Simposio Anual de ACM sobre Teoría de la Computación : 151-158. CiteSeerX 10.1.1.406.395 . doi : 10.1145 / 800157.805047 . S2CID 7573663 .   
9. Levin, Leonid (1973). "Problemas de búsqueda universal (ruso: Универсальные задачи перебора, Universal'nye perebornye zadachi)". Problemas de transmisión de información (ruso: Проблемы передачи информа́ции, Problemy Peredachi Informatsii) . 9 (3): 115-116. (pdf) (en ruso) , traducido al inglés por Trakhtenbrot, BA (1984). "Una encuesta de enfoques rusos a los algoritmos de perebor (búsquedas de fuerza bruta)". Anales de la historia de la informática . 6 (4): 384–400. doi : 10.1109 / MAHC.1984.10036 . S2CID 950581 . 
10. Alfred V. Aho; John E. Hopcroft; Jeffrey D. Ullman (1974). El diseño y análisis de algoritmos informáticos . Addison-Wesley.; aquí: Thm.10.4
11. Aho, Hopcroft, Ullman ^[10] (1974); Thm.10.5
12. Schöning, Uwe (octubre de 1999). "Un algoritmo probabilístico para k- SAT y problemas de satisfacción de restricciones" (PDF) . Proc. 40th Ann. Symp. Fundamentos de la informática . págs. 410–414. doi : 10.1109 / SFFCS.1999.814612 . ISBN  0-7695-0409-4. S2CID  123177576 .
13. Bart Selman; David Mitchell; Héctor Levesque (1996). "Generando Problemas Duros de Satisfacción". Inteligencia artificial . 81 (1–2): 17–29. CiteSeerX 10.1.1.37.7362 . doi : 10.1016 / 0004-3702 (95) 00045-3 . 
14. Schaefer, Thomas J. (1978). "La complejidad de los problemas de satisfacibilidad" (PDF) . Actas del X Simposio Anual ACM sobre Teoría de la Computación . San Diego, California. págs. 216–226.
15. (Schaefer, 1978), p. 222, Lema 3.5
16. Arkin, Esther M .; Banik, Aritra; Carmi, Paz; Citovsky, Gui; Katz, Matthew J .; Mitchell, Joseph SB; Simakov, Marina (11 de diciembre de 2018). "Seleccionar y cubrir puntos de colores" . Matemáticas aplicadas discretas . 250 : 75–86. doi : 10.1016 / j.dam.2018.05.011 . ISSN 0166-218X . 
17. Buning, HK; Karpinski, Marek; Flogel, A. (1995). "Resolución de fórmulas booleanas cuantificadas" . Información y Computación . Elsevier. 117 (1): 12–18. doi : 10.1006 / inco.1995.1025 .
18. Moore, Cristopher ; Mertens, Stephan (2011), La naturaleza de la computación , Oxford University Press, pág. 366, ISBN 9780199233212.
19. R. E. Bryant, SM German y MN Velev, Verificación de microprocesador mediante procedimientos de decisión eficientes para una lógica de igualdad con funciones no interpretadas , en cuadros analíticos y métodos relacionados, págs. 1-13, 1999.
20. Alhazov, Artiom; Martín-Vide, Carlos; Pan, Linqiang (2003). "Resolver un problema completo de PSPACE mediante el reconocimiento de sistemas P con membranas activas restringidas" . Fundamenta Informaticae . 58 : 67–77. Aquí: Sección 3, Teo 3.1
21. Blass, Andreas; Gurevich, Yuri (1 de octubre de 1982). "Sobre el problema de la satisfacibilidad única" . Información y control . 55 (1): 80–88. doi : 10.1016 / S0019-9958 (82) 90439-9 . ISSN 0019-9958 . 
22. "Complejidad zoológico: U - Complejidad zoológico" . ComplexZoo.uwaterloo.ca . Archivado desde el original el 9 de julio de 2019 . Consultado el 5 de diciembre de 2019 .
23. Kozen, Dexter C. (2006). "Clase complementaria F: Satisfabilidad única" . Teoría de la Computación . Textos en Informática. Londres: Springer-Verlag. pag. 180. ISBN 9781846282973.
24. Valiente, L .; Vazirani, V. (1986). "NP es tan fácil como detectar soluciones únicas" (PDF) . Informática Teórica . 47 : 85–93. doi : 10.1016 / 0304-3975 (86) 90135-0 .
25. Buldas, Ahto; Lenin, Aleksandr; Willemson, Jan; Charnamord, Anton (2017). Obana, Satoshi; Chida, Koji (eds.). "Certificados de inviabilidad simple para árboles de ataque". Avances en Información y Seguridad Informática . Apuntes de conferencias en Ciencias de la Computación. Springer International Publishing. 10418 : 39–55. doi : 10.1007 / 978-3-319-64200-0_3 . ISBN 9783319642000.
26. Gi-Joon Nam; Sakallah, KA; Rutenbar, RA (2002). "Un nuevo enfoque de enrutamiento detallado de FPGA a través de la satisfacibilidad booleana basada en búsquedas" (PDF) . Transacciones IEEE sobre diseño asistido por computadora de circuitos y sistemas integrados . 21 (6): 674. doi : 10.1109 / TCAD.2002.1004311 .
27. Davis, M .; Putnam, H. (1960). "Un procedimiento de cálculo para la teoría de la cuantificación". Revista de la ACM . 7 (3): 201. doi : 10.1145 / 321033.321034 . S2CID 31888376 . 
28. Davis, M .; Logemann, G .; Loveland, D. (1962). "Un programa de máquina para la demostración de teoremas" (PDF) . Comunicaciones de la ACM . 5 (7): 394–397. doi : 10.1145 / 368273.368557 . hdl : 2027 / mdp.39015095248095 . S2CID 15866917 .  
29. Zhang, Lintao; Malik, Sharad (2002), "The Quest for Efficient Boolean Satisfiability Solvers", Verificación asistida por computadora , Springer Berlin Heidelberg, págs. 17–36, doi : 10.1007 / 3-540-45657-0_2 , ISBN 978-3-540-43997-4
30. "Un algoritmo de tiempo exponencial mejorado para k-SAT" , Paturi, Pudlak, Saks, Zani
31. "Algoritmos k-SAT más rápidos usando PPSZ sesgado" , Hansen, Kaplan, Zamir, Zwick
32. Vizel, Y .; Weissenbacher, G .; Malik, S. (2015). "Solucionadores de satisfacción booleana y sus aplicaciones en la comprobación de modelos". Actas del IEEE . 103 (11): 2021-2035. doi : 10.1109 / JPROC.2015.2455034 . S2CID 10190144 . 
33. Moskewicz, MW; Madigan, CF; Zhao, Y .; Zhang, L .; Malik, S. (2001). "Chaff: ingeniería de un solucionador SAT eficiente" (PDF) . Actas de la 38ª conferencia sobre automatización del diseño (DAC) . pag. 530. doi : 10.1145 / 378239.379017 . ISBN  1581132972. S2CID  9292941 .
34. Marques-Silva, JP; Sakallah, KA (1999). "GRASP: un algoritmo de búsqueda para la satisfacibilidad proposicional" (PDF) . Transacciones IEEE en computadoras . 48 (5): 506. doi : 10.1109 / 12.769433 . Archivado desde el original (PDF) el 4 de noviembre de 2016 . Consultado el 28 de agosto de 2015 .
35. http://www.cril.univ-artois.fr/~jabbour/manysat.htm
36. "La página web de los concursos internacionales SAT" . Consultado el 15 de noviembre de 2007 .
37. "Concurso SAT 2016" . baldur.iti.kit.edu . Consultado el 13 de febrero de 2020 .
38. "Concurso SAT 2017" . baldur.iti.kit.edu . Consultado el 13 de febrero de 2020 .
39. "Concurso SAT 2018" . sat2018.forsyte.tuwien.ac.at . Consultado el 13 de febrero de 2020 .
40. Balyo, Tomáš; Sinz, Carsten (2018), "Parallel Satisfiability", Handbook of Parallel Constraint Reasoning , Springer International Publishing, págs. 3–29, doi : 10.1007 / 978-3-319-63516-3_1 , ISBN 978-3-319-63515-6
41. Biere, Armin. "Lingeling, Plingeling, PicoSAT y PrecoSAT en SAT Race 2010" (PDF) . CARRERA SAT 2010 .
42. "solucionador de ppfolio" . www.cril.univ-artois.fr . Consultado el 29 de diciembre de 2019 .
43. "Concurso SAT 2011: pista de 32 núcleos: ranking de solucionadores" . www.cril.univ-artois.fr . Consultado el 13 de febrero de 2020 .
44. Balyo, Tomáš; Sanders, Peter; Sinz, Carsten (2015), "HordeSat: A Massively Parallel Portfolio SAT Solver", Lecture Notes in Computer Science , Springer International Publishing, págs. 156-172, arXiv : 1505.03340 , doi : 10.1007 / 978-3-319-24318- 4_12 , ISBN 978-3-319-24317-7, S2CID  11507540
45. "Concurso SAT 2018" . sat2018.forsyte.tuwien.ac.at . Consultado el 13 de febrero de 2020 .
46. Heule, Marijn JH ; Kullmann, Oliver; Wieringa, Siert; Biere, Armin (2012), "Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads", Hardware y software: Verificación y pruebas , Springer Berlin Heidelberg, págs. 50–65, doi : 10.1007 / 978-3-642-34188- 5_8 , ISBN 978-3-642-34187-8
47. Heule, Marijn JH ; van Maaren, Hans (2009). "Soluciones SAT basadas en anticipaciones" (PDF) . Manual de satisfacción . IOS Press. págs. 155-184. ISBN  978-1-58603-929-5.
48. Heule, Marijn JH ; Kullmann, Oliver; Marek, Victor W. (2016), "Resolver y verificar el problema de las triples pitagóricas booleanas a través del cubo y conquistar", Teoría y aplicaciones de las pruebas de satisfacción - SAT 2016 , Springer International Publishing, págs. 228–245, arXiv : 1605.00723 , doi : 10.1007 / 978-3-319-40970-2_15 , ISBN 978-3-319-40969-6, S2CID  7912943
49. Roli, Andrea (2002), "Criticidad y paralelismo en instancias SAT estructuradas", Principios y práctica de la programación de restricciones - CP 2002 , Lecture Notes in Computer Science, 2470 , Springer Berlin Heidelberg, págs. 714–719, doi : 10.1007 / 3-540-46135-3_51 , ISBN 978-3-540-44120-5
50. Arbeláez, Alejandro; Hamadi, Youssef (2011), "Improving Parallel Local Search for SAT", Lecture Notes in Computer Science , Springer Berlin Heidelberg, págs. 46–60, doi : 10.1007 / 978-3-642-25566-3_4 , ISBN 978-3-642-25565-6

Las referencias están ordenadas por fecha de publicación:

• Michael R. Garey y David S. Johnson (1979). Computadoras e intratabilidad: una guía para la teoría de NP-Completeness . WH Freeman. ISBN 0-7167-1045-5. A9.1: LO1 - LO7, págs. 259 - 260.
• Marques-Silva, J .; Vidrio, T. (1999). "Comprobación de equivalencia combinacional mediante satisfacibilidad y aprendizaje recursivo" (PDF) . Conferencia y exposición de Diseño, Automatización y Prueba en Europa, 1999. Actas (Cat. No. PR00078) (PDF) . pag. 145. doi : 10.1109 / DATE.1999.761110 . ISBN 0-7695-0078-1.
• Clarke, E .; Biere, A .; Raimi, R .; Zhu, Y. (2001). "Comprobación del modelo acotado mediante resolución de satisfacción". Métodos formales en el diseño de sistemas . 19 : 7-34. doi : 10.1023 / A: 1011276507260 . S2CID  2484208 .
• Giunchiglia, E .; Tacchella, A. (2004). Giunchiglia, Enrico; Tacchella, Armando (eds.). Teoría y aplicaciones de las pruebas de satisfacción . Apuntes de conferencias en Ciencias de la Computación. 2919 . doi : 10.1007 / b95238 . ISBN 978-3-540-20851-8. S2CID  31129008 .
• Babic, D .; Bingham, J .; Hu, AJ (2006). "B-Cubing: nuevas posibilidades para la resolución de SAT eficiente" (PDF) . Transacciones IEEE en computadoras . 55 (11): 1315. doi : 10.1109 / TC.2006.175 . S2CID  14819050 .
• Rodríguez, C .; Villagra, M .; Baran, B. (2007). "Algoritmos de equipo asincrónico para la satisfacción booleana" (PDF) . 2007 2º Modelos Bioinspirados de Sistemas de Red, Información y Computación . págs. 66–69. doi : 10.1109 / BIMNICS.2007.4610083 . S2CID  15185219 .
• Carla P. Gomes ; Henry Kautz; Ashish Sabharwal; Bart Selman (2008). "Solucionadores de satisfacción". En Frank Van Harmelen; Vladimir Lifschitz; Bruce Porter (eds.). Manual de representación del conocimiento . Fundamentos de la Inteligencia Artificial. 3 . Elsevier. págs. 89-134. doi : 10.1016 / S1574-6526 (07) 03002-7 . ISBN 978-0-444-52211-5.
• Vizel, Y .; Weissenbacher, G .; Malik, S. (2015). "Solucionadores de satisfacción booleana y sus aplicaciones en la comprobación de modelos". Actas del IEEE . 103 (11): 2021-2035. doi : 10.1109 / JPROC.2015.2455034 . S2CID  10190144 .

Enlaces externos

• Juego SAT : intente resolver usted mismo un problema de satisfacción booleana

Formato de problema de SAT

Un problema de SAT se describe a menudo en el formato DIMACS-CNF : un archivo de entrada en el que cada línea representa una sola disyunción. Por ejemplo, un archivo con las dos líneas

1-5 4 0
-1 5 3 4 0

representa la fórmula "( x ₁ ∨ ¬ x ₅ ∨ x ₄ ) ∧ (¬ x ₁ ∨ x ₅ ∨ x ₃ ∨ x ₄ )".

Otro formato común para esta fórmula es la representación ASCII de 7 bits "(x1 | ~ x5 | x4) & (~ x1 | x5 | x3 | x4)".

• BCSAT es una herramienta que convierte archivos de entrada en formato legible por humanos al formato DIMACS-CNF.

Solucionadores de SAT en línea

• BoolSAT: resuelve fórmulas en formato DIMACS-CNF o en un formato más amigable para los humanos: "ay no bo a". Funciona en un servidor.
• Logictools : proporciona diferentes solucionadores en javascript para aprender, comparar y piratear. Se ejecuta en el navegador.
• minisat-in-your-browser : resuelve fórmulas en el formato DIMACS-CNF. Se ejecuta en el navegador.
• SATRennesPA : resuelve fórmulas escritas de manera fácil de usar. Funciona en un servidor.
• somerby.net/mack/logic : resuelve fórmulas escritas en lógica simbólica. Se ejecuta en el navegador.

Solucionadores de SAT sin conexión

• MiniSAT : formato DIMACS-CNF y formato OPB para su compañero solucionador de restricciones pseudo-booleano MiniSat +
• Lingeling : ganó una medalla de oro en una competencia SAT de 2011.
  • PicoSAT : un solucionador anterior del grupo Lingeling.
• Sat4j : formato DIMACS-CNF. Código fuente de Java disponible.
• Glucosa : formato DIMACS-CNF.
• RSat : ganó una medalla de oro en una competencia SAT de 2007.
• UBCSAT . Admite cláusulas ponderadas y no ponderadas, tanto en formato DIMACS-CNF. Código fuente C alojado en GitHub .
• CryptoMiniSat : ganó una medalla de oro en una competencia SAT de 2011. Código fuente C ++ alojado en GitHub . Intenta poner muchas características útiles del núcleo MiniSat 2.0, PrecoSat ver 236 y Glucose en un solo paquete, agregando muchas características nuevas
• Spear : admite aritmética de vectores de bits. Puede utilizar el formato DIMACS-CNF o el formato Spear .
  • HyperSAT : escrito para experimentar con la poda de espacio de búsqueda de cubos B. Ganó el 3er lugar en una competencia SAT de 2005. Un solucionador anterior y más lento de los desarrolladores de Spear.
• BASolver
• ArgoSAT
• Fast SAT Solver : basado en algoritmos genéticos .
• zChaff : ya no es compatible.
• BCSAT : formato de circuito booleano legible por humanos (también convierte este formato al formato DIMACS-CNF y se vincula automáticamente a MiniSAT o zChaff).
• gini : solucionador de idiomas SAT Go con herramientas relacionadas.
• gophersat : solucionador de SAT de lenguaje Go que también puede lidiar con problemas pseudo-booleanos y MAXSAT.
• CLP (B) - Programación lógica de restricción booleana, por ejemplo SWI-Prolog .

Aplicaciones SAT

• WinSAT v2.04 : una aplicación SAT basada en Windows diseñada especialmente para investigadores.

Conferencias

• Conferencia internacional sobre teoría y aplicaciones de las pruebas de satisfacción

Publicaciones

• Revista sobre satisfacción, modelado booleano y computación
• Propagación de encuestas

Puntos de referencia

• Puntos de referencia SAT satisfactorios forzados
• Puntos de referencia de verificación de software
• Benchmarks de Fadi Aloul SAT

Resolución de SAT en general:

• http://www.satlive.org
• http://www.satisfiability.org

Evaluación de solucionadores de SAT

• Evaluación anual de solucionadores de SAT
• Resultados de la evaluación de SAT Solvers para 2008
• Competiciones Internacionales SAT
• Historia

Más información sobre SAT:

• SAT y MAX-SAT para el investigador no profesional
• SAT / SMT por ejemplo

---

Este artículo incluye material de una columna en el boletín electrónico ACM SIGDA del Prof. Karem Sakallah
El texto original está disponible aquí