Verificación de traductores de problemas combinatorios en SAT

De WikiGLC
Saltar a: navegación, buscar

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.