واليوم، في عام 2024، أصبح المشروع غير خاضع للصيانة إلى حد كبير. أنا أستخدمه كملعب لبعض الأشياء التي أرغب في تجربتها، لكنني لا أنصح أي شخص ببناء هذا.
هل تتذكر الألغاز المنطقية التي تبدو هكذا؟ كان لديهم أدلة مثل:
هناك منزل واحد بين توشار وماوي.
لعبة الفيديو المفضلة لدى روبي هي بوكيمون.
شارب الشاي لا يحب اللون الأزرق.
لقد أحببت هذه المشكلات عندما كنت طفلاً، وألهمتني مشاهدة حديث ريموند هيتنجر في PyCon 2019 بإعادة النظر في هذه المشكلات. لقد أظهر لنا كيفية حلها؛ أردت أن أتعلم كيفية توليدها.
باستخدام أدوات حل بايثون الحديثة ورضا القيد (SAT)، يمكن استخدام هذا المشروع لإنشاء ألغاز حمار وحشي عشوائية.
يستخدم هذا المشروع Python 3.12 والشعر.
نقطة الدخول لهذا المشروع هي src/main.py
; وفقًا لذلك، قم بتشغيله باستخدام [poetry run] python -m src.main
. نحن نستخدم الاستبيان لإنشاء واجهة سطر الأوامر (CLI) مع تفاعل بسيط.
ومن الملفات الهامة الأخرى:
يحتوي puzzle.py
على فئة الألغاز الرئيسية، والتي يتم لصقها في الغالب حول القرائن وعناصر اللغز
يحدد clues.py
الدليل (عبارة ذات مستوى أعلى يمكننا تحويلها إلى CNF) والعديد من المصانع، مثل found_at
أو same_house
؛ لدى generate.py
أدوات مساعدة لإنشاء القرائن
لدى elements.py
و traptor_elements.py
عناصر ألغاز مختلفة
وأخيرًا، يحتوي sat_utils.py
على الأدوات المساعدة الأساسية للتفاعل مع pycosat الذي يحلل SAT. تمت كتابة هذا الرمز بالكامل تقريبًا بواسطة ريموند هيتينجر في محاضرته لعام 2019 (شكرًا لك!).
❯ تشغيل الشعر بيثون -m src.main؟ ما هو حجم اللغز؟ (استخدم مفاتيح الأسهم) » 5 4 3؟ اختر نوع Traptor (استخدم مفاتيح الأسهم) ؟ استوائي » ؟ أسطوري؟ ؟ هل يجب أن يتضمن اللغز العصائر؟ (استخدم مفاتيح الأسهم) " نعم لا؟ ؟ هل يجب أن يتضمن اللغز أغطية الزجاجات؟ (استخدم مفاتيح الأسهم) " نعم لا القرائن -----# ... تم حذف بعض نص النكهة ...1. يوجد The Lesser Traptor وSwamp Traptor في نفس المنزل. 2. الصياد القديم موجود مباشرة على يسار عصير الشوكولاتة. 3. الصياد القديم وعصير الليمون موجودان في نفس المنزل. 4. يقع Volcano Traptor مباشرة على يسار Restless Traptor. 5. صائد الكهف وأغطية الزجاجات الخضراء موجودان في نفس المنزل. 6. يوجد منزلان بين بحيرة ترابتور وسمك النهاش. 7. توجد أغطية الزجاجات الخضراء والصياد الشرس في نفس المنزل. 8. هناك منزل واحد بين أغطية الزجاجات السوداء وعصير جوز الهند. 9. هناك منزل واحد بين الصياد الصغير وعصير الكيوي. 10. يتواجد The Dweller Traptor وعصير الشوكولاتة في نفس المنزل. 11. أغطية الزجاجات الحمراء وDweller Traptor موجودان في نفس المنزل. 12. أغطية الزجاجات الحمراء موجودة مباشرة على يسار Hoarder Traptor. 13. هناك منزلان بين عصير Starfruit وأغطية الزجاجات الصفراء. 14. بحيرة Traptor وأغطية الزجاجات السوداء موجودان في نفس المنزل. 15. الصياد المطارد والصياد الشرس موجودان في نفس المنزل. حل ┏━━━━━━┳━━━━━━━━━━━━━━━━━━━━━━ ┳━━━━━━━━━━━━━━━━━━━━━━━━┳━━━━━ ━━━━━━━━━━━━━━━━━━┳━━━━━━━━━━━━ ━━━━━━━━━━┳━━━━━━━━━━━━━━━━┓ ┃ Nest ┃ MythicalTraptorPrimary ┃ MythicalTraptorSecondary ┃ MythicalTraptorTertiary ┃ عصير ┃ غطاء زجاجة ┃ ┡━━━━━━╇━━━━━━━━━━━━━━━━━━━━━━ ╇━━━━━━━━━━━━━━━━━━━━━━━━╇━━━━━ ━━━━━━━━━━━━━━━━━━╇━━━━━━━━━━━━ ━━━━━━━━━━━━╇━━━━━━━━━━━━━━━━┩ │ 1 │ الفخ الشرس │ صائد الكهف │ الفخ المطارد │ عصير ستارفروت │ أغطية الزجاجات الخضراء │ │ 2 │ الصياد القديم │ بحيرة Traptor │ الصياد الزاحف │ عصير الليمون │ أغطية الزجاجات السوداء │ │ 3 │ الفخاخ الصغرى │ الفخاخ المستنقع │ الفخ الساكن │ عصير الشوكولاتة │ أغطية الزجاجات الحمراء │ │ 4 │ الصياد الأكبر │ الصياد البركاني │ الصياد المكتنز │ عصير جوز الهند │ أغطية الزجاجات الصفراء │ │ 5 │ The Restless Traptor │ Mountain Traptor │ Snapper Traptor │ عصير الكيوي │ أغطية الزجاجات الزرقاء │ └──────┴────────────────────── ┴─────────────────────────── ──────────────────┴──────────── ────────────┴──────────────┘
في فبراير 2024، ما الذي أحتاجه لأعتبر أن هذا "تم"؟
أضف قوالب HTML، لأن الموقع الذي أقوم بإنشاء هذه القوالب من أجله يتطلب تضمين أشياء مثل علامات BR.
قم بتحسين القواعد النحوية في الإخراج، مثل الكتابة بالأحرف الكبيرة في نص النكهة.
قم بإضافة موارد الرأس/التذييل التي قمت بنسخها/لصقها في الإرسال.
ربما، يومًا ما، سأفكر في واجهة الويب. هل يمكنني رفع المشروع باستخدام البيوديد، أم أن البيكوسات المعتمد على C سيسبب مشاكل؟ ماذا عن واجهة برمجة منطقية أخرى، مثل PySAT، أو برمجة مجموعة الإجابات، أو غيرها من سلسلة HN هذه؟
قد تحدث هذه. لكن المشروع وصل أخيرًا إلى مكان يسعدني، ولذلك فأنا متحمس لمشاركته والكتابة عنه.
2/18: جعل المخرجات أبسط، وأقل إسهابًا، وأجمل. قم بتحديث الملف التمهيدي هذا بتنسيق وتغييرات جديدة. استخدم مولد الألغاز لإنشاء لغز جديد أخيرًا!
2/17: تحديث توقيع اللغز لقبول الحل فقط واستنتاج العناصر وفئات العناصر منه. أضف عرضًا أجمل للحل.
26/11: تنظيف منطق توليد اللغز/الحل. اسمح للمستخدم باختيار حجم اللغز.
25/11: قم بتسمية بعض الأنواع الشائعة كأسماء مستعارة للنوع (شكرًا، Python 3.12). استخدم التسجيل بدلاً من المطبوعات.
أضف اختبارات لأنواع الأدلة داخل generate.py
.
أصلح الخلل الذي قدمته في clues.py
. من الصعب جدًا فهم هذا الملف، ولكن من الصعب أيضًا كتابة اختبارات الوحدة له؛ تحويل التعبيرات المنطقية إلى CNF يدويًا ليس أمرًا ممتعًا.
ضبط أوزان القرائن في الحل. الاستعداد لدمج فصول اللغز والحل.
قم بإزالة تحديد Smoothie الذي يشبه خانة الاختيار، لأنه يعيق الطريق عند محاولة إنشاء الألغاز بسرعة.
استمر في إضافة الاختبارات. قم بإنهاء اختبارات الوحدة لـ sat_utils.py
وابدأ اثنين من clues.py
، على الرغم من صعوبة اختبار هذا الملف نظرًا لصعوبة إجراء عمليات حسابية يدوية لتحويلات DNF-to-CNF.
الخطوات التالية هي توحيد اللغز والحل، وإنشاء __repr__
أفضل، وتبسيط كيفية تمثيل حجم اللغز (السمة في Puzzle
، مجموعة ints من 1 إلى N، فقط الرقم n_houses
، وما إلى ذلك).
إزالة اللون الأسود واستخدام راف للتنسيق. تحديث التبعيات. أضف واجهة سطر الأوامر (CLI) جديدة باستخدام أبسط وأكثر وضوحًا؛ python -m src.main
.
إعادة تسمية SATLiteral
-> PuzzleElement
(عصير، قطة، وما إلى ذلك)؛ يوضح هذا أنه ليس حرفيًا بالمعنى المنطقي، بل هو اسم لشخصيات في اللغز على سبيل المثال.
قم بإنشاء نوع جديد SATLiteral
(وهو عبارة عن str
في معطف واقٍ من المطر)؛ وهذا يمثل الحرفي بالمعنى المتغير المنطقي، مثل "Value el is at house loc " أو "Value el is not at house loc ." داخليًا، يتم تمثيلها بعدد صحيح i ونظيره السلبي -i .
استخدم (الجديد) SATLiteral
كنوع الإرجاع comb(el: str, loc: int) -> SATLiteral
، ورسم عناصر اللغز إلى قيم حرفية، و neg(el: SATLiteral) -> SATLiteral
لإلغاء حرفي.
إضافة Clause: tuple[SATLiteral, ...]
يمثل "∨" (منطقية OR؛ انفصال) للأحرف الحرفية؛ على سبيل المثال، (1, -5, 6)
عبارة عن انفصال يوضح أن x_1
صحيح، أو x_5
غير صحيح، أو x_6
صحيح.
أضف ClueCNF: list[Clause]
، الذي يمثل "∧" (منطقي AND؛ اقتران) Clause
s. اللغز في CNF هو "AND of ORs" ("∧ of ∨s" أو "∧ of Clauses").
طباعة اللغز بشكل أكثر وضوحا. تقليل إسهاب الحد من فكرة.
قم بإنشاء اللغز بشكل عشوائي (ببذور) في كل جولة.
نقل الأمثلة إلى ملفاتهم الخاصة. التحديث إلى بايثون 3.12 (بيتا). إضافة المزيد من قواعد الوبر. تنظيف الواردات.
إضافة أدوات التطوير (أسود، راف، بيرايت)؛ قم بتشغيل Black & Ruff في الالتزام المسبق. تحديث بعض الأنواع.
"∧" هو المنطقي AND
"∨" هو OR المنطقي
الشرط هو "∨ من الحروف"
CNF هو "∧ من البنود،" أو ما يعادل "∧ من ∨s" ("AND of ORs")
في المقابل، فإن DNF هو "∨ من ∧s." DNF هو الحل لمشكلة SAT؛ يقرأ DNF لـ "A أو B أو C" أن A وB وC كلها تعيينات صالحة (مرضية). وبالتالي فإن تحويل CNF إلى DNF هو أمر صعب NP، لأنه من DNF يمكنك قراءة الحلول إلى CNF.
CNF هو ∧ من ∨s، حيث ∨ فوق المتغيرات أو نفيها (الأحرف الحرفية)؛ يُطلق على ∨ من الأحرف الحرفية أيضًا اسم الجملة. DNF هو ∨ من ∧s؛ يُطلق على ∧ من الأحرف الحرفية مصطلح.
جوهر هذا المشروع هو التعبير عن لغز الحمار الوحشي باعتباره مشكلة الإشباع المنطقي (SAT) (ويكيبيديا.
من المعروف أن مشكلة 3-SAT هي NP-Complete . وهذا يعني أنه ربما لا توجد خوارزمية متعددة الحدود لحلها. هذا يصف الحالة العامة فقط.
مشكلتنا صغيرة ومحددة جيدًا (بعد كل شيء، نحن نصنعها خصيصًا للبشر!). وهذا يجعله مناسبًا بشكل ممتاز لمحللي اختبارات SAT الحديثة، ويوضح حديث Hettinger (وملاحظاته) هذا بشكل جميل.