Verificación de sistemas SAT

El objetivo es construir en ACL2 un sistema SAT con un doble objetivo

1. la eficiencia del sistema debe de ser comparable con los más avanzados y
2. las propiedades crítica del sistema deben de verificarse formalmente en ACL2.

Como punto de partida se puede usar el siguiente trabajo

Francisco J. Martín, José A. Alonso, María J. Hidalgo, José L. Ruiz Reina: Formal Verification of a Generic Framework to Synthesize SAT-Provers. Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313.

donde se muestra la construcción de un sistema SAT basado en DPLL.

Otro trabajo interesante para el proyecto es

Filip Maric Formal Verification of Modern SAT Solvers. The Archive of Formal Proofs, 2008-07-23.

donde verifica en Isabelle propiedades de sistemas SAT. El trabajo es interesante desde el punto de vista de las demostraciones, pero carece de algoritmos ejecutables.