يتكون هذا المشروع من حل لغز بينايرو (انظر هنا لعبة على الإنترنت)، وتسمى أيضًا تاكوزو، ويتم وصفها على النحو التالي. لدينا شبكة من خلايا nxn التي قد تحتوي على دائرة بيضاء أو دائرة سوداء. يوفر التكوين الأولي بعض قيم الخلايا ويجب ملء الباقي بالدوائر وفقًا للقواعد التالية:
يجب أن يحتوي كل صف وكل عمود على نفس عدد الدوائر من كل لون، أي عدد n/2 من كل حالة.
لا يمكن أن يكون هناك أكثر من دائرتين متتاليتين من نفس اللون في أي اتجاه (عمودي أو أفقي).
لا يمكن أن يكون هناك صفين أو عمودين بنفس التكوين.
يمكن الاطلاع على مثال للتكوين الأولي والحل المقابل أدناه.
سيقوم بترميز السيناريو كمشكلة SAT وكبرنامج ASP.
يأخذ هذا ملف ASCII مع الشبكة الأولية حيث تحتوي كل خلية على حرف: '0' (دائرة بيضاء)، '1' (دائرة سوداء) أو '.' (خلية فارغة ليتم ملؤها). يحتوي السطر الأول على رقم زوجي n>=2 يحدد عدد الصفوف والأعمدة (لدينا شبكة مربعة). على سبيل المثال، المثال في الصورة أعلاه سيتم تمثيله على النحو التالي:
6
......
.11.0.
01....
....00
.1....
0..1..
سيقوم هذا البرنامج بإنشاء ملف DIMACS وإجراء مكالمة خارجية للقفل عندما يستخدم SAT أو clingo عندما يستخدم ASP للحصول على حل. سيقوم أيضًا بفك تشفير الإخراج الخلفي وطباعة الحل الكامل على النحو التالي:
100110
011001
010011
101100
110010
001101
افتراضيًا، يستخدم ASP ويحتوي مجلد الأمثلة على مجموعة من المعايير ذات الأحجام المختلفة (6، 8، 10، 14، 20)، حيث يكون domX.txt هو ملف الإدخال وsolX.txt هو الحل المقابل له.
./binairo.py [-h] [-a] [-c input] input
-h show this help message and exit
-a use ASP to solve
-c compare the result with this file
-input route of the binairo puzzle instance