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 de J. Harrison A short survey of automated reasoning.

José A. Alonso 11:34, 19 November 2008 (CET)