في Habré ، كانت هناك عدة مقالات حول حل الكلمات المتقاطعة اليابانية ، حيث توصل المؤلفون إلى طرق مختلفة لكيفية حل هذه الكلمات المتقاطعة. في التعليق على المقال
حل الكلمات المتقاطعة اليابانية بسرعة الضوء ، اقترحت أنه بما أن حل الكلمات المتقاطعة اليابانية يمثل مشكلة في NP كاملة ، فيجب حلها باستخدام الأداة المناسبة ، وهي SAT حلالا. منذ أن قوبلت فكي بالشك ، قررت أن أحاول تنفيذها ومقارنة النتائج مع الأساليب الأخرى. ما جاء من هذا يمكن العثور عليها تحت خفض.
كما تعلمون ، الكلمات المتقاطعة اليابانية أو الرسوم البيانية هي لغز منطقي تحتاج فيه إلى استعادة الصورة في مستطيل باستخدام الأرقام الموجودة على اليسار في رؤوس الصفوف وفوق ذلك في رؤوس الأعمدة. تتوافق هذه الأرقام مع ترتيب وطول كتل الخلايا المملوءة على التوالي في الصف أو العمود المقابل ، وعند تثبيت الكتل ، يجب أن يكون هناك خلية فارغة واحدة على الأقل بينها. أنا هنا أعتبر الكلمات المتقاطعة ذات اللونين فقط ، حيث يمكن طلاء كل خلية أو لا. في الواقع ، لحل هذه المشكلة ، فمن الضروري العثور على موقف كل كتلة. تجدر الإشارة إلى أن المهمة يمكن أن يكون لها حل واحد أو عدة حلول ، فضلاً عن عدم وجود حلول على الإطلاق. يجب على Solver أيضًا الإبلاغ عن هذا.
من السهل أن نفهم أن المشكلة شاملة بشكل عام وأن مؤلفي العديد من التطبيقات يحاولون العثور على أسرع خوارزمية للحل عن طريق
كتابة الدراجات الخاصة بهم من الحيل المختلفة ، بدلاً من استخدام الطرق المطورة جيدًا المستخدمة في مشكلة الثبات المنطقي. ومع ذلك ، فإن هذا البيان يتطلب دليلًا ، لذلك قررت إعادة صياغة مشكلة حل لغز الكلمات المتقاطعة اليابانية بشكل طبيعي متواصل واستخدام أحد حل SAT المعروف لحلها لتأكيدها أو دحضها.
لتمثيل هذه المشكلة في شكل طبيعي مترابط ، نقدم متغير منطقي واحد لكل خلية في الحقل ومتغير واحد لكل موضع محتمل لكل كتلة في الصفوف والأعمدة. بالنسبة لخلية حقل Boolean ، يعني المتغير ما إذا كانت خلية معينة ملونة أم لا ، وبالنسبة لموضع كتلة Boolean ، سيعني المتغير ما إذا كانت هذه الكتلة موجودة في هذا الموضع أم لا. نكتب العلاقات اللازمة بين المتغيرات (الجمل):
1. يجب أن تظهر كل كتلة تم إعلانها في صف أو عمود في موضع واحد على الأقل. هذا يتوافق مع فقرة من النموذج (X1 V X2 V ... XN) ، حيث X1 ، X2 ... XN كلها مواضع محتملة لهذه الكتلة في صف أو عمود.
2. يجب ألا يظهر كل كتلة في صف أو عمود أكثر من مرة. هذا يتوافق مع العديد من جمل النموذج (وليس Xi) V (وليس Xj) ، حيث Xi و Xj (i! = J) كلها مواضع محتملة لهذه الكتلة في صف أو عمود.
3. الترتيب الصحيح للكتل. نظرًا لأنه من الضروري الحفاظ على الترتيب الصحيح لترتيب الكتل ، وكذلك لإزالة تقاطعها ، من الضروري إضافة جمل من النموذج (وليس Xi) V (وليس Xj) ، حيث Xi ، Xj هي متغيرات متوافقة مع مواضع الكتل المختلفة التي لها ترتيب خاطئ أو تتقاطع.
4. يجب أن تحتوي الخلية الملطخة على كتلة واحدة على الأقل يشتمل موضعها على هذه الخلية. هذا يتوافق مع فقرة من النموذج ((وليس Xk) V X1 V X2 ... XN) ، حيث Xk هو المتغير المقابل للخلية ، و X1 ، X2 ... XN هي المتغيرات المقابلة لمواقع الكتل التي تحتوي على هذه الخلية.
5. لا ينبغي أن تحتوي كل خلية فارغة في أي موقف ممكن من كتلة واحدة. هذا يتوافق مع العديد من جمل النموذج Xi V (وليس Xj) ، حيث Xi هو المتغير المقابل للخلية ، و Xj هو المتغير المقابل لموضع واحد لأي كتلة تحتوي على هذه الخلية.
وبالتالي ، يتم صياغة المشكلة في شكل نموذج طبيعي ملتحمة ويمكن حلها باستخدام SAT حلالا. علاوة على ذلك ، إذا لم يكن هناك حل ، فإن محلل SAT سيحدد أنه لا يوجد حل.
لقد حان الوقت الآن لتأكيد أو دحض افتراضاتي بأن SAT حلالا سيتعامل مع حل الكلمات المتقاطعة اليابانية بشكل أسرع من الخوارزميات الأخرى. للتحقق من ذلك ، أخذت أمثلة من موقع
Survey of Paint-by-Number Puzzle Solvers . يوجد في هذا الموقع جدول يقارن سرعة التطبيقات المختلفة لحل الكلمات المتقاطعة اليابانية ومجموعة جيدة من الأمثلة - من الأخف وزناً ، التي يحلها الجميع ، إلى تلك المعقدة ، والتي لا يحلها سوى تطبيق واحد. تم الحصول على هذه النتائج على جهاز كمبيوتر مزود بمعالج AMD Phenom II X4 810 رباعي النواة بسرعة 2.6 جيجا هرتز ، ذاكرة: 8 جيجا بايت. استخدمت جهاز كمبيوتر Intel® Core (TM) i7-2600K CPU @ 3.40GHz Memory 16 Gb.
نتيجة لذلك ، حصلت على النتائج التالية:
======== sample-nin/webpbn-00001.nin ======== Start read data. 16 lines were read Solver started. vars = 150 Clauses = 562 SATISFIABLE apsnono finished. real 0m0,610s user 0m0,004s sys 0m0,002s ========= sample-nin/webpbn-00006.nin ======== Start read data. 41 lines were read Solver started. vars = 1168 Clauses = 10215 SATISFIABLE apsnono finished. real 0m0,053s user 0m0,028s sys 0m0,000s ========= sample-nin/webpbn-00016.nin ======== Start read data. 69 lines were read Solver started. vars = 7484 Clauses = 191564 SATISFIABLE apsnono finished. real 0m0,368s user 0m0,186s sys 0m0,008s ========= sample-nin/webpbn-00021.nin ======== Start read data. 40 lines were read Solver started. vars = 1240 Clauses = 11481 SATISFIABLE apsnono finished. real 0m0,095s user 0m0,034s sys 0m0,000s ========= sample-nin/webpbn-00023.nin ======== Start read data. 22 lines were read Solver started. vars = 311 Clauses = 1498 SATISFIABLE apsnono finished. real 0m0,147s user 0m0,006s sys 0m0,000s ========= sample-nin/webpbn-00027.nin ======== Start read data. 51 lines were read Solver started. vars = 2958 Clauses = 38258 SATISFIABLE apsnono finished. real 0m0,089s user 0m0,050s sys 0m0,010s ========= sample-nin/webpbn-00065.nin ======== Start read data. 75 lines were read Solver started. vars = 7452 Clauses = 134010 SATISFIABLE apsnono finished. real 0m0,272s user 0m0,166s sys 0m0,009s ========= sample-nin/webpbn-00436.nin ======== Start read data. 76 lines were read Solver started. vars = 6900 Clauses = 134480 SATISFIABLE apsnono finished. real 0m0,917s user 0m0,830s sys 0m0,005s ========= sample-nin/webpbn-00529.nin ======== Start read data. 91 lines were read Solver started. vars = 10487 Clauses = 226237 SATISFIABLE apsnono finished. real 0m0,286s user 0m0,169s sys 0m0,005s ========= sample-nin/webpbn-00803.nin ======== Start read data. 96 lines were read Solver started. vars = 9838 Clauses = 278533 SATISFIABLE apsnono finished. real 0m0,827s user 0m0,697s sys 0m0,008s ========= sample-nin/webpbn-01611.nin ======== Start read data. 116 lines were read Solver started. vars = 25004 Clauses = 921246 SATISFIABLE apsnono finished. real 0m3,467s user 0m3,301s sys 0m0,084s ========= sample-nin/webpbn-01694.nin ======== Start read data. 96 lines were read Solver started. vars = 13264 Clauses = 391427 SATISFIABLE apsnono finished. real 0m0,964s user 0m0,822s sys 0m0,016s ========= sample-nin/webpbn-02040.nin ======== Start read data. 116 lines were read Solver started. vars = 26445 Clauses = 1182535 SATISFIABLE apsnono finished. real 0m7,512s user 0m7,354s sys 0m0,122s ========= sample-nin/webpbn-02413.nin ======== Start read data. 41 lines were read Solver started. vars = 1682 Clauses = 15032 SATISFIABLE apsnono finished. real 0m0,258s user 0m0,053s sys 0m0,001s ========= sample-nin/webpbn-02556.nin ======== Start read data. 111 lines were read Solver started. vars = 11041 Clauses = 340630 SATISFIABLE apsnono finished. real 0m0,330s user 0m0,136s sys 0m0,009s ========= sample-nin/webpbn-02712.nin ======== Start read data. 95 lines were read Solver started. vars = 13212 Clauses = 364416 SATISFIABLE apsnono finished. real 0m6,503s user 0m6,365s sys 0m0,032s ========= sample-nin/webpbn-03541.nin ======== Start read data. 111 lines were read Solver started. vars = 19249 Clauses = 676595 SATISFIABLE apsnono finished. real 0m5,008s user 0m4,785s sys 0m0,100s ========= sample-nin/webpbn-04645.nin ======== Start read data. 121 lines were read Solver started. vars = 19159 Clauses = 793580 SATISFIABLE apsnono finished. real 0m4,739s user 0m4,477s sys 0m0,107s ========= sample-nin/webpbn-06574.nin ======== Start read data. 51 lines were read Solver started. vars = 2932 Clauses = 33191 SATISFIABLE apsnono finished. real 0m0,231s user 0m0,176s sys 0m0,000s ========= sample-nin/webpbn-06739.nin ======== Start read data. 81 lines were read Solver started. vars = 10900 Clauses = 256833 SATISFIABLE apsnono finished. real 0m0,782s user 0m0,730s sys 0m0,008s ========= sample-nin/webpbn-07604.nin ======== Start read data. 111 lines were read Solver started. vars = 18296 Clauses = 478535 SATISFIABLE apsnono finished. real 0m1,524s user 0m1,324s sys 0m0,026s ========= sample-nin/webpbn-08098.nin ======== Start read data. 39 lines were read Solver started. vars = 1255 Clauses = 10950 SATISFIABLE apsnono finished. real 0m0,216s user 0m0,133s sys 0m0,000s ========= sample-nin/webpbn-09892.nin ======== Start read data. 91 lines were read Solver started. vars = 13887 Clauses = 419787 SATISFIABLE apsnono finished. real 0m12,048s user 0m11,858s sys 0m0,088s ========= sample-nin/webpbn-10088.nin ======== Start read data. 116 lines were read Solver started. vars = 23483 Clauses = 1020515 SATISFIABLE apsnono finished. real 0m17,472s user 0m16,795s sys 0m0,321s ========= sample-nin/webpbn-10810.nin ======== Start read data. 121 lines were read Solver started. vars = 25726 Clauses = 895436 SATISFIABLE apsnono finished. real 0m0,898s user 0m0,562s sys 0m0,026s ========= sample-nin/webpbn-12548.nin ======== Start read data. 88 lines were read Solver started. vars = 13685 Clauses = 486012 SATISFIABLE apsnono finished. real 3m1,682s user 2m58,537s sys 0m1,507s ========= sample-nin/webpbn-18297.nin ======== Start read data. 79 lines were read Solver started. vars = 9708 Clauses = 272394 SATISFIABLE apsnono finished. real 0m16,643s user 0m16,326s sys 0m0,210s ========= sample-nin/webpbn-22336.nin ======== Start read data. 159 lines were read Solver started. vars = 67137 Clauses = 5420886 SATISFIABLE apsnono finished. real 1m46,555s user 1m43,336s sys 0m3,075s
ما هي الاستنتاجات التي يمكن استخلاصها من هذا؟
- حل SAT حلالاً جميع الأمثلة التي تم حلها بواسطة التطبيقات الأخرى ، حتى webpbn-22336 ، والتي تم حلها من خلال تطبيق واحد فقط.
- SAT حلالا يحل بسهولة العديد من الأمثلة التي لا يمكن حلها من قبل معظم التطبيقات.
- في معظم الحالات ، يكون وقت الحل بالنسبة لمحلل SAT أفضل من التطبيقات الأخرى.
- لقد استخدمت حلالاً SAT فردي الخيوط ، إذا كنت تستخدم حلال SAT متعدد الخيوط ، فستكون النتائج أفضل.
- عند استخدام SAT حلالا ، ليست هناك حاجة لاختراع الخوارزميات الخاصة بك ، والتي بالفعل ، مع وجود احتمال كبير ، اخترع شخص ما.
في الختام ، يمكننا إضافة أن محلل SAT يمكنه تلقي أكثر من حل واحد ، إن وجد. للقيام بذلك ، قم بإضافة جملة واحدة من النموذج ((وليس X1) V (وليس X2) V ... (وليس XN)) ، حيث X1 و X2 ... XN هي المتغيرات المقابلة للخلايا المعبأة في الحل السابق.