Hispanopedia Wiki
Articulo de referencia

Problema de satisfacibilidad booleana

En lógica e informática , el problema de satisfacibilidad booleana (a veces llamado problema de satisfacibilidad proposicional y abreviado como SATISFACCIÓN , SAT o B-SAT ) preg...

Hispanopedia WikiContenido en espanolLectura gratuita

En lógica e informática , el problema de satisfacibilidad booleana (a veces llamado problema de satisfacibilidad proposicional y abreviado como SATISFACCIÓN , SAT o B-SAT ) pregunta si existe una interpretación que satisfaga una fórmula booleana dada . En otras palabras, pregunta si las variables de la fórmula pueden reemplazarse consistentemente por los valores VERDADERO o FALSO para que la fórmula se evalúe como VERDADERO. Si esto sucede, la fórmula se llama satisfacible; de ​​lo contrario, insatisfacible . Por ejemplo, la fórmula " a AND NOT b " es satisfacible porque se pueden encontrar los valores a = VERDADERO y b = FALSO, que hacen que ( a AND NOT b ) = VERDADERO. En cambio, " a AND NOT a " es insatisfacible.

SAT es el primer problema que se demostró que es NP-completo —este es 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, como máximo, tan difíciles de resolver como SAT. No se conoce ningún algoritmo que resuelva eficientemente cada problema SAT (donde "eficientemente" significa "de forma determinista en tiempo polinomial "). Aunque generalmente se cree que tal algoritmo no existe, esta creencia no se ha probado ni refutado matemáticamente. Resolver la cuestión de si SAT tiene un algoritmo de tiempo polinomial resolvería el problema P versus NP , uno de los problemas abiertos más importantes en la teoría de la computación. [ 1 ] [ 2 ]

Sin embargo, los algoritmos SAT heurísticos son capaces de resolver instancias de problemas que involucran decenas de miles de variables y fórmulas que constan de millones de símbolos, [ 3 ] lo cual es suficiente para muchos problemas SAT prácticos que ocurren en inteligencia artificial , diseño de circuitos , [ 4 ] y demostración automática de teoremas .

Definiciones

Una fórmula de 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 satisfacible si puede hacerse VERDADERA asignando valores lógicos apropiados (es decir, VERDADERO, FALSO) a sus variables. El problema de satisfacibilidad booleana (SAT) consiste en comprobar, dada una fórmula, si es satisfacible. Este problema de decisión es de vital importancia en muchas áreas de la informática , incluyendo la informática teórica , la teoría de la complejidad , [ 5 ] [ 6 ] la algoritmia , la criptografía [ 7 ] [ 8 ] y la inteligencia artificial . [ 9 ]

forma normal conjuntiva

Un literal es una variable (en cuyo caso se denomina literal positivo ) o la negación de una variable (denominada literal negativo ). Una cláusula es una disyunción de literales (o un solo literal). Una cláusula se denomina cláusula de Horn si contiene como máximo un literal positivo. Una fórmula está en forma normal conjuntiva (FNC) si es una conjunción de cláusulas (o una sola cláusula).

Por ejemplo, x 1 es un literal positivo, ¬ x 2 es un literal negativo y x 1 ∨ ¬ x 2 es una cláusula. La fórmula ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1 está en forma conjuntiva normal; su primera y tercera cláusulas son cláusulas de Horn, pero su segunda cláusula no lo es. La fórmula es satisfacible, eligiendo x 1  =  FALSO, x 2  =  FALSO y x 3 arbitrariamente, ya que (FALSO ∨ ¬FALSO) ∧ (¬FALSO ∨ FALSO ∨ x 3 ) ∧ ¬FALSO se evalúa como (FALSO ∨ VERDADERO) ∧ (VERDADERO ∨ FALSO ∨ x 3 ) ∧ VERDADERO, y a su vez como VERDADERO ∧ VERDADERO ∧ VERDADERO (es decir, VERDADERO). En cambio, la fórmula CNF a ∧ ¬ a , que consta de dos cláusulas de un literal, es insatisfacible, ya que para a = VERDADERO o a = FALSO se evalúa como VERDADERO ∧ ¬VERDADERO (es decir, FALSO) o FALSO ∧ ¬FALSO (es decir, de nuevo FALSO), respectivamente.

Para algunas versiones del problema SAT, es útil definir la noción de una fórmula de forma normal conjuntiva generalizada , es decir, como una conjunción de un número arbitrario de cláusulas generalizadas , siendo estas últimas de la forma R ( l 1 ,..., l n ) para alguna función booleana R y literales (ordinarios) l i . Diferentes conjuntos de funciones booleanas permitidas conducen a diferentes versiones del problema. Como 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 utiliza a continuación , donde R es el operador ternario que es VERDADERO solo cuando exactamente uno de sus argumentos lo es.

