Verificación de traductores de problemas combinatorios en SAT
Revisión del 21:03 22 oct 2008 de Jalonso (discusión | contribuciones)
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 A short survey of automated reasoning.