En este artículo vamos a ver un estilo de programación que puede parecer totalmente extraño y capaz un poco mágico para muchos lectores. ¿Qué tal si pudiéramos escribir un test unitario para un problema y dejar que el compilador devuelva una implementación correcta? Llámenlo "test only" en lugar de "test driven". Vamos a traducir un problema en un lenguaje de especificación y usar el solver Z3 de Microsoft Research para encontrar una solución. No vamos a escribir ningún código de implementación.
Este es el problema que tengo como ejemplo, es el problema #4 del the Project Euler:
Un número capicúa se lee igual en las dos direcciones. El capicúa más grande hecho con el producto de dos números de 2 dígitos es 9009 = 91 × 99.
Encontrá el capicúa más grande hecho con el producto de dos números de 3 dígitos.
La aproximación habitual es usar fuerza bruta. Acá va un ejemplo en C#, que sospecho ser similar a lo que haría la mayoría de la gente:
(from factor1 in Enumerable.Range(100, 899) from factor2 in Enumerable.Range(100, 899) let product = factor1 * factor2 where IsPalindrome(product) // definido en otro lado orderby product descending select new { Factor1 = factor1, Factor2 = factor2, Product = product}).First()
No es una solución mala. Anda bastante rápido y devuelve la solución correcta, y se ven posibilidades de hacerla más eficiente. Me imagino que la mayoría de la gente declararía el problema como resuelto y pasaría a otra cosa.
Sin embargo, la sintaxis LINQ puede esconder el hecho que sigue siendo una solución de fuerza bruta. Cada vez que tenemos que pensar en como explicarle a una computadora como encontrar una solución en lugar de dar características del problema mismo, nos sobrecargamos cognitivamente e incrementamos las chances de cometer un error.
Además, ¿qué esconde ese IsPalindrome(product)? La mayoría de la gente convertiría el número en string, y la compararía con su valor invertido. Pero ocurre que las propiedades matemáticas de un número capicúa son críticas para encontrar una solución eficiente.
Para mi solución puramente declarativa, voy a usar el lenguaje SMT-LIB. Siendo un lenguaje de pura especificación, ¡no me permite definir nada de implementación! En lugar de eso, voy a usarlo para expresar las restricciones del problema, y luego usar el solver Z3 para encontrar una solución. SMT-LIB utiliza S-expresiones a lo LISP, entonces, sí, habrá paréntesis, pero no nos dejemos impresionar. Siempre vale la pena aprender lenguajes que nos hacen pensar problemas de manera distinta, y ¡creo que van a encontrar que SMT-LIB cumple!
Como este lenguaje va a parecerles extraño a muchos lectores, veamos este problema paso por paso.
Primero, tenemos que declarar ciertas variables usadas en el problema. Acá uso la palabra "variable" en el sentido matemático, más que informático: es un nombre para una desconocida, pero no es algo a lo cual le voy a asignar valores cambiantes. Entonces ahí van tres variables que se corresponden aproximadamente a las variables C# vistas más arriba:
(declare-const product Int) (declare-const factor1 Int) (declare-const factor2 Int)
En una S-expresión, el primer elemento dentro de las paréntesis es la función, y los otros elementos son argumentos. Entonces declare-const es la función acá y los elementos restantes son el nombre de la variable y su "sort" (tipo).
Luego, el problema dice que product debe ser el producto de los dos factores:
(assert (= (* factor1 factor2) product))
"assert" suena como un test unitario, ¿no? De hecho, mucha gente que se pone a usar un solver viniendo del desarrollo de software va a encontrar que programarlos es más cercano a escribir tests que escribir código. La línea arriba dice que factor1 * factor2 = product. Pero es una aserción, no una asignación; no hemos especificado valores para ninguna de esas variables.
El enunciado dice que los dos factores son números de 3 dígitos:
(assert (and (>= factor1 100) (<= factor1 999))) (assert (and (>= factor2 100) (<= factor2 999)))
Matemáticamente, ¿qué significa que un número sea capicúa? En ese caso, el producto más grande de números de 3 dígitos va a ser un número de 6 dígitos de la forma abccba, entonces product = 100000a + 10000b + 1000c + 100c + 10b + a. Como lo observé más arriba, expresar la relación de esa manera es clave para encontrar una solución que no sea fuerza bruta, usando álgebra. Pero no hace falta que sepas eso para usar Z3, ¡dado que Z3 conoce álgebra! Lo único que tenés que saber es que deberías expresar relaciones matemáticamente en lugar de manipular strings.
(declare-const a Int) (declare-const b Int) (declare-const c Int) (assert (= product (+ (* 100000 a) (* 10000 b) (* 1000 c) (* 100 c) (* 10 b) a)))
Supuse más arriba que a, b, and c eran números de un solo dígito, entonces tenemos que especificarlo. Además, a no puede ser 0, sino no tendremos un número de 6 dígitos.
(assert (and (>= a 1) (<= a 9))) (assert (and (>= b 0) (<= b 9))) (assert (and (>= c 0) (<= c 9)))
Estas 4 aserciones sobre a, b, y c son suficientes para determinar que un product es una capicúa. No hemos terminado todavía, pero veamos como vamos hasta ahí. (check-sat) pregunta a Z3 si hay una solución al problema que hemos planteado, y (get-model) imprime esa solución. Ahí va el script entero hasta ahora:
(declare-const product Int) (declare-const factor1 Int) (declare-const factor2 Int) (assert (and (>= factor1 100) (< factor1 1000))) (assert (and (>= factor2 100) (< factor2 1000))) (assert (= (* factor1 factor2) product)) (declare-const a Int) (declare-const b Int) (declare-const c Int) (assert (and (>= a 1) (<= a 9))) (assert (and (>= b 0) (<= b 9))) (assert (and (>= c 0) (<= c 9))) (assert (= product (+ (* 100000 a) (* 10000 b) (* 1000 c) (* 100 c) (* 10 b) a))) (check-sat) (get-model)
Cuando se lo damos a Z3 (¡probalo!), el solver contesta:
sat (model (define-fun c () Int 1) (define-fun b () Int 0) (define-fun a () Int 1) (define-fun product () Int 101101) (define-fun factor2 () Int 143) (define-fun factor1 () Int 707) )
¡Bastante bien! Acá sat significa que Z3 encontró una solución (sino, habría mostrado unsat). Elidiendo parte de la sintaxis, la solución encontrada fue 143 * 707 = 101101. No está mal para un código que tiene cero implementación, pero no es la respuesta del problema de Project Euler, que pide cuál es el producto más grande.
En le jerga de Z3, "optimización" se refiere a encontrar la "mejor" prueba para un teorema, no hacerlo lo más rápido que se pueda. ¿Pero como le decimos a Z3 de encontrar el producto más grande?
Z3 tiene una función llamada maximize. Si intentamos agregar (maximize product), y ejecutamos Z3, nos va a encontrar la solución que maximice la variable product. (Comprobado con la versión 4.5.1, con la versión 4.4.1, Z3 contesta un error).
Hay que saber que el programa que le estamos dando a Z3 involucra ecuaciones no-lineales (es decir, no solo con sumas y diferencias pero también con productos entre variables) sobre enteros. Esa teoría no es decidible, es decir, ningún algoritmo es capaz de siempre dar una respuesta para ese problema. Lo menos que se puede decir es que es probable que Z3 tome su tiempo para contestar.
Una forma de salir de ese problema es guiar un poco más la especificación. Dado que buscamos el producto más grande, podemos suponer que el valor de a en la solución va a ser más cerca del 9 que del 1. Podemos especificar (= a 9) y ver si existe una solución máxima con esa restricción. Ocurre que sí:
sat (model (define-fun factor1 () Int 913) (define-fun factor2 () Int 993) (define-fun c () Int 6) (define-fun a () Int 9) (define-fun b () Int 0) (define-fun product () Int 906609) )
El script final es:
(declare-const product Int) (declare-const factor1 Int) (declare-const factor2 Int) (assert (and (>= factor1 100) (< factor1 1000))) (assert (and (>= factor2 100) (< factor2 1000))) (assert (= (* factor1 factor2) product)) (declare-const a Int) (declare-const b Int) (declare-const c Int) (assert (and (>= a 1) (<= a 9))) (assert (and (>= b 0) (<= b 9))) (assert (and (>= c 0) (<= c 9))) (assert (= product (+ (* 100000 a) (* 10000 b) (* 1000 c) (* 100 c) (* 10 b) a))) (maximize product) (check-sat) (get-model)
Z3 en Ubuntu es la versión 4.4.1, mientras que la versión 4.5 ya está en GitHub.