Este algoritmo fue desarrollado por Martin Davis y Hilary Putnam para poder poder llevar a cabo la comprabación de las formulas de la lógica proposicional en  FNC (forma normal conjuntiva). Se puede decir que esto es una foma de resolución en la cual las variables son elegidas iterativamente y eliminadas mediante la resolución de cada cláusula en la que que la variable aparece afirmada con una cláusula en la que la variable es negada.

este algoritmo es para los siguientes casos:

• para cada variable en la fórmula

• para cada cláusula  que contenga la variable y cada cláusula  que contenga la negación de la variable

• resolver  y  y añadir la resolución a la fórmula

• eliminar todas las cláusulas originales que contengan la variable o su negación

 

aveces se reifieren a ese algoritmo como "algoritmo DPLL", pero es incorrecto, está relacionado pero es diferente