Utilizando las leyes del álgebra booleana , toda fórmula de lógica proposicional puede transformarse en una forma normal conjuntiva equivalente, que, sin embargo, puede ser exponencialmente más larga. Por ejemplo, al transformar la fórmula ( x 1 ∧ y 1 ) ∨ ( x 2 ∧ y 2 ) ∨ ... ∨ ( x n ∧ y n ) en forma normal conjuntiva se obtiene:

( x 1  ∨ x 2 ∨ … ∨ x n ) ∧     
( y 1  ∨ x 2 ∨ … ∨ x n ) ∧     
( x 1  ∨ y 2 ∨ … ∨ x n ) ∧     
( y 1  ∨ y 2 ∨ … ∨ x norte ) ∧ ... ∧     
( x 1  ∨ x 2 ∨ … ∨ y n ) ∧     
( y 1  ∨ x 2 ∨ … ∨ y norte ) ∧     
( x 1  ∨ y 2 ∨ … ∨ y norte ) ∧     
( y 1  ∨ y 2 ∨ … ∨ y norte )      ;

Mientras que la primera es una disyunción de n conjunciones de 2 variables, la segunda consta de 2 n cláusulas de n variables.

Sin embargo, mediante el uso de la transformación de Tseytin , podemos encontrar una fórmula de forma normal conjuntiva equisatisfacible con una longitud lineal en el tamaño de la fórmula lógica proposicional original.

Complejidad

SAT fue el primer problema conocido como NP-completo , como lo demostró Stephen Cook en la Universidad de Toronto en 1971 [ 10 ] e independientemente Leonid Levin en la Academia Rusa de Ciencias en 1973. [ 11 ] Hasta ese momento, el concepto de un problema NP-completo ni siquiera existía. La demostración muestra cómo todo problema de decisión en la clase de complejidad NP puede reducirse al problema SAT para fórmulas CNF [ a ] , a veces llamado CNFSAT . Una propiedad útil de la reducción de Cook es que preserva el número de respuestas aceptables. Por ejemplo, decidir si un grafo dado tiene una 3-coloración es otro problema en NP; si un grafo tiene 17 3-coloraciones válidas, entonces la fórmula SAT producida por la reducción de Cook-Levin tendrá 17 asignaciones satisfactorias.

La NP-completitud solo se refiere al tiempo de ejecución de los casos más desfavorables. Muchos de los casos que se presentan en aplicaciones prácticas se pueden resolver mucho más rápidamente. Véase la sección «Algoritmos para resolver SAT» más abajo.

3-satisfacibilidad

La instancia 3-SAT ( x ∨ x ∨ y ) ∧ (¬ x ∨ ¬ y ∨ ¬ y ) ∧ (¬ x ∨ y ∨ y ) se reduce a un problema de clique . Los vértices verdes forman un 3-clique y corresponden a la asignación que satisface 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 SAT no restringido a 3-SAT, transforme cada cláusula l 1 ∨ ⋯ ∨ l n en una conjunción de n - 2 cláusulas.

( l 1 ∨ l 2 ∨ x 2 ) ∧
(¬ x 2 ∨ l 3 ∨ x 3 ) ∧
(¬ x 3 ∨ l 4 ∨ x 4 ) ∧ ⋯ ∧
(¬ x n −3 ∨ l n −2 ∨ x n −2 ) ∧
(¬ x n −2 ∨ l n −1 ∨ l n )

donde x 2 , ⋯ , x n −2 son variables nuevas que no aparecen en ningún otro lugar. Aunque las dos fórmulas no son lógicamente equivalentes , son equisatisfacibles . La fórmula resultante de transformar todas las cláusulas es como máximo 3 veces más larga que la original; es decir, el crecimiento de la longitud es polinomial. [ 12 ]

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 . [ b ] Esto se hace mediante la reducción en tiempo polinomial de 3-SAT al otro problema. Un ejemplo de un problema donde se ha utilizado este método es el problema de la clique : dada una fórmula CNF que consta de c cláusulas, el grafo correspondiente consta de un vértice para cada literal y una arista entre cada dos literales no contradictorios [ c ] de diferentes cláusulas; véase la imagen. El grafo tiene una c -clique si y solo si la fórmula es satisfacible. [ 13 ]

Existe un algoritmo aleatorio simple debido a Schöning (1999) que se ejecuta en tiempo (4/3) n 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. [ 14 ]

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

Selman, Mitchell y Levesque (1996) proporcionan datos empíricos sobre la dificultad de fórmulas 3-SAT generadas aleatoriamente, en función de sus parámetros de tamaño. La dificultad se mide en el número de llamadas recursivas realizadas por un algoritmo DPLL . Identificaron una región de transición de fase desde fórmulas casi seguramente satisfacibles a fórmulas casi seguramente insatisfacibles en una relación cláusulas-variables de aproximadamente 4,26. [ 15 ]

