Formal Correctness Proof for DPLL Procedure

Pilip Marić y Predrag Janicić (2009) Formal Correctness Proof for DPLL Procedure. Aceptado en Informatica. Pendiente de publicación.

---

En este trabajo se presenta la formalización en Isabelle/Isar de una demostración de la corrección del procedimiento DPLL (Davis-Putnam-Logemann-Loveland). La formalización se encuentra classic DPLL procedure. Aunque afirma que es la primera formalización de DPLL, en el artículo Formal Verification of a Generic Framework to Synthesize SAT-Provers (Journal of Automated Reasoning. Vol. 32. Núm. 4. 2004. Pag. 287-313) se presenta una formalización del procedimiento DPLL en ACL2 con la demostración en ACL2 de su corrección.

La estructura del trabajo es la siguiente

1. Introducción en la que se presenta el problema SAT, el procedimiento DPLL, sus mejoras, su papel en los modernos SAT y sus aplicaciones. Me ha parecido interesante las razones que justifican la formalización (1) algunos SMT de los que han participado en las competiciones no son adecuados y (2) el trabajo incrementa el conocimiento matemático formalizado.
2. Antecedentes donde comenta el procedimiento DPLL junto con comentarios sobre Isabelle, Isar y la verificación de programas.
3. Notaciones y definiciones donde presenta las notaciones, definiciones (de variable, literal, cláusula, fórmula e interpretación, variable de un literal, literal complementario, ocurrencia de un literal en una fórmula, conjuntos de variables de una cláusula (de una fórmula y de una interpretación), cuando un literal (cláusula o fórmula) es verdadero (o falso) en una interpretación, interpretaciones consistentes, modelo de una fórmula), y las proposiciones básicas de la formalización en Isabelle.
4. Formalización del procedimiento DPLL
   1. Sustituciones en donde define la sustitución de un literal de una fórmula por un booleano, enuncia las propiedades básicas de la sustitución y demuestra el lema de bifurcación.
   2. Cláusulas unitarias en donde define las cláusulas unitarias y demuestra el lema de las cláusulas unitarias.
   3. Literales puros en donde define los literales puros y el lema de los literales puros.
   4. Definición del procedimiento DPLL en donde define el procedimiento DPLL en donde los procedimientos auxiliares sólo son especificados. Una definición de los procedimientos auxiliares se da en el apéndice.
   5. Terminación y corrección del procedimiento DPLL en donde demuestra la terminación del procedimiento a partir de la dismininución del número de literales y la corrección por inducción
5. Formalización en Isabelle/Isar en donde presenta la definición en Isabelle/Isar del procedimiento DPLL y la demostración de su corrección.
6. Trabajos relacionados donde comenta algunas formalizaciones en Isabelle y las descripciones abstractas de DPLL.
7. Conclusiones y trabajos futuros donde vuelve a repetir que es la primera formalización de DPLL (aunque anteriormente comentamos la realizada en ACL2) y propone continuar la tarea formalizando la corrección de buscadores SAT y SMT correspondientes a las actuales implementaciones.

José A. Alonso 20:34, 10 April 2009 (CEST)