Hoy, en 2024, el proyecto prácticamente no se mantiene. Lo estoy usando como patio de juegos para algunas cosas que quiero probar, pero no recomiendo a nadie que construya a partir de esto.
¿Recuerdas los acertijos de lógica que se parecían a este? Tenían pistas como:
Hay una casa entre Tushar y Maui.
El videojuego favorito de Ruby es Pokémon.
Al bebedor de chai no le gusta el color azul.
Me encantaban cuando era niño y ver la charla de Raymond Hettinger sobre PyCon 2019 me inspiró a revisar estos problemas. Nos mostró cómo resolverlos; Quería aprender a generarlos.
Utilizando Python moderno y solucionadores de satisfacción de restricciones (SAT), este proyecto se puede utilizar para crear rompecabezas de cebra aleatorios.
Este proyecto utiliza Python 3.12 y Poetry.
El punto de entrada a este proyecto es src/main.py
; en consecuencia, ejecútelo con [poetry run] python -m src.main
. Usamos cuestionarios para crear una CLI con interactividad simple.
Otros archivos importantes son:
puzzle.py
contiene la clase principal de Puzzle, que en su mayoría se pega alrededor de pistas y elementos de rompecabezas.
clues.py
define una pista (una declaración de nivel superior que podemos convertir a CNF) y varias fábricas, como found_at
o same_house
; generate.py
tiene utilidades para crear pistas
elements.py
y traptor_elements.py
tienen varios elementos de rompecabezas
Finalmente, sat_utils.py
contiene las utilidades básicas para interactuar con el solucionador SAT pycosat. Este código fue escrito casi en su totalidad por Raymond Hettinger para su charla de 2019 (¡gracias!).
❯ poesía ejecutar python -m src.main? ¿Qué tan grande es el rompecabezas? (Utilice las teclas de flecha) » 5 4 3? Elija un tipo de Traptor (use las teclas de flecha) ? Tropical » ? ¿Mítico? ? ¿El rompecabezas debería incluir batidos? (Utilice las teclas de flecha) " Sí ¿No? ? ¿Debería el rompecabezas incluir tapas de botellas? (Utilice las teclas de flecha) " Sí No Pistas -----# ... Se omitió algún texto de estilo ...1. El Atrapador Menor y el Atrapador del Pantano están en la misma casa. 2. El Ancient Traptor está directamente a la izquierda del batido de chocolate. 3. El Ancient Traptor y el Smoothie de Limón están en la misma casa. 4. El Volcano Traptor está directamente a la izquierda del Restless Traptor. 5. El Cave Traptor y las tapas de botellas verdes están en la misma casa. 6. Hay dos casas entre Lake Traptor y Snapper Traptor. 7. Las tapas de botellas verdes y el Fierce Traptor están en la misma casa. 8. Hay una casa entre las chapas negras y el batido de coco. 9. Hay una casa entre Lesser Traptor y Kiwi Smoothie. 10. El Dweller Traptor y el batido de chocolate están en la misma casa. 11. Las tapas de botellas rojas y el Dweller Traptor están en la misma casa. 12. Las tapas de botellas rojas están directamente a la izquierda del Hoarder Traptor. 13. Hay dos casas entre el batido de carambola y las chapas amarillas. 14. Las tapas de botellas de Lake Traptor y Black están en la misma casa. 15. El Stalker Traptor y el Fierce Traptor están en la misma casa. Solución ┏━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━ ┳━━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━ ━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━┓ ┃ Nido ┃ MythicalTraptorPrimary ┃ MythicalTraptorSecundario ┃ MythicalTraptorTerciario ┃ Batido ┃ Tapa de botella ┃ ┡━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━ ╇━━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━ ━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━┩ │ 1 │ el Atrapador Feroz │ el Atrapador de Cuevas │ el Atrapador Acechador │ el batido de carambola │ Tapas de botellas verdes │ │ 2 │ el Atrapador Antiguo │ el Atrapador del Lago │ el Atrapador Reptador │ el batido de Limón │ Tapas de botellas negras │ │ 3 │ el Atrapador Menor │ el Atrapador del Pantano │ el Atrapador Habitante │ el batido de chocolate │ Tapas de botellas rojas │ │ 4 │ el Gran Atrapador │ el Atrapador de Volcán │ el Atrapador Acaparador │ el batido de coco │ Tapas de botellas amarillas │ │ 5 │ el Atrapador Inquieto │ el Atrapador de Montaña │ el Atrapador de Pargos │ el batido de Kiwi │ Tapas de botellas azules │ └──────┴──────────────────────── ┴──────────────────────────┴───── ────────────────────┴──────────── ────────────┴───────────────────┘
En febrero de 2024, ¿qué necesito para considerar esto "hecho"?
Agregue plantillas HTML, porque el sitio para el que las construyo requiere que incluya cosas como etiquetas BR.
Mejore los detalles gramaticales en la salida, como las mayúsculas en el texto de estilo.
Agregue los recursos de encabezado/pie de página que copio/pego en el envío.
Quizás algún día considere una interfaz web. ¿Podría levantar el proyecto usando piodio o el pycosat basado en C causaría problemas? ¿Qué pasa con otra interfaz de programación lógica, como PySAT, programación de conjuntos de respuestas u otras de este hilo de HN?
Esto puede suceder. Pero el proyecto finalmente está en un lugar con el que estoy contento y por eso estoy emocionado de compartirlo y escribir sobre él.
18/02: hacer que los resultados sean más simples, menos detallados y más bonitos. Actualice este README con nuevos formatos y cambios. ¡Usa el generador de rompecabezas para crear un nuevo rompecabezas, finalmente!
17/02: actualice la firma del rompecabezas para aceptar solo la solución, infiriendo los elementos y las clases de elementos a partir de ella. Agregue una visualización más agradable para la solución.
26/11: Limpiar la lógica de generación de rompecabezas/soluciones. Deje que el usuario elija el tamaño del rompecabezas.
25/11: Nombra algunos tipos comunes como alias de tipo (gracias, Python 3.12). Utilice registros en lugar de impresiones.
Agregue pruebas para tipos de pistas dentro de generate.py
.
Corrige un error que introduje en clues.py
. Ese archivo es muy difícil de entender, pero también es difícil escribir pruebas unitarias para él; convertir expresiones booleanas a CNF manualmente no es divertido.
Sintonice los pesos de las pistas en la solución. Prepárate para integrar las clases de acertijos y soluciones.
Elimina la selección de Smoothie, similar a una casilla de verificación, porque simplemente interfiere cuando intentas hacer rompecabezas rápidamente.
Continúe agregando pruebas. Termine las pruebas unitarias para sat_utils.py
y comience un par para clues.py
, aunque ese archivo es muy difícil de probar debido a la dificultad de calcular manualmente las conversiones de DNF a CNF.
Los siguientes pasos son unificar el rompecabezas y la solución, crear un mejor __repr__
y simplificar la forma en que representamos el tamaño del rompecabezas (atributo en Puzzle
, tupla de enteros 1 a N, solo el número n_houses
, etc.).
Elimine el negro y use gorguera para formatear. Actualizar dependencias. Agregue una nueva CLI con un uso más simple y claro; python -m src.main
.
Cambiar el nombre SATLiteral
-> PuzzleElement
(batido, gato, etc.); esto aclara que no es un literal en el sentido booleano sino que es un nombre para, por ejemplo, personajes de un rompecabezas.
Cree un nuevo tipo SATLiteral
(que es una str
con una gabardina); esto representa el literal en el sentido de variable booleana, como "El valor el está en casa loc " o "El valor el no está en casa loc ". Internamente, estos están representados por algún número entero i y su contraparte negativa -i .
Utilice (el nuevo) SATLiteral
como tipo de retorno de comb(el: str, loc: int) -> SATLiteral
, asignando elementos del rompecabezas a literales, y neg(el: SATLiteral) -> SATLiteral
para negar un literal.
Agregar Clause: tuple[SATLiteral, ...]
que representa un "∨" (OR booleano; disyunción) de literales; por ejemplo, (1, -5, 6)
es una disyunción que establece que x_1
es verdadero, x_5
no es verdadero o x_6
es verdadero.
Agregue ClueCNF: list[Clause]
, que representa un "∧" (Y booleano; conjunción) de Clause
s. Un rompecabezas en CNF es un "Y de OR" ("∧ de ∨s" o "∧ de Cláusulas").
Imprime el rompecabezas con mayor claridad. Reducir la verbosidad de la reducción de pistas.
Genera aleatoriamente el rompecabezas (con una semilla) en cada ejecución.
Mueva los ejemplos a sus propios archivos. Actualización a Python 3.12 (beta). Agregue más reglas de pelusa. Limpiar las importaciones.
Agregar herramientas de desarrollo (black, ruff, pyright); ejecute black & ruff en precompromiso. Actualiza algunos tipos.
"∧" es el AND booleano
"∨" es el OR booleano
una cláusula es una "∨ de literales"
un CNF es un "∧ de Cláusulas" o, de manera equivalente, un "∧ de ∨s" ("Y de OR")
Un DNF, por el contrario, es un "∨ de ∧s". El DNF es la respuesta a un problema del SAT; un DNF de "A o B o C" indica que A, B y C son todas asignaciones válidas (satisfactorias). Por lo tanto, la conversión de un CNF a un DNF es NP-difícil, ya que desde el DNF se pueden leer soluciones al CNF.
CNF es una ∧ de ∨s, donde ∨ está sobre variables o sus negaciones (literales); una ∨ de literales también se llama cláusula. DNF es un ∨ de ∧s; un ∧ de literales se llama término.
El núcleo de este proyecto consiste en expresar el rompecabezas de la cebra como un problema de satisfacibilidad booleana (SAT) (Wikipedia.
Se sabe que el problema 3-SAT es NP-completo . Es decir, probablemente no exista ningún algoritmo de tiempo polinomial para resolverlo. Sin embargo, esto sólo describe el caso general.
Nuestro problema es pequeño y está bien especificado (después de todo, ¡los estamos creando específicamente para humanos!). Esto lo convierte en una excelente opción para los solucionadores de SAT modernos, y la charla (y las notas) de Hettinger lo demuestran maravillosamente.