La demostración automática de teoremas consiste de métodos algorítmicos para lograr demostraciones por medio de una computadora. La dificultad para resolver un problema puede depender del tipo de lógica que se utilice, en nuestro caso, al utilizar la Lógica Proposicional el problema es decidible pero NP-completo. Por lo que para resolverlos solo existen algoritmos directos de tiempo exponencial en el peor caso. De ahí la importancia de disminuir el tiempo de ejecución de cualquier implementación.
La satisfactibilidad proposicional (SAT) es un problema importante en las ciencias de la computación debido a que la mayoría de las veces es más eficiente pasar un problema a SAT y resolverlo con alguno de los programas existentes, que desarrollar una versión particular para dicho problema. Recientemente ha sido muy importante para una amplia gama de aplicaciones practicas las cuales incluyen el diseño, síntesis y verificación de circuitos integrados, optimización de FPGA, inteligencia artificial y planificación de tareas. Una de las principales aplicaciones que han motivado un nuevo auge de los resolvedores de satisfactibilidad ha sido la verificación de circuitos integrados, dando como resultado un desarrollo acelerado de nuevos diseños.
En este trabajo presentamos diversas implementaciones del algoritmo de Davis Putnam, que permiten la experimentación con el algoritmo por medio de la modificación de las variables que influyen directamente en su desempeño. Las versiones paralelas se desarrollaron con pThreads y MPI, con el fin de obtener una eficiencia mejor que la versión secuencial al valernos de la utilización de varios procesadores. Con las implementaciones en paralelo se experimentaron diversas estrategias de selección de cláusulas y literales para hacer más eficiente el algoritmo.