zebra
1.0.0
Hoje, em 2024, o projeto está praticamente sem manutenção. Estou usando-o como playground para algumas coisas que quero experimentar, mas não recomendo que ninguém construa isso.
Lembra dos quebra-cabeças lógicos parecidos com este? Eles tinham pistas como:
Há uma casa entre Tushar e Maui.
O videogame favorito de Ruby é Pokémon.
Quem bebe chai não gosta da cor azul.
Eu adorava isso quando criança, e assistir à palestra PyCon 2019 de Raymond Hettinger me inspirou a revisitar esses problemas. Ele nos mostrou como resolvê-los; Eu queria aprender como gerá-los.
Usando Python moderno e solucionadores de satisfação de restrição (SAT), este projeto pode ser usado para criar quebra-cabeças de zebra aleatórios.
Este projeto usa Python 3.12 e Poesia.
O ponto de entrada para este projeto é src/main.py ; portanto, execute-o com [poetry run] python -m src.main . Usamos questionário para criar uma CLI com interatividade simples.
Outros arquivos importantes são:
puzzle.py contém a classe principal Puzzle, que consiste principalmente em cola em torno de pistas e elementos de quebra-cabeça
clues.py define uma pista (uma instrução de nível superior que podemos converter em um CNF) e várias fábricas, como found_at ou same_house ; generate.py possui utilitários para criar pistas
elements.py e traptor_elements.py possuem vários elementos de quebra-cabeça
Finalmente, sat_utils.py contém os utilitários básicos para interagir com o solucionador SAT pycosat. Este código foi quase inteiramente escrito por Raymond Hettinger para sua palestra de 2019 (obrigado!).
❯ poesia execute python -m src.main? Qual é o tamanho do quebra-cabeça? (Use as teclas de seta)
» 5
4
3? Escolha um tipo de Traptor (use as teclas de seta)
? Tropical
» ? Mítico? ? O quebra-cabeça deveria incluir smoothies? (Use as teclas de seta)
" Sim
Não? ? O quebra-cabeça deveria incluir tampas de garrafa? (Use as teclas de seta)
" Sim
Não
Pistas
-----# ... Algum texto de sabor omitido ...1. O Lesser Traptor e o Swamp Traptor estão na mesma casa.
2. O Ancient Traptor está logo à esquerda do smoothie de chocolate.
3. O Ancient Traptor e o smoothie de limão estão na mesma casa.
4. O Volcano Traptor está diretamente à esquerda do Restless Traptor.
5. As tampas Cave Traptor e Green estão na mesma casa.
6. Existem duas casas entre o Lake Traptor e o Snapper Traptor.
7. As tampas verdes e o Fierce Traptor estão na mesma casa.
8. Há uma casa entre as tampas pretas e o smoothie de coco.
9. Há uma casa entre o Lesser Traptor e o smoothie Kiwi.
10. O Dweller Traptor e o smoothie de chocolate estão na mesma casa.
11. As tampas vermelhas e o Dweller Traptor estão na mesma casa.
12. As tampas vermelhas estão diretamente à esquerda do Hoarder Traptor.
13. Existem duas casas entre o smoothie de carambola e as tampas amarelas.
14. As tampas das garrafas Lake Traptor e Black estão na mesma casa.
15. O Stalker Traptor e o Fierce Traptor estão na mesma casa.
Solução
┏━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━ ┳━━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━ ━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━┓
┃ Ninho ┃ MythicalTraptorPrimário ┃ MythicalTraptorSecundário ┃ MythicalTraptorTerciário ┃ Smoothie ┃ Tampa de garrafa ┃
┡━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━ ╇━━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━ ━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━┩
│ 1 │ o Fierce Traptor │ o Cave Traptor │ o Stalker Traptor │ o smoothie de carambola │ Tampinhas verdes │
│ 2 │ o Ancient Traptor │ o Lake Traptor │ o Crawler Traptor │ o smoothie de limão │ tampas pretas │
│ 3 │ o Lesser Traptor │ o Swamp Traptor │ o Dweller Traptor │ o smoothie de chocolate │ tampas de garrafa vermelhas │
│ 4 │ o Greater Traptor │ o Volcano Traptor │ o Hoarder Traptor │ o smoothie de coco │ tampas de garrafa amarelas │
│ 5 │ o Restless Traptor │ o Mountain Traptor │ o Snapper Traptor │ o smoothie de Kiwi │ Tampas de garrafas azuis │
└──────┴──────────────────────── ┴──────────────────────────┴───── ────────────────────┴──────────── ────────────┴───────────────────┘Em fevereiro de 2024, o que preciso para considerar isso “feito”?
Adicione modelos HTML, porque o site para o qual eu os construo exige que eu inclua coisas como tags BR.
Melhore os detalhes gramaticais na saída, como letras maiúsculas no texto de sabor.
Adicione os recursos de cabeçalho/rodapé que copio/colo no envio.
Talvez, algum dia, eu considere uma interface web. Eu poderia levantar o projeto usando pyodide ou o pycosat baseado em C causaria problemas? E quanto a outra interface de programação lógica, como PySAT, programação de conjunto de respostas ou outras deste segmento HN?
Isso pode acontecer. Mas o projeto finalmente chegou a um ponto que me deixa feliz e, por isso, estou animado para compartilhar e escrever sobre ele.
18/02: torne as saídas mais simples, menos detalhadas e mais bonitas. Atualize este README com nova formatação e alterações. Use o gerador de quebra-cabeças para criar um novo quebra-cabeça, finalmente!
17/02: atualize a assinatura do quebra-cabeça para aceitar apenas a solução, inferindo os elementos e classes de elementos dela. Adicione uma exibição mais agradável para a solução.
26/11: Limpe a lógica de geração de quebra-cabeças/soluções. Deixe o usuário escolher o tamanho do quebra-cabeça.
25/11: Nomeie alguns tipos comuns como aliases de tipo (obrigado, Python 3.12). Use registro em vez de impressões.
Adicione testes para tipos de pistas em generate.py .
Corrija um bug que introduzi em clues.py . Esse arquivo é muito difícil de entender, mas também é difícil escrever testes de unidade; converter expressões booleanas em CNF manualmente não é divertido.
Ajuste os pesos das pistas na solução. Prepare-se para integrar as classes de quebra-cabeça e solução.
Remova a seleção de Smoothie no estilo caixa de seleção, porque ela apenas atrapalha ao tentar fazer quebra-cabeças rapidamente.
Continue adicionando testes. Conclua os testes de unidade para sat_utils.py e inicie alguns para clues.py , embora esse arquivo seja muito difícil de testar devido à dificuldade de calcular manualmente as conversões de DNF para CNF.
Os próximos passos são unificar o quebra-cabeça e a solução, criar um __repr__ melhor e simplificar a forma como representamos o tamanho do quebra-cabeça (atributo em Puzzle , tupla de ints 1 a N, apenas o número n_houses , etc.).
Remova o preto e use ruff para formatação. Atualizar dependências. Adicione nova CLI com uso mais simples e claro; python -m src.main .
Renomear SATLiteral -> PuzzleElement (batido, gato, etc.); isso esclarece que não é um Literal no sentido booleano e, em vez disso, é um nome para, por exemplo, personagens de um quebra-cabeça.
Crie um novo tipo SATLiteral (que é um str em um sobretudo); isso representa o literal no sentido de variável booleana, como "O valor el está na casa loc " ou "O valor el não está na casa loc ". Internamente, estes são representados por algum inteiro i e sua contraparte negativa -i .
Use (o novo) SATLiteral como o tipo de retorno de comb(el: str, loc: int) -> SATLiteral , mapeando elementos do quebra-cabeça para literais e neg(el: SATLiteral) -> SATLiteral para negar um literal.
Adicionar Clause: tuple[SATLiteral, ...] representando um "∨" (OR booleano; disjunção) de literais; por exemplo, (1, -5, 6) é uma disjunção que afirma que x_1 é verdadeiro, x_5 não é verdadeiro ou x_6 é verdadeiro.
Adicione ClueCNF: list[Clause] , representando um "∧" (conjunção booleana AND;) de Clause s. Um quebra-cabeça em CNF é um "AND de ORs" ("∧ de ∨s" ou "∧ de cláusulas").
Imprima o quebra-cabeça com mais clareza. Reduza a verbosidade da redução de pistas.
Gere aleatoriamente o quebra-cabeça (com uma semente) em cada corrida.
Mova os exemplos para seus próprios arquivos. Atualize para Python 3.12 (beta). Adicione mais regras de lint. Limpe as importações.
Adicione ferramentas de desenvolvimento (black, ruff, pyright); execute black & ruff no pré-commit. Atualize alguns tipos.
"∧" é o booleano AND
"∨" é o booleano OR
uma cláusula é um "∨ de literais"
um CNF é um "∧ de cláusulas" ou equivalentemente um "∧ de ∨s" ("AND de ORs")
Um DNF, por outro lado, é um “∨ de ∧s”. O DNF é a resposta para um problema do SAT; um DNF de "A ou B ou C" indica que A, B e C são todas atribuições válidas (satisfatórias). Converter um CNF em DNF é, portanto, NP-difícil, pois a partir do DNF você pode ler soluções para o CNF.
CNF é um ∧ de ∨s, onde ∨ está sobre variáveis ou suas negações (literais); um ∨ de literais também é chamado de cláusula. DNF é um ∨ de ∧s; um ∧ de literais é chamado de termo.
O núcleo deste projeto é expressar o quebra-cabeça da zebra como um problema de satisfatibilidade booleana (SAT) (Wikipedia.
O problema 3-SAT é conhecido por ser NP-completo . Ou seja, provavelmente não existe um algoritmo de tempo polinomial para resolvê-lo. No entanto, isso descreve apenas o caso geral.
Nosso problema é pequeno e bem especificado (afinal, estamos criando isso especificamente para humanos!). Isso o torna uma excelente opção para solucionadores SAT modernos, e a palestra (e notas) de Hettinger demonstra isso lindamente.