La 3-satisfacibilidad puede generalizarse a k- satisfacibilidad ( k -SAT , también k -CNF-SAT ), cuando se consideran fórmulas en CNF con cada cláusula conteniendo hasta k literales. [ 16 ] Sin embargo, dado que para cualquier k ≥ 3 , este problema no puede ser ni más fácil que 3-SAT ni más difícil que SAT, y estos 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 con menos de k literales puede rellenarse con copias repetidas de los mismos literales. [ 17 ]

Se ha investigado estadísticamente la satisfacibilidad y la geometría del espacio de soluciones de problemas k -SAT con cláusulas generadas aleatoriamente. En función de la relación cláusula-variable (también conocida como densidad), el modelo presenta diversas transiciones de fase con respecto a la satisfacibilidad y la geometría del espacio de soluciones. Para la satisfacibilidad, existe un umbral bien definido, de modo que con alta probabilidad existe una solución si y solo si la densidad se mantiene por debajo de este umbral. [ 18 ] Muy por debajo del umbral de satisfacibilidad, el espacio de soluciones también experimenta una transición de fase geométrica, es decir, se fragmenta en un número exponencial de clústeres bien separados. El inicio de esta transición de fase coincide con el umbral algorítmico conocido, lo que sugiere una relación entre la geometría y la intratabilidad algorítmica. [ 19 ] [ 20 ]

Casos especiales de 3SAT

forma normal conjuntiva

La forma normal conjuntiva (en particular, con 3 literales por cláusula) se considera a menudo la representación canónica para las fórmulas SAT. Como se muestra arriba, el problema general de SAT se reduce a 3-SAT, el problema de determinar la satisfacibilidad para fórmulas en esta forma.

SAT lineal

Una fórmula 3-SAT es SAT lineal ( LSAT ) si cada cláusula (considerada como un conjunto de literales) interseca como máximo una cláusula más y, además, si dos cláusulas intersecan, entonces tienen exactamente un literal en común. Una fórmula LSAT puede representarse como un conjunto de intervalos semicerrados disjuntos en una línea. Decidir si una fórmula LSAT es satisfacible es un problema NP-completo. [ 21 ]

2-satisfacibilidad

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

Satisfacción con el cuerno

El problema de determinar la satisfacibilidad de una conjunción dada de cláusulas de Horn se denomina satisfacibilidad de Horn , o HORN-SAT . Puede resolverse en tiempo polinomial mediante un único paso del algoritmo de propagación unitaria , que produce el único modelo mínimo del conjunto de cláusulas de Horn (con respecto al conjunto de literales asignados a VERDADERO). La satisfacibilidad de Horn es P-completa . Puede considerarse como la versión P del problema de satisfacibilidad booleana. Asimismo, determinar la veracidad de fórmulas de Horn cuantificadas puede hacerse en tiempo polinomial. [ 22 ]

Las cláusulas de Horn son interesantes porque permiten expresar la implicación de una variable a partir de un conjunto de otras variables. De hecho, una de estas cláusulas, ¬ x 1 ∨ ... ∨ ¬ x n ∨ y, puede reescribirse como x 1 ∧ ... ∧ x n → y ; es decir, si x 1 ,..., x n son todas VERDADERAS, entonces y también debe ser VERDADERA.

Una generalización de la clase de fórmulas de Horn es la de fórmulas de Horn renombrables, que es el conjunto de fórmulas que se pueden poner en forma de Horn reemplazando algunas variables con su respectiva negación. Por ejemplo, ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1 no es una fórmula de Horn, pero se puede renombrar a la fórmula de Horn ( x 1 ∨ ¬ x 2 ) ∧ (¬ x 1 ∨ x 2 ∨ ¬ y 3 ) ∧ ¬ x 1 introduciendo y 3 como negación de x 3 . Por el contrario, ningún cambio de nombre de ( x 1 ∨ ¬ x 2 ∨ ¬ x 3 ) ∧ (¬ x 1 ∨ x 2 ∨ x 3 ) ∧ ¬ x 1 conduce a una fórmula de Horn. La comprobación de la existencia de tal sustitución puede realizarse en tiempo lineal; por lo tanto, la satisfacibilidad de tales fórmulas pertenece a P, ya que puede resolverse realizando primero esta sustitución y luego comprobando la satisfacibilidad de la fórmula de Horn resultante.

No son problemas del 3SAT

Forma normal disyuntiva

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

Exactamente-1 3-satisfacibilidad

Otra variante NP-completa del problema de 3-satisfacibilidad es el 3-SAT de uno en tres (también conocido como 1-SAT de tres y exactamente 1 3-SAT ). Dada una forma normal conjuntiva con tres literales por cláusula, el problema consiste en determinar si existe una asignación de verdad a las variables tal que cada cláusula tenga exactamente un literal VERDADERO (y, por lo tanto, exactamente dos literales FALSOS).

Satisfacibilidad 3 no todas iguales

Otra variante es el problema de 3-satisfacibilidad no todos iguales (también llamado NAE3SAT ). Dada una forma normal conjuntiva con tres literales por cláusula, el problema consiste en determinar si existe una asignación a las variables tal 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. [ 23 ]

Satisfacibilidad XOR

Otro caso especial es la clase de problemas donde cada cláusula contiene XOR (es decir, OR exclusivo ) en lugar de operadores OR (simples). Esto pertenece a P , ya que una fórmula XOR-SAT también puede verse como un sistema de ecuaciones lineales módulo 2 y puede resolverse en tiempo cúbico mediante eliminación gaussiana . [ 24 ]

Teorema de la dicotomía de Schaefer

Las restricciones anteriores (CNF, 2CNF, 3CNF, Horn, XOR-SAT) obligan a que las fórmulas consideradas sean 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 se pueden usar para formar estas subfórmulas, el problema de satisfacibilidad correspondiente pertenece a P o es NP-completo. La pertenencia a P de la satisfacibilidad de las fórmulas 2CNF, Horn y XOR-SAT son casos especiales de este teorema. [ 23 ]

La siguiente tabla resume algunas variantes comunes del SAT.

Extensiones del SAT

Una extensión que ha ganado gran popularidad desde 2003 es la satisfacibilidad módulo teorías ( SMT ), que puede enriquecer las fórmulas CNF con restricciones lineales, matrices, restricciones totalmente diferentes, funciones no interpretadas , [ 25 ] etc. Estas extensiones suelen seguir siendo NP-completas, pero ahora existen solucionadores muy eficientes que pueden manejar muchos tipos de restricciones.

El problema de satisfacibilidad se vuelve más difícil si se permiten cuantificadores "para todo" ( ∀ ) y "existe" ( ∃ ) para vincular 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 e y , se puede encontrar un valor apropiado de z , a saber, z = VERDADERO si tanto x como y son FALSO, y z = FALSO en caso contrario. SAT en sí mismo (tácitamente) usa solo cuantificadores ∃. Si en cambio solo se permiten cuantificadores ∀, se obtiene el llamado problema de tautología , que es co-NP-completo . Si se permite cualquier número de 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 PSPACE-completos son estrictamente más difíciles que cualquier problema en NP, aunque esto aún no se ha demostrado.

La prueba SAT ordinaria pregunta si existe al menos una asignación de variable que haga que la fórmula sea verdadera. Diversas variantes abordan el número de dichas asignaciones:

  • MAJ-SAT pregunta si al menos la mitad de todas las asignaciones hacen que la fórmula sea VERDADERA. Se sabe que es completa para PP , una clase probabilística. Sorprendentemente, se demuestra que MAJ-kSAT está en P para todo entero finito k. [ 26 ]
  • #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 [ 27 ] es el problema de determinar si una fórmula tiene exactamente una asignación. Es completo para US , [ 28 ] la clase de complejidad que describe problemas resolubles por una máquina de Turing no determinista de tiempo polinomial que acepta cuando hay exactamente una ruta de aceptación no determinista y rechaza en caso contrario.
  • UNAMBIGUOUS-SAT es el nombre que se le da al problema de satisfacibilidad cuando se promete que la fórmula de entrada tendrá como máximo una asignación satisfactoria. El problema también se llama USAT . [ 29 ] Un algoritmo de resolución para UNAMBIGUOUS-SAT puede exhibir cualquier comportamiento, incluyendo bucles infinitos, en una fórmula con varias asignaciones satisfactorias. Aunque este problema parece más fácil, Valiant y Vazirani han demostrado [ 30 ] que si existe un algoritmo práctico (es decir, aleatorio de tiempo polinomial ) 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. Requiere determinar el número máximo de cláusulas que pueden ser satisfechas por cualquier asignación. Cuenta con algoritmos de aproximación eficientes , pero su solución exacta es NP-difícil. Peor aún, es APX -completo, lo que significa que no existe un esquema de aproximación en 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 negación). Los pesos de las variables proposicionales se proporcionan como entrada del problema. El peso de una asignación es la suma de los pesos de las variables verdaderas. Este problema es NP-completo (véase el Teorema 1 de [ 31 ] ).

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

Encontrar una tarea satisfactoria

