# Resolver sudokus con un solucionador SAT La revista de pasatiempos de la universidad publica sudokus de 9 por 9, y este año también de 16 por 16 y de 25 por 25. Les piden comprobar cada tablero antes de imprimirlo: encontrar una solución, o avisar que no hay ninguna, porque de vez en cuando un tablero llega con un error de digitación. Un sudoku de orden k es un tablero de n por n celdas, con n = k · k, partido en cajas de k por k. Se llena con los números de 1 a n, de modo que cada número aparezca exactamente una vez en cada fila, en cada columna y en cada caja. Los valores que ya vienen en el tablero no se pueden cambiar. Esta vez no van a escribir una búsqueda. Van a escribir dos funciones, en `solution.cpp`: - `encode` recibe un sudoku y escribe una fórmula CNF, en formato DIMACS, con **una variable por cada terna (fila, columna, dígito)**. - `decode` recibe la respuesta de `minisat` y escribe el tablero resuelto. El archivo `driver.h` trae el `main`: lee el sudoku, llama a `encode`, revisa la fórmula, corre `minisat` y llama a `decode`. Así que el juez corre un solo programa, que lee de la entrada y escribe en la salida como siempre. No hace falta cambiar `driver.h`, y conviene leerlo. Si quieren, pueden agregar funciones auxiliares en `solution.cpp`. ## Entrada La primera línea tiene k. Luego vienen n líneas con n enteros cada una, separados por espacios: los valores del tablero, con 0 en las celdas vacías. ## Salida - Si el sudoku tiene solución, n líneas con n enteros cada una, separados por espacios. Puede tener varias soluciones, y cualquiera vale: un verificador revisa las reglas y que los valores dados sigan en su lugar. - Si no tiene solución, una línea con la palabra `imposible`. También es el caso de un tablero que ya trae un valor repetido. ## Lo que se revisa de la fórmula El programa termina con un error, que el juez muestra como `RE`, y explica la causa en la terminal, si la fórmula de `encode`: - no empieza con una línea `p cnf V C`, después de comentarios opcionales que empiezan con `c`; - no tiene V = n³; - no tiene exactamente C cláusulas, cada una terminada en 0; - usa un literal mayor que V. `minisat` solo daría un aviso con estos errores, y seguiría. Aquí no pasan. ## Límites - 1 ≤ k ≤ 5, así que n es 1, 4, 9, 16 o 25. - Cada valor está entre 0 y n. ## Ejemplo Entrada: ```text 2 1 0 0 0 0 0 3 0 0 4 0 0 0 0 0 2 ``` Salida: ```text 1 3 2 4 4 2 3 1 2 4 1 3 3 1 4 2 ``` ## Tiempo 3 segundos por caso, compilado con `-O2`. Corran `make test` para probar con el juez. ## Mirar cada parte El programa también corre cada mitad por separado, y el `Makefile` trae tres blancos para hacerlo con un caso: ```sh make formula CASO=01 # encode: escribe build/01.cnf y muestra su encabezado make respuesta CASO=01 # lo anterior, y corre minisat: escribe build/01.res y muestra el código con que terminó make decode CASO=01 # lo anterior, y llama a decode con esa respuesta ``` `minisat` termina con el código 10 si la fórmula es satisfacible, y con 20 si no lo es. Su archivo de respuesta tiene la palabra `SAT` y una línea de literales que termina en 0, o la palabra `UNSAT`. Una variable que no sale en ninguna cláusula tampoco sale en la respuesta. ## Comparar 1. Anoten las variables y las cláusulas que tiene su fórmula en `casos/14.in`, de 9 por 9, y en `casos/17.in`, de 25 por 25. El encabezado lo dice. Revisen esos números con la cuenta a mano. 2. Midan su programa en esos dos casos. En bash, `time ./build/solution < casos/14.in`. 3. Midan un backtracking en `casos/14.in`, que es un sudoku difícil para buscar por filas. Si conservan su solucionador de sudokus de Introducción a la Programación, úsenlo: lee 9 líneas de 9 dígitos, sin espacios y sin la primera línea con k. Si no, el curso trae uno, que ya tiene ese sudoku adentro. Dentro de `code/week-13`, corran `make` y luego `build/backtrack_bench`. Informa los nodos y el tiempo. Acepta un archivo con ese mismo formato. 4. Prueben quitar de `encode` cada regla de "a lo sumo uno", una por una. ¿Cuáles cambian el veredicto del juez, y por qué? Escriban los tiempos con la máquina en la que midieron y cómo lo hicieron: dependen de los dos.