Problema de satisfacibilidad booleano - Boolean satisfiability problem

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 SAT heurísticos pueden resolver casos de problemas que involucran decenas de miles de variables y fórmulas que constan de millones de símbolos, lo cual es suficiente para muchos problemas SAT prácticos de, por ejemplo, inteligencia artificial , diseño de circuitos y sistemas automáticos. demostración del teorema .

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 Y ( 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 , incluida la informática teórica , la teoría de la complejidad , la algorítmica , la criptografía y la inteligencia artificial .

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, es insatisfactorio, 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 alguna función booleana R y literales (ordinarios) l _i . Diferentes conjuntos de funciones booleanas permitidas 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 cláusula generalizada. forma normal conjuntiva. 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 de NP completo conocido , como lo demostró Stephen Cook en la Universidad de Toronto en 1971 e independientemente por Leonid Levin en la Academia Nacional de Ciencias en 1973. Hasta ese momento, el concepto de un problema de NP completo no era suficiente. incluso existir. La prueba muestra cómo cada problema de decisión en la clase de complejidad NP puede reducirse al problema SAT para fórmulas CNF, 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 la 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.

Como 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 transformar 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.

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 . Esto se hace mediante la reducción del tiempo polinómico 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 de cláusulas diferentes, cf. fotografía. La gráfica tiene un c -clique si y solo si la fórmula es satisfactoria.

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.

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

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 .

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. 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 . 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 para garantizar que solo d ₁ = ⋯ = d _k = FALSE pueda 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 si se permiten literales duplicados en las cláusulas, como en ¬ x ∨ ¬ y ∨ ¬ y .

Exactamente-1 3-satisfacibilidad

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. Derecha: 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 uno en tres 3-SAT se da como una forma normal conjuntiva generalizada con todas las cláusulas generalizadas usando un operador ternario R que 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, se enumera como problema NP-completo "LO4" en la referencia estándar, Computadoras e intratabilidad: una guía para la teoría de NP-Completeness 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.

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 satisfactoria por alguna configuración 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. Otra reducción involucra solo cuatro variables nuevas y tres cláusulas: R (¬ x , a , b ) ∧ R ( b , y , c ) ∧ R ( c , d , ¬ z ), ver imagen (derecha).

No todos iguales 3-satisfacibilidad

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.

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.

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 veracidad de las fórmulas de Horn cuantificadas en tiempo polinomial.

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 ₁ introduciendo y ₃ 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

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). 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 ; vea el cuadro 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 VERDADEROS, cada solución del problema 1-en-3-SAT para una fórmula CNF dada también es 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. fotografía. 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 las funciones booleanas que puedan usarse 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.

La siguiente tabla resume algunas variantes comunes de SAT.

Extensiones de SAT

Una extensión que ha ganado popularidad significativa desde 2003 es teorías de satisfacibilidad módulo ( SMT ) que puede enriquecer fórmulas CNF con restricciones lineales, matrices, todo diferentes limitaciones, funciones no interpretados , etc. Tales extensiones típicamente permanecen NP-completa, pero solucionadores muy eficientes son ahora disponible que puede 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 y son FALSOS, y z = FALSO en caso contrario. 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.

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 es 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 es el problema de determinar si una fórmula tiene exactamente una asignación. Está completo para EE . UU. , 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 . 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 que si existe un algoritmo práctico (es decir, polinomio-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 polinomial (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).

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 ₁ = 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, donde n 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 = Σ ₂   ( 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 instancias de problemas que involucran decenas de miles de variables y millones de restricciones (es decir, cláusulas). Ejemplos de tales problemas en automatización de diseño electrónico (EDA) incluyen la comprobación formal de equivalencia , la verificación de modelos , la verificación formal de microprocesadores pipeline , generación automática patrón de prueba , de enrutamiento de FPGAs , planificación , y problemas de programación , 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 denomina comúnmente algoritmo Davis-Putnam-Logemann-Loveland ("DPLL" o "DLL"). 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. En teoría, se han demostrado límites inferiores exponenciales para la familia de algoritmos DPLL.

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.

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 de 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 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. ${\ Displaystyle O (1.308 ^ {n})}$${\ Displaystyle O (1.307 ^ {n})}$

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. Solucionadores de conflictos impulsado, como el conflicto impulsado por la cláusula de aprendizaje (CDCl), aumentan 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 "dos-literales-visto" unidad propagación , 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). Las implementaciones bien conocidas incluyen Chaff y GRASP . Los solucionadores de anticipación han fortalecido especialmente las reducciones (que van más allá de la propagación de cláusulas unitarias) y las heurísticas, 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 tienen un 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. 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 se destacan por demostrar insatisfacción y otros por encontrar soluciones. Todos estos comportamientos se pueden ver en los concursos de resolución de SAT.

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, 2017 y 2018, los puntos de referencia se ejecutaron en un sistema de memoria compartida con 24 núcleos de procesamiento , por lo que 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. La diversificación de las carteras mediante la inclusión de una variedad de solucionadores, cada uno con un buen desempeño en un conjunto diferente de problemas, aumenta la solidez del solucionador.

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.

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 el simple hecho de 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. 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 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 SAT Solver . Ejemplos notables de tales solucionadores incluyen Plingeling y painless-mcomsps.

Divide y conquistaras

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 .

Fase de cubo para la fórmula . 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.${\ Displaystyle F}$

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 . 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 equivalente a 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, por lo que se usa 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 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.

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 .

Busqueda local

Una estrategia hacia un algoritmo de búsqueda local paralelo para la resolución de SAT es probar múltiples cambios de variable al mismo tiempo en diferentes unidades de procesamiento. 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.

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

Referencias

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

enlaces externos

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

Formato de problema 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 del 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 - Go language SAT solver 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

Benchmarks

• Puntos de referencia SAT satisfactorios forzados
• Benchmarks 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 por el Prof. Karem Sakallah
El texto original está disponible aquí