Generalidades
SAT es el ejemplo canónico de problema NP-completo. Consiste en determinar, dada una fórmula booleana en forma de conjunción de disyunciones (donde cada disyunción se llama claúsula), si existe una asignación de valores a sus variables que hagan verdadera la fórmula (esto se denomina “satisfacer” la fórmula y de ahí viene el nombre SATisfiability asignado al problema). Por ejemplo,
ya que la asignación 
ya que no existe forma de asignarle valores de verdad a 
Un algoritmo simple para resolverlo es probar distintas combinaciones de valores para las variables hasta encontrar alguna que haga verdadera a la fórmula o agotar las posibles combinaciones de valores. En el peor caso (cuando no se pueda encontrar una asignación), el algoritmo examinará 
Pero, aunque no se cree posible encontrar un algoritmo de complejidad sub-exponencial para este problema, si se conocen algoritmos que mejoran significativamente al algoritmo anteriormente descrito. A continuación estudiaremos uno de los más simples, conocido como DPLL.
DPLL
El algoritmo DPLL, llamado así por las iniciales de sus creadores, mejora al algoritmo anteriormente descrito mediante el uso de dos técnicas:
- Backtracking: la asignación de variables para satisfacer la fórmula se construye variable por variable, volviéndose atrás apenas se detecta que la asignación de valor efectuada a una variable hace imposible satisfacer la fórmula.
- Unit propagation: cuando una de las cláusulas contiene una sola variable (negada o no), la conjunción obliga a que esta variable tome un valor específico. El proceso de unit propagation consiste en propagar el efecto de esta asignación de valor sobre el resto de las cláusulas.
Si bien la referencia original utilizaba una técnica adicional de eliminación de literales puros, esta no proporciona ventajas significativas en performance por lo que la omitiremos del análisis.
Implementación de DPLL en Javascript
A continuación analizaremos una implementación de este algoritmo en Javascript. La implementación enlazada toma una claúsula por línea, utilizando - como operador de negación y sin requerir operadores explícitos para la disyunción y la conjunción. Por ejemplo, la fórmula 
x1 x2 -x3
-x2 x3
-x1
Un script incluido en el archivo HTML se encarga de transformar el problema a un formato canónico, en el que las variables son reemplazadas por números enteros mayores que uno y la negación lógica se transforma en una negaciór aritmética. Las cláusulas se convierten en arrays Javascript, con lo que la fórmula anterior quedaría transformada en [[1, 2, -3], [-2, 3], [-1]].
La primera función que analizaremos es simplifyClause():
function simplifyClause(c, a) {
var nc, i;
nc = [];
for (i = 0; i < c.length; i++) {
if (c[i] in a) {
return null;
} else if (!(-c[i] in a)) {
nc.push(c[i]);
}
}
return nc;
}
Toma dos parámetros, c y a, que representan una claúsula dada como array de valores numéricos y una asignación de valores a las variables dada como un diccionario, respectivamente. El diccionario se utiliza como conjunto, empleando el número correspondiente a la variable como clave y true como valor; la clave numérica se niega para indicar la asignación de un valor falso a la variable. Por ejemplo, la asignación 
{1: true, -2: true}.
La función simplemente copia la claúsula c a una nueva cláusula nc, examinando las apariciones de variables a la luz de la asignación de valores que se utiliza en ese momento. Si encuentra una aparición de variable que se corresponda con una asignación incluida en a, significa que la cláusula es verdadera; por lo tanto devuelve null indicando la “desaparición” de la misma. Por el contrario, si encuentra la aparición negada en a, simplemente no la incluye en la nueva claúsula (ya que es falsa, el valor neutro de la disyunción).
Continuando con las funciones, podemos examinar la función applyAssignment():
function applyAssignment(f, a) {
var nf, i, nc;
nf = [];
for (i = 0; i < f.length; i++) {
nc = simplifyClause(f[i], a);
if (nc !== null) {
nf.push(nc);
}
}
return nf;
}
Esta función hace lo mismo que la anteriormente descrita pero sobre toda una fórmula. Como la simplificación se efectúa cláusula por cláusula, el único procesamiento no delegado a simplifyClause() es la supresión de las claúsulas que son devueltas como null (que son las que simplifyClause() determinó como tautológicas dada la asignación a).
Dejando a un lado funciones auxiliares, como cloneAssignment(), solo resta analizar la función principal: recDPLL().
function recDPLL(f, a) {
var i, na, v, ret;
f = applyAssignment(f, a);
if (f.length === 0) {
return [true, a];
}
for (i = 0; i < f.length; i++) {
if (f[i].length === 0) {
return [false, {}];
} else if (f[i].length === 1) {
na = cloneAssignment(a);
na[f[i][0]] = true;
return recDPLL(f, na);
}
}
na = cloneAssignment(a);
na[f[0][0]] = true;
ret = recDPLL(f, na);
if (ret[0]) {
return ret;
}
delete na[f[0][0]];
na[-f[0][0]] = true;
return recDPLL(f, na);
}
En primer lugar la función simplifica la fórmula f con la asignación de valores a, empleando las técnicas anteriormente descritas. Si esta simplificación conduzca a una fórmula vacía, dado que una conjunción vacía es verdadera, devuelve true y la asignación de valores que llevó a este valor de verdad.
Si no se llegó a una fórmula vacía es obvio que restan cláusulas no tautológicas dentro de la misma (todo esto tomando como “dada” la asignación a de variables). Estas pueden ser de dos tipos: cláusulas contradictorias o contingencias. Como las cláusulas restantes no pueden contener variables con valores asignados, dado el anterior paso de simplificación, una cláusula contradictoria solo puede ser vacía.
El procesamiento restante de la fórmula consiste en recorrer las cláusulas buscando cláusulas vacías o con una sola aparición de variable. Si se encuentra un cláusula vacía, estaremos en presencia de una contradicción que imposibilita aumentar a hasta convertirla en una asignación que satisfaga a la fórmula en cuestión. Por lo tanto se realiza backtracking devolviendo [false, {}].
La aparición de una cláusula con una sola variable es más interesante, ya que puede verse como “forzando” una asignación. En este caso es cuando se realiza el proceso de unit propagation, que consiste simplemente en incorporar la única asignación compatible con la cláusula unitaria dentro de a y continuar la búsqueda recursiva. No es necesario simplificar la fórmula, ya que esto se realizará apenas comience la ejecución de la nueva instancia de recDPLL().
Por último, si la fórmula no cae en ninguno de estos dos casos se realiza una exploración recursiva normal.
Utilizando SAT para resolver otros problemas
Para mostrar como SAT puede utilizarse para resolver problemas lógicos en general, veremos como aplicarlo a la resolución de un problema de lógica conocido como “el problema de Einstein” (aunque es bastante poco probable que Einstein efectivamente lo haya creado). La formulación que utilizaremos es la siguiente:
1. There are 5 houses (along the street) in 5 different colors: blue, green, red, white and yellow.
2. In each house lives a person of a different nationality: Brit, Dane, German, Norwegian and Swede.
3. These 5 owners drink a certain beverage: beer, coffee, milk, tea and water,
smoke a certain brand of cigar: Blue Master, Dunhill, Pall Mall, Prince and blend,
and keep a certain pet: cat, bird, dog, fish and horse.
4. No owners have the same pet, smoke the same brand of cigar, or drink the same beverage.Hints
1. The Brit lives in a red house.
2. The Swede keeps dogs as pets.
3. The Dane drinks tea.
4. The green house is on the left of the white house (next to it).
5. The green house owner drinks coffee.
6. The person who smokes Pall Mall rears birds.
7. The owner of the yellow house smokes Dunhill.
8. The man living in the house right in the center drinks milk.
9. The Norwegian lives in the first house.
10. The man who smokes blend lives next to the one who keeps cats.
11. The man who keeps horses lives next to the man who smokes Dunhill.
12. The owner who smokes Blue Master drinks beer.
13. The German smokes Prince.
14. The Norwegian lives next to the blue house.
15. The man who smokes blend has a neighbor who drinks water.The question is: Who keeps fish?
(Puede verse también una formulación equivalente en español.)
Si bien probablemente la técnica más simple de aplicar en este caso sea constraint-based programming, podemos aplicar SAT sin problemas. Para ello debemos decidir primero que variables utilizaremos, siendo una elección razonable numerar las casas, colores, nacionalidades, bebidas, cigarros y mascotas e introducir variables booleanas asociando las casas con los distintos atributos de la persona que vive en ellas. Eso nos da un total de 
La traducción de estas relaciones a cláusulas SAT puede ser algo tediosa, por lo que nos conviene emplear un script simple para este proceso. En caso de no disponer de Python, puede consultarse la salida del script en ep_sat.txt. La nomenclatura de las variables es simple: hijk, donde i indica el núemro de casa, j indica el atributo en cuestión y k indica un posible valor de este atributo. En el código Python pueden verse los detalles de como se traducen las implicaciones y restricciones a disyunciones.
Introduciendo las cláusulas SAT en la página de prueba de DPLL, podemos encontrar el siguiente resultado:
SATISFIABLE h0c4 h1c0 h2c2 h3c1 h4c3 h0n3 h0b4 h0s1 h0p0 h1n1 h1b3 h1s4 h1p4 h2n0 h2b2 h2s2 h2p1 h3n2 h3b1 h3s3 h3p3 h4n4 h4b0 h4s0 h4p2 -h0c3 -h2b0 -h2b1 -h2b3 -h2b4 -h0b2 -h1b2 -h3b2 -h4b2 -h2n1 -h2c1 -h3c3 -h0n0 -h0n1 -h0n2 -h0n4 -h1n3 -h2n3 -h3n3 -h4n3 -h2s0 -h1c1 -h1c2 -h1c3 -h1c4 -h0c0 -h2c0 -h3c0 -h4c0 -h1n0 -h2c3 -h0c1 -h0c2 -h2c4 -h3c2 -h4c2 -h3c4 -h4c1 -h4c4 -h3n0 -h4n0 -h5c3 -h3b0 -h3b3 -h3b4 -h0b1 -h1b1 -h4b1 -h3n1 -h0s0 -h0s2 -h0s3 -h0s4 -h1s1 -h2s1 -h3s1 -h4s1 -h1p0 -h1p1 -h1p2 -h1p3 -h0p4 -h2p4 -h3p4 -h4p4 -h1n4 -h1s2 -h3s0 -h4s4 -h0b0 -h0b3 -h1b4 -h4b4 -h2s4 -h3s4 -h0p1 -h0p2 -h0p3 -h2p0 -h3p0 -h4p0 -h1n2 -h4n1 -h1b0 -h4b3 -h1s0 -h1s3 -h2n2 -h2n4 -h2s3 -h3s2 -h4s2 -h4s3 -h2p2 -h2p3 -h3p1 -h4p1 -h4n2 -h3n4 -h4p3 -h3p2
Como el pez sería la mascota número 3, buscamos apariciones de p3 en una variable no negada y encontramos h3p3. Buscando la nacionalidad del habitante de la casa número 3 encontramos h3n2, por lo que podemos concluir que el alemán es quien tiene un pez como mascota (coincidiendo con la solución dada a este problema).
Spin Foam 