[1] Hasta entonces el concepto de problema NP-completo no había sido definido.
El SAT sigue siendo NP-completo incluso si todas las fórmulas están en forma normal conjuntiva (FNC) con 3 variables por cláusula (3SAT-FNC) creando el problema (3SAT), o aun en el caso de que solo se permita un único valor verdadero en cada cláusula (3SAT en 1).
En 1962 se desarrolló el algoritmo DPLL por Davis-Putnam-Logemann-Lovelandes, un algoritmo completo basado en la vuelta atrás (backtracking) que sirve para decidir la satisfacibilidad de las fórmulas de lógica proposicional en una forma normal conjuntiva; es decir, para resolver el problema FNC-SAT, al igual que hacía el algoritmo anterior de Davis y Putnam.
El problema SAT es el problema de saber si, dada una expresión booleana con variables y sin cuantificadores, hay alguna asignación de valores para sus variables que hace que la expresión sea verdadera.
Sin embargo, más allá de este teorema, desde la última década se han desarrollado algoritmos eficientes y resistentes al cambio de tamaño del problema para SAT, y ha habido contribuciones con poderosos avances en nuestra capacidad para resolver automáticamente el problema de satisfactibilidad.
La 3-satisfactibilidad es un caso especial de -satisfactibilidad (-SAT), o simplemente satisfactibilidad (SAT), en la que cada cláusula contiene exactamente 3 literales.
Partiendo de SAT (el caso general) se reduce a 3-SAT y SAT 3 -en 1 y se puede demostrar que son NP-completos, entonces podemos usarlos para demostrar también otros problemas NP-completos.
Esto se hace mostrando cómo una solución a otro problema podría ser utilizado para resolver 3-SAT.
Una extensión significativa a la popularidad que ganó desde 2003 es el problema de las teorías de satisfactibilidad módulo, que permite enriquecer las fórmulas en la FNC con lineales, vectores, la restricción de que todas las variables sean distintas, y no interpretar funciones, etc.
Se cree ampliamente que los problemas son PSPACE completa-es son más difíciles que cualquier problema en NP, aunque esto aún no ha sido demostrada.
Una resolución del tipo SAT Algoritmo DPLL emplea un procedimiento sistemático de rastreo para buscar a explorar el espacio (del tamaño exponencial) los valores de las variables que se ajusten.
Algunos solucionadores potente disponibles entan en el dominio público, y son muy fáciles de usar.