💫 🎅🏽 👨🏻‍🔬 सैट सॉल्वर के साथ जापानी वर्ग पहेली को हल करें 👩🏻‍🔬 👩🏿‍🎤 ♈️

Habré पर जापानी वर्ग पहेली को हल करने पर कई लेख थे, जहाँ लेखक इस तरह के वर्ग पहेली को हल करने के विभिन्न तरीकों के साथ आए थे। लेख की टिप्पणी में प्रकाश की गति के साथ जापानी रंग वर्ग पहेली को हल करते हुए, मैंने सुझाव दिया कि चूंकि जापानी वर्ग पहेली हल करना एक एनपी-पूर्ण समस्या है, इसलिए उन्हें उचित उपकरण का उपयोग करके हल किया जाना चाहिए, अर्थात् सैट सॉल्वर। चूंकि मेरा विचार संशयवाद से मिला था, इसलिए मैंने इसे लागू करने और अन्य दृष्टिकोणों के साथ परिणामों की तुलना करने का प्रयास करने का निर्णय लिया। इसके बारे में क्या पता कट के तहत मिल सकता है।

जैसा कि आप जानते हैं, एक जापानी क्रॉसवर्ड या नोमोग्राम एक तार्किक पहेली है जिसमें आपको कॉलम हेडर में ऊपर और नीचे पंक्ति हेडर में बाईं ओर स्थित संख्याओं का उपयोग करके एक आयत में छवि को पुनर्स्थापित करने की आवश्यकता होती है। ये संख्याएँ संबंधित पंक्ति या स्तंभ में क्रमिक रूप से भरे गए कोशिकाओं के ब्लॉक के क्रम और लंबाई के अनुरूप होती हैं, और ब्लॉक स्थापित करते समय, उनके बीच कम से कम एक खाली सेल होना चाहिए। यहां मैं केवल दो-रंग के क्रॉसवर्ड पर विचार करता हूं, जहां प्रत्येक कोशिका को या तो चित्रित किया जा सकता है या नहीं। वास्तव में, इस समस्या को हल करने के लिए, प्रत्येक ब्लॉक की स्थिति का पता लगाना आवश्यक है। यह ध्यान दिया जाना चाहिए कि एक कार्य में एक या कई समाधान हो सकते हैं, साथ ही साथ कोई भी समाधान नहीं हो सकता है। सॉल्वर को भी इसकी सूचना देनी होगी।

यह समझना आसान है कि सामान्य मामले में समस्या व्यापक है और कई अनुप्रयोगों के लेखक बूलियन संतोषजनक समस्या में उपयोग किए गए अच्छी तरह से विकसित तरीकों का उपयोग करने के बजाय, विभिन्न चाल के ~~अपने स्वयं के साइकिल लिखकर~~ सबसे तेज़ समाधान एल्गोरिदम खोजने की कोशिश करते हैं। हालाँकि, इस कथन के लिए प्रमाण की आवश्यकता है, इसलिए मैंने जापानी सामान्य पहेली को हल करने के लिए एक सामान्य रूप में हल करने की समस्या का सुधार करने का निर्णय लिया और इसे सुलझाने या पुष्टि करने के लिए प्रसिद्ध सैट सॉल्वरों में से एक का उपयोग किया।

सामान्य रूप से इस समस्या का प्रतिनिधित्व करने के लिए, हम फ़ील्ड में प्रत्येक सेल के लिए एक बूलियन चर और पंक्तियों और स्तंभों में प्रत्येक ब्लॉक की प्रत्येक संभावित स्थिति के लिए एक चर का परिचय देते हैं। बुलियन फ़ील्ड के सेल के लिए, एक वेरिएबल का मतलब होगा कि दी गई सेल रंगीन है या नहीं, और बुलियन ब्लॉक की स्थिति के लिए, एक वेरिएबल का मतलब होगा कि यह ब्लॉक इस स्थिति में मौजूद है या नहीं। हम चर (खंड) के बीच आवश्यक संबंध लिखते हैं:

1. पंक्ति या स्तंभ में घोषित प्रत्येक ब्लॉक कम से कम एक स्थिति में होना चाहिए। यह प्रपत्र (X1 V X2 V ... XN) के एक खंड से मेल खाती है, जहां X1, X2 ... XN एक पंक्ति या स्तंभ में इस ब्लॉक के सभी संभावित स्थान हैं।

2. एक पंक्ति या स्तंभ में प्रत्येक ब्लॉक एक से अधिक बार नहीं दिखाई देना चाहिए। यह प्रपत्र के कई खंड (ग्यारहवीं नहीं) वी (एक्सजे नहीं) से मेल खाती है, जहां शी, एक्सजे (i! = J) एक पंक्ति या स्तंभ में इस ब्लॉक के सभी संभावित स्थान हैं।

