Problema booleano de satisfacibilidad

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 satisfaga una determinada fórmula booleana. En otras palabras, pregunta si las variables de una fórmula booleana determinada pueden reemplazarse consistentemente por los valores VERDADERO o FALSO de tal manera que la fórmula se evalúe como VERDADERO. Si este es el caso, la fórmula se llama satisfacible. 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 y b = FALSO, lo que hace que (a Y NO b) = VERDADERO. Por el contrario, "a Y NO a" es insatisfactorio.

SAT es el primer problema que demostró ser NP-completo; véase el teorema de Cook-Levin. Esto significa que todos los problemas de la clase de complejidad NP, que incluye una amplia gama de problemas de decisión natural y optimización, son como mucho tan difíciles de resolver como SAT. No existe un algoritmo conocido que resuelva de manera eficiente cada problema del SAT y, en general, se cree que dicho algoritmo no existe; sin embargo, esta creencia no se ha probado 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 instancias de problemas que involucran decenas de miles de variables y fórmulas que consisten en millones de símbolos, lo cual es suficiente para muchos problemas prácticos de SAT de, por ejemplo, inteligencia artificial, diseño de circuitos 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 satisfactoria si puede hacerse VERDADERA asignando valores lógicos apropiados (es decir, VERDADERO, FALSO) a sus variables. El problema booleano de satisfacibilidad (SAT) es, dada una fórmula, para comprobar si es satisfacible. Este problema de decisión es de importancia central en muchas áreas de la informática, incluida la informática teórica, la teoría de la complejidad, los algoritmos, la criptografía y la inteligencia artificial.

Forma normal conjuntiva

Un literal es una variable (en cuyo caso se llama literal positivo) o la negación de una variable (llamado literal negativo). Una cláusula es una disyunción de literales (o un único literal). Una cláusula se denomina cláusula Horn si contiene como máximo un literal positivo. Una fórmula está en forma normal conjuntiva (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 conjuntiva normal; sus cláusulas primera y tercera 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 insatisfactoria, ya que para a=VERDADERO o < i>a=FALSO se evalúa como VERDADERO ∧ ¬VERDADERO (es decir, FALSO) o FALSO ∧ ¬FALSO (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 arbitrariamente muchas cláusulas generalizadas, siendo estas últimas 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 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 usa a continuación, siendo R el operador ternario que es VERDADERO justo cuando lo es exactamente uno de sus argumentos.

Usando las leyes del álgebra booleana, cada fórmula de lógica proposicional se puede transformar en una forma normal conjuntiva equivalente, que puede, sin embargo, ser exponencialmente más larga. Por ejemplo, transformando la fórmula (x₁∧y₁) ∨ (x_{2< /sub>∧y2) ∨... ∨ (xn ∧yn) en forma normal conjuntiva produce}

()x₁Alternativax₂Alternativa...x_n∧

()Sí.₁Alternativax₂Alternativa...x_n∧

()x₁AlternativaSí.₂Alternativa...x_n∧

()Sí.₁AlternativaSí.₂Alternativa...x_n∧... ∧

()x₁Alternativax₂Alternativa...Sí._n∧

()Sí.₁Alternativax₂Alternativa...Sí._n∧

()x₁AlternativaSí.₂Alternativa...Sí._n∧

()Sí.₁AlternativaSí.₂Alternativa...Sí._n);

mientras que el primero es una disyunción de n conjunciones de 2 variables, el segundo consta de 2ⁿ cláusulas de n< /i> variables.

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

Complejidad

SAT fue el primer problema NP-completo conocido, como lo probó Stephen Cook en la Universidad de Toronto en 1971 y de forma independiente Leonid Levin en la Academia Rusa de Ciencias en 1973. Hasta ese momento, el concepto de un NP-completo el problema ni siquiera existía. 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 de aceptación. Por ejemplo, decidir si un gráfico dado tiene 3 colores es otro problema en NP; si un gráfico tiene 17 3 colores válidos, la fórmula SAT producida por la reducción de Cook-Levin tendrá 17 asignaciones satisfactorias.

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

3-satisfacibilidad

La instancia 3-SAT ()x Alternativa x Alternativa Sí.∧x ∨Sí. ∨Sí.∧x Alternativa Sí. Alternativa Sí.) reducido a un problema de camarilla. Los vértices verdes forman un 3-clique y corresponden a la asignación satisfactoria x=FALSE, Sí.=TRUE.