Si bien SAT es un problema de decisión , el problema de búsqueda de una asignación satisfactoria se reduce a SAT. Es decir, cada algoritmo que responde correctamente si una instancia de SAT es resoluble puede usarse para encontrar una asignación satisfactoria. Primero, se pregunta sobre la fórmula dada Φ. Si la respuesta es "no", la fórmula es insatisfacible. De lo contrario, se pregunta sobre la fórmula parcialmente instanciada Φ { x 1 =VERDADERO} , es decir, Φ con la primera variable x 1 reemplazada por VERDADERO, y simplificada en consecuencia. Si la respuesta es "sí", entonces x 1 =VERDADERO, de lo contrario x 1 =FALSO. Los valores de las demás variables pueden encontrarse 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 se utiliza en varios teoremas de la teoría de la complejidad:

Algoritmos para resolver SAT

Complejidad exponencial de la resolución de problemas SAT frente al número de variables, el número de cláusulas y la longitud de la fórmula.

Dado que el problema SAT es NP-completo, solo se conocen algoritmos con complejidad exponencial en el peor de los casos. A pesar de esto, durante la década de 2000 se desarrollaron algoritmos eficientes y escalables para SAT que contribuyeron a avances drásticos en la capacidad de resolver automáticamente instancias de problemas que involucran decenas de miles de variables y millones de restricciones (es decir, cláusulas). [ 3 ] Ejemplos de tales problemas en la automatización del diseño electrónico (EDA) incluyen la verificación de equivalencia formal , la verificación de modelos , la verificación formal de microprocesadores segmentados , [ 25 ] la generación automática de patrones de prueba , el enrutamiento de FPGA , [ 32 ] la planificación y los problemas de programación , etc. Un motor de resolución SAT también se considera un componente esencial en el conjunto de herramientas de automatización del diseño electrónico .

Las principales técnicas utilizadas por los solucionadores SAT modernos incluyen el algoritmo Davis-Putnam-Logemann-Loveland (o DPLL), el aprendizaje de cláusulas basado en conflictos (CDCL) y algoritmos de búsqueda local estocástica como WalkSAT . Casi todos los solucionadores SAT incluyen tiempos de espera, por lo que terminarán en un tiempo razonable incluso si no pueden encontrar una solución. Diferentes solucionadores SAT encontrarán diferentes instancias fáciles o difíciles, y algunos sobresalen en demostrar la insatisfacibilidad, y otros en encontrar soluciones. Recientemente se han realizado intentos para aprender la satisfacibilidad de una instancia utilizando técnicas de aprendizaje profundo . [ 33 ]

Los solucionadores SAT se desarrollan y comparan en concursos de resolución SAT. [ 34 ] Los solucionadores SAT modernos también están teniendo un impacto significativo en los campos de la verificación de software, la resolución de restricciones en inteligencia artificial y la investigación operativa , entre otros.

En las últimas décadas se han presentado algoritmos teóricos con garantías de tiempo de ejecución en el peor de los casos cada vez mejores, incluyendo unO∗(1.0638L){\displaystyle O^{*}(1,0638^{L})}algoritmo para conjuntos de cláusulas de longitud (recuento total de literales)L{\displaystyle L}, [ 35 ] [ 36 ] unO∗(1.2226metro){\displaystyle O^{*}(1,2226^{m})}algoritmo para conjuntos demetro{\displaystyle m}cláusulas, [ 37 ] [ 38 ] y unaO∗(1.32793norte){\displaystyle O^{*}(1,32793^{n})}algoritmo para 3-SAT connorte{\displaystyle n}variables. [ 39 ] Aquí, la notación "O∗(.){\displaystyle O^{*}(.)}" significa "hasta un factor polinómico", es decirO∗(F(norte))=O(F(norte)norteO(1)){\displaystyle O^{*}(f(n))=O(f(n)n^{O(1)})}En el diagrama se muestran las garantías de tiempo de ejecución anteriores.

Véase también

Notas

  1. ↑ El problema SAT para fórmulas arbitrarias también es NP-completo, ya que se demuestra 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, de tal manera que un literal no sea la negación del otro.
  • Juego SAT : intenta resolver tú mismo un problema de satisfacibilidad booleana.
  • El sitio web de la competencia internacional SAT
  • Conferencia Internacional sobre Teoría y Aplicaciones de las Pruebas de Satisfacibilidad
  • Revista sobre Satisfacibilidad, Modelado Booleano y Computación
  • SAT Live, un sitio web que recopila información para la investigación sobre el problema de la satisfacibilidad.
  • Evaluación anual de los solucionadores MaxSAT

Referencias

  1. ↑ Fortnow, L. (2009). "El estado del problema P versus NP" (PDF) . Communications of the ACM . 52 (9): 78– 86. doi : 10.1145/1562164.1562186 . S2CID 5969255 . 
  2. ↑ Fortnow, L. (2021). "Cincuenta años de P versus NP y la posibilidad de lo imposible" (PDF) . Actas de la Conferencia ACM (Conference'17) .
  3. 1 2 Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael (2007), "Propagación = Generación perezosa de cláusulas", Principios y práctica de la programación con restricciones – CP 2007 , Lecture Notes in Computer Science, vol. 4741, pp. 544–558 , CiteSeerX 10.1.1.70.5471 , doi : 10.1007/978-3-540-74970-7_39 , ISBN    978-3-540-74969-1Los solucionadores SAT modernos a menudo pueden manejar problemas con millones de restricciones y cientos de miles de variables..
  4. ↑ 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 post-silicio eficaz". Conferencia Internacional de Pruebas IEEE 2010. págs. 1–10 . doi : 10.1109/TEST.2010.5699215 . ISBN  978-1-4244-7206-2. S2CID 7909084 . 
  5. ↑ 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: Plenum. pp. 85–103 . ISBN  0-306-30707-3Archivado del original (PDF) el 29/06/2011 . Consultado el 07/05/2020 .Aquí: pág. 86
  6. ↑ Aho, Alfred V.; Hopcroft, John E.; Ullman, Jeffrey D. (1974). El diseño y análisis de algoritmos informáticos . Addison-Wesley. pág. 403. ISBN  0-201-00029-6.
  7. ↑ Massacci, Fabio; Marraro, Laura (2000-02-01). "Criptoanálisis lógico como problema SAT". Journal of Automated Reasoning . 24 (1): 165– 203. doi : 10.1023/A:1006326723002 . S2CID 3114247 . 
  8. ↑ Mironov, Ilya; Zhang, Lintao (2006). "Aplicaciones de solucionadores SAT al criptoanálisis de funciones hash" . En Biere, Armin; Gomes, Carla P. (eds.). Teoría y aplicaciones de las pruebas de satisfacibilidad - SAT 2006. Lecture Notes in Computer Science. Vol. 4121. Springer. pp. 102–115 . doi : 10.1007/11814948_13 . ISBN   978-3-540-37207-3.
  9. ↑ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Solucionadores de satisfacibilidad booleana y sus aplicaciones en la verificación de modelos". Actas del IEEE . 103 (11): 2021– 2035. doi : 10.1109/JPROC.2015.2455034 . S2CID 10190144 . 
  10. ↑ Cook, Stephen A. (1971). "La complejidad de los procedimientos de demostración de teoremas" (PDF) . Actas del tercer simposio anual de la ACM sobre Teoría de la Computación - STOC '71 . págs. 151–158 . CiteSeerX 10.1.1.406.395 . doi : 10.1145/800157.805047 . S2CID 7573663. Archivado (PDF) del original el 9 de octubre de 2022 .   
  11. ^ 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). "Un estudio de los enfoques rusos de los algoritmos perebor (búsquedas por fuerza bruta)". Anales de la historia de la computación . 6 (4): 384– 400. Bibcode : 1984IAHC....6d.384T . doi : 10.1109/MAHC.1984.10036 . S2CID 950581 . 
  12. ↑ Aho, Hopcroft y Ullman (1974) , Teorema 10.4.
  13. ↑ Aho, Hopcroft y Ullman (1974) , Teorema 10.5.
  14. ↑ Schöning, Uwe (octubre de 1999). «Un algoritmo probabilístico para problemas k-SAT y de satisfacción de restricciones» (PDF) . 40.º Simposio Anual sobre Fundamentos de la Informática (Cat. n.º 99CB37039) . págs. 410-414 . doi : 10.1109/SFFCS.1999.814612 . ISBN  0-7695-0409-4. S2CID 123177576 . Archivado (PDF) del original el 09-10-2022. 
  15. ↑ Selman, Bart; Mitchell, David; Levesque, Hector (1996). "Generación de problemas de satisfacibilidad difíciles". Inteligencia artificial . 81 ( 1–2 ): 17–29 . CiteSeerX 10.1.1.37.7362 . doi : 10.1016/0004-3702(95)00045-3 . 
  16. ^ Vazirani, Vijay V. (2001). Algoritmos de aproximación . Berlín: Springer-Verlag. pag. 343.ISBN​  3-540-65367-8. MR 1851303 . 
  17. ↑ Papadimitriou, Christos H. (1994). Complejidad computacional . Reading, Massachusetts: Addison-Wesley Publishing Company. pág. 183. ISBN  0-201-53082-1. MR 1251285 . 
  18. ↑ Ding, Jian; Sly, Allan; Sun, Nike (2022). "Demostración de la conjetura de satisfacibilidad para k grande " . Annals of Mathematics . Segunda serie. 196 (1): 1– 388. doi : 10.4007/annals.2022.196.1.1 .
  19. ↑ Krzakała, Florent; Montanari, Andrea; Ricci-Tersenghi, Federico; Semerjian, Guilhem; Zdeborová, Lenka (2007-06-19). "Estados de Gibbs y el conjunto de soluciones de problemas de satisfacción de restricciones aleatorias". Actas de la Academia Nacional de Ciencias . 104 (25): 10318– 10323. doi : 10.1073/pnas.0703685104 .
  20. ↑ Achlioptas, Dimitris; Coja-Oghlan, Amin (2008). "Barreras algorítmicas a partir de transiciones de fase". 49.º Simposio Anual IEEE sobre Fundamentos de la Informática, FOCS 2008, Filadelfia, PA, EE. UU., 25-28 de octubre de 2008. IEEE Computer Society. págs. 793-802 . arXiv : 0803.2122 . doi : 10.1109/FOCS.2008.11 . 
  21. ↑ Arkin, Esther M.; Banik, Aritra; Carmi, Paz; Citovsky, Gui; Katz, Matthew J.; Mitchell, Joseph SB; Simakov, Marina (11 de diciembre de 2018). "Selección y recubrimiento de puntos coloreados" . Matemáticas Aplicadas Discretas . 250 : 75–86 . doi : 10.1016/j.dam.2018.05.011 . ISSN 0166-218X . 
  22. ↑ Buning, HK; Karpinski, Marek; Flogel, A. (1995). "Resolución para fórmulas booleanas cuantificadas" . Information and Computation . 117 (1). Elsevier: 12–18 . doi : 10.1006/inco.1995.1025 .
  23. 1 2 Schaefer, Thomas J. (1978). "La complejidad de los problemas de satisfacibilidad" (PDF) . Actas del 10.º Simposio Anual de la ACM sobre Teoría de la Computación . San Diego, California. págs. 216–226 . CiteSeerX 10.1.1.393.8951 . doi : 10.1145/800133.804350 .  
  24. ↑ Moore, Cristopher ; Mertens, Stephan (2011), La naturaleza de la computación , Oxford University Press, pág. 366, ISBN  9780199233212.
  25. 1 2 R. E. Bryant, SM German y MN Velev, Verificación de microprocesadores mediante procedimientos de decisión eficientes para una lógica de igualdad con funciones no interpretadas , en Tablas analíticas y métodos relacionados, págs. 1–13, 1999.
  26. ↑ Akmal, Shyan; Williams, Ryan (2022). MAJORITY-3SAT (y problemas relacionados) en tiempo polinomial . págs. 1033–1043 . arXiv : 2107.02748 . doi : 10.1109/ FOCS52979.2021.00103 . ISBN  978-1-6654-2055-6.
  27. ↑ Blass, Andreas; Gurevich, Yuri (1982-10-01). "Sobre el problema de la satisfacibilidad única" . Information and Control . 55 (1): 80– 88. doi : 10.1016/S0019-9958(82)90439-9 . hdl : 2027.42/23842 . ISSN 0019-9958 . 
  28. ↑ "Complexity Zoo:U - Complexity Zoo" . complexityzoo.uwaterloo.ca . Archivado del original el 9 de julio de 2019. Consultado el 5 de diciembre de 2019 .
  29. ↑ Kozen, Dexter C. (2006). «Lección complementaria F: Satisfacibilidad única» . Teoría de la computación . Textos en informática. Springer. pág. 180. ISBN  9781846282973.
  30. ↑ Valiant, L.; Vazirani, V. (1986). "NP es tan fácil como detectar soluciones únicas" (PDF) . Theoretical Computer Science . 47 : 85–93 . doi : 10.1016/0304-3975(86)90135-0 .
  31. ↑ Buldas, Ahto; Lenin, Aleksandr; Willemson, Jan; Charnamord, Anton (2017). «Certificados de inviabilidad simples para árboles de ataque». En Obana, Satoshi; Chida, Koji (eds.). Avances en seguridad informática y de la información . Lecture Notes in Computer Science. Vol. 10418. Springer International Publishing. pp. 39–55 . doi : 10.1007/978-3-319-64200-0_3 . ISBN   9783319642000.
  32. ↑ Gi-Joon Nam; Sakallah, KA; Rutenbar, RA (2002). "Un nuevo enfoque de enrutamiento detallado de FPGA mediante satisfacibilidad booleana basada en búsqueda" (PDF) . IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems . 21 (6): 674. Bibcode : 2002ITCAD..21..674N . doi : 10.1109/TCAD.2002.1004311 . Archivado del original (PDF) el 15 de marzo de 2016. Recuperado el 4 de septiembre de 2015 .
  33. ↑ Selsam, Daniel; Lamm, Matthew; Bünz, Benedikt; Liang, Percy ; de Moura, Leonardo; Dill, David L. (11 de marzo de 2019). "Aprendizaje de un solucionador SAT a partir de supervisión de un solo bit". arXiv : 1802.03685 [ cs.AI ].
  34. ↑ "Página web de las competiciones internacionales SAT" . Consultado el 15 de noviembre de 2007 .
  35. ↑ Junqiang Peng y Mingyu Xiao (agosto de 2022). Mejoras adicionales para SAT en términos de longitud de fórmula (Informe técnico). arXiv : 2105.06131 .
  36. ↑ Junqiang Peng y Mingyu Xiao (octubre de 2023). "Mejoras adicionales para SAT en términos de longitud de fórmula". Information and Computation . 294 105085: Número de artículo 105085. doi : 10.1016/j.ic.2023.105085 .
  37. ↑ Huairui Chu y Mingyu Xiao y Zhe Zhang (julio de 2020). Un límite superior mejorado para SAT (Informe técnico). arxiv. arXiv : 2007.03829 .
  38. ↑ Huairui Chu y Mingyu Xiao y Zhe Zhang (octubre de 2021). "Una cota superior mejorada para SAT". Theoretical Computer Science . 887 : 51–62 . doi : 10.1016/j.tcs.2021.06.045 .
  39. ↑ S. Liu (julio de 2018). I. Chatzigiannakis y C. Kaklamanis y D. Marx y D. Sannella (eds.). Cadena, generalización del código de cobertura y algoritmo determinista para k -SAT . Proc. ICALP. LIPIcs. Vol. 107. Schloss Dagstuhl. pp. 88:1–13. doi : 10.4230/LIPIcs.ICALP.2018.88 .  