3. ब्लॉक का सही क्रम। चूंकि ब्लॉकों की व्यवस्था के सही क्रम को बनाए रखना आवश्यक है, साथ ही साथ उनके चौराहे को खत्म करने के लिए, प्रपत्र (न कि ग्यारहवीं) वी (एक्सजे नहीं) के खंड को जोड़ना आवश्यक है, जहां शी, एक्सजे विभिन्न ब्लॉकों के पदों के अनुरूप चर हैं जो गलत क्रम या प्रतिच्छेद हैं।

4. दाग वाली सेल कम से कम एक ब्लॉक में होनी चाहिए, जिसकी स्थिति में यह सेल शामिल हो। यह प्रपत्र ((Xk नहीं) V X1 V X2 ... XN) के एक खंड से मेल खाती है, जहां Xk सेल के अनुरूप चर है, और X1, X2 ... XN इस सेल के ब्लॉक के पदों के अनुरूप चर हैं।

5. प्रत्येक खाली सेल को किसी एक ब्लॉक की किसी भी संभावित स्थिति में समाहित नहीं किया जाना चाहिए। यह ज़ी वी (एक्सजे नहीं) फॉर्म के कई खंडों से मेल खाता है, जहां शी सेल के अनुरूप चर है, और एक्सजे इस सेल वाले किसी भी ब्लॉक की एक स्थिति के लिए चर है।

इस प्रकार, समस्या एक संयुग्मित रूप से सामान्य रूप में तैयार की जाती है और इसे सैट सॉल्वर का उपयोग करके हल किया जा सकता है। इसके अलावा, अगर कोई समाधान नहीं है, तो एसएटी सॉल्वर यह निर्धारित करेगा कि कोई समाधान नहीं है।

अब मेरी धारणा की पुष्टि या खंडन करने का समय आ गया है कि एसएटी सॉल्वर अन्य एल्गोरिदम की तुलना में जापानी वर्ग पहेली को सुलझाने में सामना करेगा। इसे सत्यापित करने के लिए, मैंने सर्वे ऑफ पेंट-बाय-नंबर पहेली सॉल्वर वेबसाइट से उदाहरण लिया। इस साइट पर जापानी वर्ग पहेली को हल करने के लिए विभिन्न अनुप्रयोगों की गति और उदाहरणों के एक अच्छे सेट की तुलना करने वाली एक तालिका है - सबसे हल्के से, जो सभी द्वारा हल की जाती है, जटिल लोगों के लिए, जो केवल एक आवेदन हल करता है। कंप्यूटर पर ये परिणाम 2.6GHz CPU AMD Phenom II X4 810 क्वाड-कोर 64-बिट प्रोसेसर मेमोरी: 8 Gb के साथ प्राप्त हुए थे। मैंने एक Intel® Core (TM) कंप्यूटर i7-2600K CPU @ 3.40GHz मेमोरी 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

इससे क्या निष्कर्ष निकाला जा सकता है?

सैट सॉल्वर ने उन सभी उदाहरणों को हल किया जो अन्य अनुप्रयोगों द्वारा हल किए गए हैं, यहां तक कि वेबपीएनबी -22336, जो केवल एक एप्लिकेशन द्वारा हल किया गया है।
सैट सॉल्वर आसानी से कई उदाहरणों को हल करता है जिन्हें अधिकांश अनुप्रयोगों द्वारा हल नहीं किया जा सकता है।
ज्यादातर मामलों में, समाधान का समय अन्य अनुप्रयोगों की तुलना में एसएटी सॉल्वर के लिए बेहतर है।
मैंने एक एकल-थ्रेडेड सैट सॉल्वर का उपयोग किया है, यदि आप एक बहु-थ्रेडेड सैट सॉल्वर का उपयोग करते हैं, तो परिणाम और भी बेहतर होंगे।
सैट सॉल्वर का उपयोग करते समय, अपने स्वयं के एल्गोरिदम का आविष्कार करने की आवश्यकता नहीं है, जो पहले से ही, उच्च संभावना के साथ, किसी ने आविष्कार किया।

निष्कर्ष में, हम यह जोड़ सकते हैं कि SAT समाधान एक से अधिक समाधान प्राप्त कर सकता है, यदि कोई हो। ऐसा करने के लिए, फॉर्म का एक क्लॉज जोड़ें ((एक्स 1 नहीं) वी (एक्स 2 नहीं) वी ... (एक्सएन नहीं)), जहां एक्स 1, एक्स 2 ... एक्सएन पिछले सॉल्यूशन में भरे हुए सेल के अनुरूप वैरिएबल हैं।

सैट सॉल्वर के साथ जापानी वर्ग पहेली को हल करें

More articles: