Verificación de traductores de problemas combinatorios en SAT
Muchos problemas combinatorios se resuelven mejor traduciéndolos a lógica proposicional y usando sistemas SAT que con algoritmos específicos. El objetivo del proyecto es la verificación formal de los traductores algunos de dichos problemas.
La idea del proyecto parte del trabajo de J. Harrison A short survey of automated reasoning.
José A. Alonso 11:34, 19 November 2008 (CET)