El problema SAT es uno de los problemas abiertos más desafiantes de la informática. Me apasiona desde mis primeros pasos en algoritmos en concursos de programación, y luego en mi tesis de grado.
En mi tesis, desarrollé la siguiente versión de Demuba, un demostrador automático diseñado originalmente por el Profesor e Investigador Ricardo Oscar Rodríguez. La nueva versión introduce una heurística para guiar la selección de fórmulas y obtener una refutación, si existe, en menos tiempo. Esta heurística se diseñó combinando diferentes enfoques para resolver el problema SAT. Esta solución está extensamente especificada en el documento de tesis.
DEI-Engineering 