Verification of a DPLL Transition System in Rocq

Imagina un mundo donde las computadoras están jugando constantemente un juego de alto riesgo de "Verdadero o Falso". En este juego, la computadora recibe un enorme nudo enredado de declaraciones lógicas —como una receta que dice: "Si añades azúcar, también debes añadir harina, pero si añades harina, no puedes añadir sal". El objetivo es encontrar una forma de seguir la receta sin romper ninguna regla. Este es el problema de la Satisfacibilidad (SAT). Es el equivalente digital de intentar encajar un millón de diferentes piezas de rompecabezas en una caja donde algunas piezas son rojas, otras son azules, y las instrucciones dicen: "No pongas rojo junto a azul".

¿Por qué nos importa? Porque esto no es solo un acertijo lógico; es el motor detrás de casi todo lo complejo en la informática. Desde el diseño de microchips hasta la demostración de que un teorema matemático es verdadero, las computadoras utilizan resolvedores (solvers) de SAT para navegar por estos enormes laberintos lógicos. Pero aquí está el truco: estos resolvedores son increíblemente complejos. Si un pequeño error se esconde en el código, la computadora podría decirte con total confianza que una prueba es válida cuando en realidad es un sinsentido. Por eso los matemáticos y científicos de la computación están obsesionados con la verificación formal. Piensa en ello como la construcción de una red de seguridad súper estricta e inquebrantable. En lugar de simplemente esperar que la computadora funcione, utilizan un tipo especial de "microscopio matemático" (llamado asistente de pruebas) para revisar cada uno de los pasos de la lógica, asegurando que la máquina nunca mienta sobre la respuesta.

La Gran Aventura del Artículo: Construyendo una Máquina Lógica Confiable

En este artículo, Julia Dijkstra y Benedikt Ahrens dan un gran salto hacia la creación de estas máquinas lógicas confiables. No se limitaron a escribir un programa; construyeron un esqueleto matemáticamente probado de un famoso método de resolución lógica llamado DPLL (Davis-Putnam-Logemann-Loveland) dentro de una herramienta llamada Rocq.

Piensa en el método DPLL no como un robot rígido que sigue un guion, sino como un juego de "Cambio de Estado". Imagina a un detective intentando resolver un misterio. El detective comienza con una libreta vacía (sin pistas). Tiene un conjunto de reglas para actualizar su libreta:

1. La Regla del "¡Ah, ya veo!" (Propagación de Unidad): Si una pista dice "El mayordomo lo hizo O la criada lo hizo", y el detective ya sabe que la criada es inocente, la libreta debe actualizarse para decir "El mayordomo lo hizo". El detective no tiene otra opción; la lógica fuerza el movimiento.
2. La Regla de la "Suposición Pura" (Literal Puro): Si el detective ve una pista sobre "el jardinero", pero nunca ve una pista sobre "el jardinero no lo hizo", puede suponer con seguridad que el jardinero está involucrado sin temor a una contradicción.
3. La Regla de "Ramificación" (Decidir): Si el detective se queda atascado, elige una pista al azar (como "El mayordomo lo hizo") y la anota como una decisión. Esto es un cruce en el camino.
4. La Regla del "Ups, Giro Equivocado" (Retroceso/Backtrack): Si el detective anota una decisión y más tarde encuentra una contradicción (una pista que dice "El mayordomo no lo hizo"), tiene que borrar todo lo que sucedió después de esa decisión, cambiar la decisión (ahora el mayordomo no lo hizo) e intentarlo de nuevo.
5. La Regla del "Fin del Juego" (Fallo): Si borra todo, cambia la última decisión y aun así encuentra una contradicción, el juego ha terminado. El misterio es irresoluble.

El logro principal de los autores es tomar todo este juego y escribirlo en un lenguaje que el asistente de pruebas Rocq pueda leer y verificar. No se limitaron a decir: "Esto parece correcto". Probaron tres cosas masivas:

• Corrección: Si el juego termina con una solución, esa solución es definitivamente real. La computadora no va a alucinar un modelo.
• Completitud: Si existe una solución, el juego la encontrará. La computadora no se quedará trabada ni se rendirá cuando no debería hacerlo.
• Terminación: El juego nunca se ejecutará para siempre. Está matemáticamente garantizado que se detendrá, ya sea con una solución o con un "Fin del Juego".

Añadiendo un Nuevo Giro: La Regla "Pura"

Una de las contribuciones geniales del artículo es que añadieron una regla específica a su juego que algunas versiones anteriores de esta teoría dejaron fuera: la Regla del Literal Puro. En la analogía del detective, este es el momento en que el detective se da cuenta: "Oye, nunca he visto evidencia en contra del jardinero, así que asumiré que el jardinero es el culpable". Los autores demostraron que añadir esta regla hace que el juego sea más rápido sin romper ninguna de las garantías de seguridad. Demostraron que, incluso con este atajo adicional, la lógica sigue siendo hermética.

De la Teoría a un Robot Real (Pero Simple)

Después de probar que las reglas del juego funcionan perfectamente en la teoría, los autores se preguntaron: "¿Podemos construir realmente un robot que juegue este juego?". Crearon una estrategia —un conjunto de instrucciones para el detective sobre qué regla elegir a continuación. Construyeron una versión concreta de esta estrategia en Rocq y luego utilizaron una herramienta mágica llamada extracción para convertir su prueba matemática en un programa real escrito en OCaml.

Probaron este nuevo robot con algunos acertijos simples. ¡Funcionó! Resolvió problemas correctamente, incluyendo un acertijo llamado zebra.cnf con 155 variables y 1,135 cláusulas. Sin embargo, los autores son muy honestos sobre las limitaciones de su robot. Es como un coche de juguete de prueba de concepto: conduce perfectamente y demuestra que el motor funciona, pero aún no es un coche de carreras de Fórmula 1. Es lento porque utiliza listas simples para recordar las pistas, mientras que los coches de carreras del mundo real utilizan memoria de alta velocidad. Los autores admiten que esta versión no está lista para vencer a los gigantes industriales utilizados por las empresas hoy en día, pero es un núcleo verificado. Es una base pequeña e inquebrantable sobre la cual se pueden construir futuros resolvedores más rápidos y más inteligentes.

Lo Que Esto Significa para el Futuro

El artículo no pretende haber resuelto el problema de crear el resolvedor de SAT más rápido del mundo. En su lugar, afirma haber construido el plano más seguro posible. Al probar las reglas abstractas en Rocq, han creado un "núcleo de confianza". Los investigadores del futuro ahora pueden tomar este plano y añadir las funciones sofisticadas de los resolvedores modernos —como "aprender de los errores" (aprendizaje de cláusulas) o "saltar varios pasos hacia atrás" (retroceso no cronológico)— con la confianza de que la lógica subyacente sigue siendo sólida.

En resumen, Dijkstra y Ahrens no solo construyeron un mejor coche; construyeron el plano para un coche que nunca puede chocar, demostando que la lógica detrás de las ruedas es matemáticamente perfecta. Es un pequeño paso verificado que allana el camino para máquinas lógicas mucho más grandes, complejas y confiables en el futuro.