zebra
1.0.0
Saat ini, pada tahun 2024, sebagian besar proyek tidak terpelihara. Saya menggunakannya sebagai taman bermain untuk beberapa hal yang ingin saya coba, tapi saya tidak menyarankan siapa pun membangunnya.
Ingat teka-teki logika yang terlihat seperti ini? Mereka memiliki petunjuk seperti:
Ada satu rumah antara Tushar dan Maui.
Video game favorit Ruby adalah Pokemon.
Peminum chai tidak menyukai warna biru.
Saya menyukai hal ini semasa kecil, dan menonton ceramah Raymond Hettinger di PyCon 2019 menginspirasi saya untuk meninjau kembali masalah ini. Dia menunjukkan kepada kita cara mengatasinya; Saya ingin belajar cara menghasilkannya.
Dengan menggunakan pemecah Python dan kepuasan kendala (SAT) modern, proyek ini dapat digunakan untuk membuat teka-teki zebra acak.
Proyek ini menggunakan Python 3.12 dan Puisi.
Titik masuk ke proyek ini adalah src/main.py ; oleh karena itu, jalankan dengan [poetry run] python -m src.main . Kami menggunakan kuesioner untuk membuat CLI dengan interaktivitas sederhana.
File penting lainnya adalah:
puzzle.py berisi kelas Puzzle utama, yang sebagian besar menempel di sekitar petunjuk dan elemen puzzle
clues.py mendefinisikan petunjuk (pernyataan tingkat tinggi yang dapat kita ubah menjadi CNF) dan beberapa pabrik, seperti found_at atau same_house ; generate.py memiliki utilitas untuk membuat petunjuk
elements.py dan traptor_elements.py memiliki berbagai elemen teka-teki
Terakhir, sat_utils.py berisi utilitas dasar untuk berinteraksi dengan pycosat pemecah SAT. Kode ini hampir seluruhnya ditulis oleh Raymond Hettinger untuk ceramahnya di tahun 2019 (terima kasih!).
❯ puisi dijalankan python -m src.main? Berapa besar teka-teki tersebut? (Gunakan tombol panah)
» 5
4
3? Pilih jenis Traptor (Gunakan tombol panah)
? Tropis
» ? Mitos? ? Haruskah teka-teki itu menyertakan smoothie? (Gunakan tombol panah)
" Ya
TIDAK? ? Haruskah teka-teki itu menyertakan tutup botol? (Gunakan tombol panah)
" Ya
TIDAK
Petunjuk
-----# ... Beberapa teks rasa dihilangkan ...1. Lesser Traptor dan Swamp Traptor berada di rumah yang sama.
2. The Ancient Traptor berada tepat di sebelah kiri smoothie Cokelat.
3. Traptor Kuno dan Smoothie Lemon ada di rumah yang sama.
4. Volcano Traptor berada tepat di sebelah kiri Restless Traptor.
5. Cave Traptor dan Green Bottlecaps berada di rumah yang sama.
6. Ada dua rumah di antara Lake Traptor dan Snapper Traptor.
7. Tutup botol hijau dan Fierce Traptor berada di rumah yang sama.
8. Ada satu rumah di antara tutup botol hitam dan smoothie kelapa.
9. Ada satu rumah di antara Lesser Traptor dan smoothie Kiwi.
10. Dweller Traptor dan Chocolate smoothie berada di rumah yang sama.
11. Tutup botol merah dan Dweller Traptor berada di rumah yang sama.
12. Tutup botol merah tepat di sebelah kiri Hoarder Traptor.
13. Ada dua rumah di antara smoothie Belimbing dan tutup botol Kuning.
14. Lake Traptor dan Black Bottlecaps ada di rumah yang sama.
15. Stalker Traptor dan Fierce Traptor berada di rumah yang sama.
Larutan
┏━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━━━ ┳━━━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━ ━━━━━━━━━━━━┳━━━━━━━━━━━━━━━━━━━┓
┃ Sarang ┃ MythicalTraptorPrimary ┃ MythicalTraptorSecondary ┃ MythicalTraptorTertiary ┃ Smoothie ┃ Bottlecap ┃
┡━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━━━ ╇━━━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━ ━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━━━━┩
│ 1 │ Perangkap Ganas │ Perangkap Gua │ Perangkap Penguntit │ smoothie Belimbing │ Tutup botol hijau │
│ 2 │ Perangkap Kuno │ Perangkap Danau │ Perangkap Perayap │ smoothie Lemon │ Tutup botol hitam │
│ 3 │ Perangkap Kecil │ Perangkap Rawa │ Perangkap Penghuni │ smoothie Cokelat │ Tutup botol merah │
│ 4 │ Perangkap Besar │ Perangkap Gunung Berapi │ Perangkap Penimbun │ Smoothie Kelapa │ Tutup Botol Kuning │
│ 5 │ Perangkap Gelisah │ Perangkap Gunung │ Perangkap Kakap │ smoothie Kiwi │ Tutup botol biru │
└──────┴──────────────────────────┴─────────────────── ─────────┴───── ──────────— ────────────────┘Pada bulan Februari 2024, apa yang perlu saya anggap sebagai "selesai"?
Tambahkan templat HTML, karena situs tempat saya membuat ini mengharuskan saya menyertakan hal-hal seperti tag BR.
Perbaiki kesalahan tata bahasa pada keluaran, seperti penggunaan huruf besar pada teks rasa.
Tambahkan sumber daya header/footer yang saya salin/tempel ke dalam kiriman.
Mungkin suatu hari nanti saya akan mempertimbangkan antarmuka web. Bisakah saya mengangkat proyek menggunakan pyodide, atau apakah pycosat berbasis C akan menimbulkan masalah? Bagaimana dengan antarmuka pemrograman logika lainnya, seperti PySAT, pemrograman kumpulan jawaban, atau lainnya dari thread HN ini?
Hal ini mungkin saja terjadi. Namun proyek ini akhirnya sampai pada titik yang membuat saya senang, jadi saya bersemangat untuk berbagi dan menulis tentangnya.
18/2: membuat keluaran lebih sederhana, lebih sedikit bertele-tele, lebih cantik. Perbarui README ini dengan format dan perubahan baru. Akhirnya gunakan pembuat teka-teki untuk membuat teka-teki baru!
17/2: perbarui tanda tangan teka-teki untuk menerima solusi saja, menyimpulkan elemen dan kelas elemen darinya. Tambahkan tampilan yang lebih bagus untuk solusinya.
26/11: Membersihkan logika pembuatan teka-teki/solusi. Biarkan pengguna memilih ukuran puzzle.
25/11: Sebutkan beberapa tipe umum sebagai alias tipe (terima kasih, Python 3.12). Gunakan logging alih-alih mencetak.
Tambahkan tes untuk tipe petunjuk dalam generate.py .
Perbaiki bug yang saya perkenalkan di clues.py . File itu sangat sulit untuk dipahami, tetapi juga sulit untuk menulis pengujian unit; mengonversi ekspresi boolean ke CNF dengan tangan bukanlah hal yang menyenangkan.
Sesuaikan bobot petunjuk dalam solusi. Bersiaplah untuk mengintegrasikan kelas teka-teki dan solusi.
Hapus pilihan Smoothie seperti kotak centang, karena itu hanya menghalangi saat mencoba membuat teka-teki dengan cepat.
Lanjutkan menambahkan tes. Selesaikan pengujian unit untuk sat_utils.py dan mulai beberapa untuk clues.py , meskipun file tersebut sangat sulit untuk diuji karena sulitnya menghitung konversi DNF-ke-CNF secara manual.
Langkah selanjutnya adalah menyatukan puzzle dan solusinya, membuat __repr__ yang lebih baik, dan menyederhanakan cara kita merepresentasikan ukuran puzzle (atribut pada Puzzle , tupel int 1 hingga N, hanya angka n_houses , dll.).
Hapus warna hitam dan gunakan ruff untuk memformat. Perbarui dependensi. Tambahkan CLI baru dengan penggunaan yang lebih sederhana dan jelas; python -m src.main .
Ganti nama SATLiteral -> PuzzleElement (smoothie, kucing, dll.); ini menjelaskan bahwa ini bukan Literal dalam arti boolean dan melainkan sebuah nama untuk misalnya, karakter dalam teka-teki.
Buat SATLiteral tipe baru (yang merupakan str di jas hujan); ini mewakili literal dalam arti variabel boolean, seperti "Nilai el ada di lokasi rumah" atau "Nilai el tidak ada di lokasi rumah." Secara internal, ini diwakili oleh beberapa bilangan bulat i dan pasangan negatifnya -i .
Gunakan SATLiteral (yang baru) sebagai tipe kembalian comb(el: str, loc: int) -> SATLiteral , memetakan elemen teka-teki ke literal, dan neg(el: SATLiteral) -> SATLiteral untuk meniadakan literal.
Tambahkan Clause: tuple[SATLiteral, ...] mewakili "∨" (boolean OR; disjungsi) literal; misal (1, -5, 6) merupakan disjungsi yang menyatakan x_1 benar, x_5 tidak benar, atau x_6 benar.
Tambahkan ClueCNF: list[Clause] , mewakili "∧" (boolean AND; konjungsi) dari Clause s. Teka-teki di CNF adalah "AND of ORs" ("∧ of ∨s" atau "∧ of Clauses").
Cetak puzzle dengan lebih jelas. Kurangi verbositas pengurangan petunjuk.
Hasilkan teka-teki secara acak (dengan benih) di setiap proses.
Pindahkan contoh ke dalam file mereka sendiri. Perbarui ke Python 3.12 (beta). Tambahkan lebih banyak aturan lint. Bersihkan impor.
Tambahkan alat pengembang (hitam, ruff, pyright); jalankan black & ruff di pra-komit. Perbarui beberapa jenis.
"∧" adalah boolean AND
"∨" adalah boolean OR
Klausa adalah "∨ dari Literal"
CNF adalah "∧ dari Klausul," atau setara dengan "∧ dari ∨s" ("DAN dari OR")
Sebaliknya, DNF adalah "∨ dari ∧s". DNF adalah jawaban atas masalah SAT; DNF "A atau B atau C" berbunyi bahwa A, B, dan C semuanya merupakan tugas yang valid (memuaskan). Oleh karena itu, mengubah CNF menjadi DNF adalah NP-hard, karena dari DNF Anda dapat membacakan solusi untuk CNF.
CNF adalah ∧ dari ∨s, dimana ∨ berada di atas variabel atau negasinya (literal); sebuah ∨ dari literal juga disebut klausa. DNF adalah ∨ dari ∧s; sebuah ∧ literal disebut istilah.
Inti dari proyek ini adalah mengekspresikan teka-teki zebra sebagai masalah Boolean satisfiability (SAT) (Wikipedia.
Masalah 3-SAT dikenal sebagai NP-complete . Artinya, mungkin tidak ada algoritma waktu polinomial untuk menyelesaikannya. Namun ini hanya menggambarkan kasus umum.
Masalah kita kecil dan spesifik (bagaimanapun juga, kita menciptakan masalah ini khusus untuk manusia!). Hal ini membuatnya sangat cocok untuk pemecah SAT modern, dan pembicaraan (dan catatan) Hettinger menunjukkan hal ini dengan indah.