Al igual que el problema de satisfacibilidad de fórmulas arbitrarias, determinar la satisfacibilidad de una fórmula en forma conjuntiva normal donde cada cláusula se limita 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 del SAT sin restricciones a 3-SAT, transforme cada cláusula l₁ ∨ ⋯ ∨ l< sub>n a una conjunción de cláusulas n - 2

()l₁ Alternativa l₂ Alternativa x₂∧

(x₂ Alternativa l₃ Alternativa x₃∧

(x₃ Alternativa l₄ Alternativa x₄∧ ∧

(x_{n 3 - 3} Alternativa l_{n − 2} Alternativa x_{n − 2}∧

(x_{n − 2} Alternativa l_{n − 1} Alternativa l_n)

donde x₂, ⋯ , 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 igualmente satisfactorias. 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.

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 de 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 no -contradictorias literales de diferentes cláusulas, cf. fotografía. El gráfico tiene una clique c si y solo si la fórmula es satisfactoria.

Existe un algoritmo aleatorio simple debido a 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 de decidir correctamente 3-SAT.

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

Selman, Mitchell y Levesque (1996) brindan datos empíricos sobre la dificultad de las fórmulas 3-SAT generadas aleatoriamente, según sus parámetros de tamaño. La dificultad se mide en 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 3-SAT ni más difícil que 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 < Los literales k se pueden rellenar con variables ficticias fijas para 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< sub>1} = ⋯ = d_k=FALSE puede conducir a una tarea 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< /i> ∨ ¬y.

Casos especiales del SAT

Forma normal conjuntiva

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

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. De hecho, tal fórmula es satisfactoria si y solo si al menos una de sus conjunciones es satisfecha, y una conjunción es satisfecha 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 se limitan 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 exponenciales convertir un problema general de SAT a una forma normal disyuntiva; para un intercambio de ejemplo "∧" y "∨" en el ejemplo de expansión exponencial anterior para formas normales conjuntivas.

Exactamente-1 3-satisfacibilidad

Izquierda: Reducción de Schaefer de una cláusula 3-SAT x Alternativa Sí. Alternativa z. El resultado R es TRUE (1) si exactamente uno de sus argumentos es TRUE, y FALSE (0) de lo contrario. Todas las 8 combinaciones de valores para x,Sí.,z son examinados, uno por línea. Las variables frescas a,...f puede ser elegido para satisfacer todas las cláusulas (exactamente una verde argumento para cada R) en todas las líneas excepto el primero, donde x Alternativa Sí. Alternativa z Es FALSE. Bien. Una reducción más simple con las mismas propiedades.

Una variante del problema de satisfacibilidad de 3 es el uno-en-tres 3-SAT (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 para que cada cláusula tenga exactamente un literal VERDADERO (y por lo tanto exactamente dos literales FALSO). En contraste, el 3-SAT ordinario requiere que cada cláusula tenga al menos un literal VERDADERO. Formalmente, un problema 3-SAT de uno en tres 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 uno en tres son positivos, el problema de satisfacibilidad se llama 3-SAT positivo uno en tres.

Uno de 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 la integridad NP 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 la 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 de tiempo polinomial de 3-SAT a uno de cada tres 3-SAT. Sea "(x o y o z)" ser una cláusula en una fórmula 3CNF. Agregue seis variables booleanas nuevas a, b, c, d, e, y f, para simular esta cláusula y ninguna otra. Entonces la fórmula R(x,a,d) ∧ R(< i>y,b,d) ∧ R(a,b< /i>,e) ∧ R(c,d,f) ∧ R(z,c,FALSE) se puede satisfacer mediante alguna configuración de las variables nuevas si y solo si al menos una de x, y o z es VERDADERO, vea la imagen (izquierda). Por lo tanto, cualquier instancia de 3-SAT con cláusulas m y n variables puede convertirse en una instancia equisatisfecha de 3-SAT con 5m cláusulas y variables n+6m. Otra reducción involucra solo cuatro variables nuevas y tres cláusulas: R(¬x,a,b) ∧ < i>R(b,y,c) ∧ R(c, d,¬z), ver imagen (derecha).

No todos son iguales 3-satisfacibilidad

Otra variante es el problema de no todos son iguales 3-satisfacibilidad (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 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, por el teorema de la dicotomía de Schaefer.

SAT Lineal

Una fórmula de 3-SAT es SAT lineal (LSAT) si cada cláusula (visto 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 es NP-completo.

2-satisfacibilidad

SAT es más fácil si el número de literales en una cláusula se limita a 2 como máximo, 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 adicionalmente todas las operaciones OR en literales se cambian a operaciones XOR, el resultado se denomina exclusivo-o-2-satisfacibilidad, que es un problema completo para la clase de complejidad SL = L.

Cuerno de satisfacción

El problema de decidir la satisfacibilidad de una conjunción dada de cláusulas Horn se denomina Horn-satisfactability, o HORN-SAT. Se puede resolver en tiempo polinomial mediante un solo paso del algoritmo de propagación de unidades, que produce el modelo mínimo único del conjunto de cláusulas de Horn (en lugar del conjunto de literales asignados a TRUE). Cuerno-satisfacibilidad es P-completo. Puede verse como la versión P's del problema de satisfacibilidad booleano. Además, la decisión sobre la verdad de las fórmulas de Horn cuantificadas se puede hacer en tiempo polinomial.

Las cláusulas Horn son interesantes 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 se puede reescribir como x₁ ∧... ∧ x_n → y, es decir, si x₁,...,x_n son VERDADEROS, entonces y también debe ser VERDADERO.

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₁ ∨ ¬x₂) ∧ (¬x ₁ ∨ x₂ ∨ x₃) ∧ ¬x< /i>₁ no es una fórmula de Horn, pero se le puede cambiar el nombre a la fórmula de Horn (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₂ ∨ ¬< i>y₃) ∧ ¬x₁ introduciendo y_{3 como negación de x3. Por el contrario, no se cambia el nombre de (x1 ∨ ¬x2 ∨ ¬x3) ∧ (¬x1 ∨ x2 ∨ x3) ∧ ¬x1 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 puede resolverse realizando primero este reemplazo y luego verificando la satisfacibilidad de la fórmula de Horn resultante.}

Una fórmula con 2 cláusulas puede ser insatisfecha (rojo), 3-satisfecha (verde), xor-3-satisfecha (azul), o/y 1-en-3-satisfecho (amarillo), dependiendo del recuento de la TRE-literal en la cláusula 1 (hor) y 2a (vert).

Satisfacción XOR

Otro caso especial es la clase de problemas en los que cada cláusula contiene operadores XOR (es decir, exclusivos o) en lugar de (simples) operadores OR. 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 mediante eliminación gaussiana; vea el recuadro para ver un ejemplo. Esta refundición se basa en el parentesco entre las álgebras booleanas y los anillos booleanos, y en el hecho de que la aritmética módulo 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, ya 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, en base al resultado, inferir que el problema 3-SAT es solucionable o que el problema 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-satisfactability es NP-completo, a diferencia de SAT.

Teorema de la dicotomía de Schaefer

Las restricciones anteriores (CNF, 2CNF, 3CNF, Horn, XOR-SAT) obligaron a las fórmulas consideradas a ser 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 está en P o NP-completo. La pertenencia a P de las fórmulas de satisfacibilidad de 2CNF, Horn y XOR-SAT son casos especiales de este teorema.

La siguiente tabla resume algunas variantes comunes de SAT.

Extensiones del SAT

Una extensión que ha ganado una popularidad significativa desde 2003 es la teoría del módulo de satisfacibilidad (SMT) que puede enriquecer las fórmulas CNF con restricciones lineales, matrices, todas las restricciones diferentes, sin interpretar funciones, etc. Tales extensiones normalmente siguen siendo NP-completas, pero ahora hay disponibles solucionadores muy eficientes que pueden manejar muchos de estos tipos de restricciones.

El problema de la satisfacibilidad se vuelve más difícil si tanto "para todos" (∀) y "existe" Los cuantificadores (∃) pueden vincular las variables booleanas. Un ejemplo de tal expresión sería ∀x ∀y ∃< i>z (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z); es válido, 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. El propio SAT (tácitamente) utiliza únicamente cuantificadores ∃. Si en su lugar sólo 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 se puede demostrar 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. Usando 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 haga 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 la fórmula TRUE. Se sabe que está completo para PP, una clase probabilista.
• #SAT, el problema de contar cuántas asignaciones variables satisfacen una fórmula, es un problema contable, 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. Es completo para EE.UU., la clase de complejidad que describe problemas solvable por un tiempo polinomio no-determinista Máquina de Turing que acepta cuando hay exactamente un camino de aceptación no determinista y rechaza lo contrario.
• UNAMBIGUOUS-SAT es el nombre dado al problema de satisfiabilidad cuando la entrada está restringida a las fórmulas que tienen en la mayoría de una asignación satisfactoria. El problema también se llama USAT. Un algoritmo de resolución para UNAMBIGUOUS-SAT se permite exhibir cualquier comportamiento, incluyendo un bucle interminable, en una fórmula que tiene varias tareas satisfactorias. Aunque este problema parece más fácil, Valiant y Vazirani han demostrado que si hay un algoritmo práctico (es decir, polinomial aleatorizado) para resolverlo, entonces todos los problemas en NP pueden resolverse tan fácilmente.
• MAX-SAT, el problema máximo de satisfiabilidad, es una generalización de SAT de la FNP. Pide el número máximo de cláusulas que pueden ser satisfechas por cualquier asignación. Tiene algoritmos de aproximación eficientes, pero es NP-hard para resolver exactamente. Peor aún, es APX-completo, lo que significa que no hay un esquema de aproximación de tiempo polinomio (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 monotona (es decir, una fórmula sin ninguna negación). Los pesos de las variables proposición se dan en la entrada del problema. El peso de una asignación es la suma de pesos de variables verdaderas. Ese problema es el NP-completo (véase Th. 1 de).

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

Encontrar una tarea satisfactoria

Si bien SAT es un problema de decisión, el problema de búsqueda de encontrar una tarea satisfactoria se reduce a SAT. Es decir, cada algoritmo que responda correctamente si una instancia de SAT es solucionable puede usarse para encontrar una tarea satisfactoria. Primero, la pregunta se hace sobre la fórmula dada Φ. Si la respuesta es "no", la fórmula es insatisfactoria. De lo contrario, la pregunta se formula en la fórmula parcialmente instanciada Φ{x1=TRUE}, es decir, Φ con la primera variable x₁ reemplazada por TRUE 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 se utiliza en varios teoremas de la teoría de la complejidad:

NP ⊆ P/poly ⇒ PH = NOV2 (Karp–Lipton theorem)

NP ⊆ BPP ⇒ NP = RP

P = NP ⇒ FP = FNP

Algoritmos para resolver SAT

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, 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 la automatización del diseño electrónico (EDA) incluyen verificación de equivalencia formal, verificación de modelo, verificación formal de microprocesadores canalizados, generación automática de patrones de prueba, enrutamiento de FPGA, problemas de planificación y programación, etc. Un motor de resolución de SAT también se considera un componente esencial en la caja de herramientas de automatización del diseño electrónico.

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

Los solucionadores de SAT se desarrollan y comparan en concursos de resolución de SAT. 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.