Fuentes

  • Este artículo incluye material de https://web.archive.org/web/20070708233347/http://www.sigda.org/newsletter/2006/eNews_061201.html del Prof. Karem A. Sakallah .

Lecturas adicionales

(por fecha de publicación)

  • Garey, Michael R.; Johnson , David S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness . WH Freeman. pp.  A9.1: LO1–LO7, pp. 259–260. ISBN 0-7167-1045-5.
  • Marques-Silva, J.; Glass, T. (1999). «Combinational equivalence checking using satisfiability and recursive learning». Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078) (PDF) . p.  145. doi : 10.1109/DATE.1999.761110 . ISBN 0-7695-0078-1Archivado (PDF) del original el 09/10/2022 .
  • Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "Verificación de modelos acotada mediante resolución de satisfacibilidad". Métodos formales en 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 sobre informática. vol.  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 eficiente de problemas SAT" (PDF) . IEEE Transactions on Computers . 55 (11): 1315. Bibcode : 2006ITCmp..55.1315B . doi : 10.1109/TC.2006.175 . S2CID 14819050. Archivado del original el 23 de octubre de 2016. 
  • Rodríguez, C.; Villagra, M.; Baran, B. (2007). "Algoritmos de equipo asíncronos para la satisfacibilidad booleana" (PDF) . 2007 2nd Bio-Inspired Models of Network, Information and Computing Systems . pp. 66– 69. doi : 10.1109/BIMNICS.2007.4610083 . S2CID 15185219 .  
  • Gomes, Carla P .; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). «Satisfiability Solvers». En Harmelen, Frank Van; Lifschitz, Vladimir; Porter, Bruce (eds.). Handbook of knowledge representation . Foundations of Artificial Intelligence. Vol.  3. Elsevier. pp. 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 satisfacibilidad booleana y sus aplicaciones en la verificación de modelos". Actas del IEEE . 103 (11): 2021– 2035. doi : 10.1109/JPROC.2015.2455034 . S2CID 10190144 . 
  • Knuth, Donald E. (2022). «Capítulo 7.2.2.2: Satisfacibilidad». El arte de la programación informática . Vol.  4B: Algoritmos combinatorios, Parte 2. Addison-Wesley Professional. pp. 185–369 . ISBN  978-0-201-03806-4.
Lecturas relacionadas
6 articulos
Cartel de 1901LógicaLa lógica estudia formas válidas de inferencia como el modus ponens . La lógica es el estudio del razonamiento correcto . Incluye tanto la lógica f...Ciencias de la ComputaciónCiencias de la ComputaciónÁreas fundamentales de la informática La informática es el estudio de la computación , la información y la automatización . [1] [2] [3] La informát...{\displaystyle {\mathcal {W}}}Interpretación (lógica)Una interpretación es una asignación de significado a los símbolos de un lenguaje formal . Muchos lenguajes formales utilizados en matemáticas , ló...{\displaystyle x+3=y}SatisfacibilidadEn lógica matemática , una fórmula es satisfacible si es verdadera bajo alguna asignación de valores a sus variables . Por ejemplo, la fórmulaincóg...{\displaystyle (A\land (B\lor C))}Fórmula bien formadaEn lógica matemática , lógica proposicional y lógica de predicados , una fórmula bien formada , abreviada WFF o wff , a menudo simplemente fórmula ...Álgebra de BooleEn matemáticas y lógica matemática , el álgebra de Boole es una rama del álgebra . Se diferencia del álgebra elemental en dos aspectos. En primer l...