सैट सॉल्वर: Difference between revisions

From Vigyanwiki
No edit summary
No edit summary
Line 2: Line 2:
[[कंप्यूटर विज्ञान]] एवं फॉर्मल मेथड्स में, '''सैट सॉल्वर''' [[कंप्यूटर प्रोग्राम]] है जिसका उद्देश्य बूलियन [[संतुष्टि|सेटिस्फिअबिलिटी प्रॉब्लम]] को सॉल्व करना है। [[बूलियन डेटा प्रकार|बूलियन डेटा टाइप]] वेरिएबल, जैसे (''x'' या ''y'') एवं (''x'' या ''y'' नहीं) पर फार्मूला इनपुट करने पर, सैट सॉल्वर आउटपुट देता है कि क्या फार्मूला सेटिसफीएबल है, जिसका अर्थ है कि ''x'' एवं ''y'' की पॉसिबल वैल्यूज हैं जो फॉर्मूले को ट्रू या अनसेटिसफीएबल बनाती हैं, जिसका अर्थ है कि ''x'' एवं ''y'' की ऐसी कोई वैल्यूज नहीं हैं। इस विषय में, ''x'' ट्रू होने पर फार्मूला सेटिसफीएबल होता है, इसलिए सॉल्वर को सेटिसफीएबल रिटर्न करना चाहिए। 1960 के दशक में सैट के लिए [[कलन विधि|एल्गोरिदम]] के प्रारम्भ के पश्चात से, आधुनिक सैट सॉल्वर कुशलतापूर्वक कार्य करने के लिए अधिक संख्या में हयूरिस्टिक्स एवं प्रोग्राम ऑप्टिमाइजेशन को सम्मिलित करते हुए काम्प्लेक्स [[सॉफ़्टवेयर]] आर्टिफैक्ट्स में विकसित हो गए हैं।
[[कंप्यूटर विज्ञान]] एवं फॉर्मल मेथड्स में, '''सैट सॉल्वर''' [[कंप्यूटर प्रोग्राम]] है जिसका उद्देश्य बूलियन [[संतुष्टि|सेटिस्फिअबिलिटी प्रॉब्लम]] को सॉल्व करना है। [[बूलियन डेटा प्रकार|बूलियन डेटा टाइप]] वेरिएबल, जैसे (''x'' या ''y'') एवं (''x'' या ''y'' नहीं) पर फार्मूला इनपुट करने पर, सैट सॉल्वर आउटपुट देता है कि क्या फार्मूला सेटिसफीएबल है, जिसका अर्थ है कि ''x'' एवं ''y'' की पॉसिबल वैल्यूज हैं जो फॉर्मूले को ट्रू या अनसेटिसफीएबल बनाती हैं, जिसका अर्थ है कि ''x'' एवं ''y'' की ऐसी कोई वैल्यूज नहीं हैं। इस विषय में, ''x'' ट्रू होने पर फार्मूला सेटिसफीएबल होता है, इसलिए सॉल्वर को सेटिसफीएबल रिटर्न करना चाहिए। 1960 के दशक में सैट के लिए [[कलन विधि|एल्गोरिदम]] के प्रारम्भ के पश्चात से, आधुनिक सैट सॉल्वर कुशलतापूर्वक कार्य करने के लिए अधिक संख्या में हयूरिस्टिक्स एवं प्रोग्राम ऑप्टिमाइजेशन को सम्मिलित करते हुए काम्प्लेक्स [[सॉफ़्टवेयर]] आर्टिफैक्ट्स में विकसित हो गए हैं।


कुक-लेविन थ्योरम के रूप में जाने जाने वाले परिणाम के अनुसार, बूलियन सटिस्फाबिलिटी सामान्य रूप से एनपी-पूर्ण समस्या है। परिणामस्वरूप, केवल घातीय वर्स्ट केस कम्प्लेक्सिटी एल्गोरिदम ही ज्ञात हैं। इसके अतिरिक्त, 2000 के दशक के समय सैट के लिए एफिशिएंट एवं स्केलेबल एल्गोरिदम विकसित किए गए, जिन्होंने हजारों वेरिएबल एवं लाखों बाधाओं से जुड़े समस्या उदाहरणों को स्वचालित रूप से निवारण करने की क्षमता में आकस्मिक प्रगति में योगदान दिया है।<ref name="Codish.Ohrimenko.Stuckey.2007">{{citation|title=Principles and Practice of Constraint Programming – CP 2007|series=Lecture Notes in Computer Science|volume=4741|year=2007|pages=544–558|contribution=Propagation = Lazy Clause Generation|first1=Olga|last1=Ohrimenko|first2=Peter J.|last2=Stuckey|first3=Michael|last3=Codish|doi=10.1007/978-3-540-74970-7_39|quote=modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables|citeseerx=10.1.1.70.5471}}</ref> सैट सॉल्वर प्रायः फार्मूला को [[संयोजक सामान्य रूप|कंजेक्टिव नॉरमल फॉर्म]] में परिवर्तित करके प्रारम्भ करते हैं। वे प्रायः [[डीपीएलएल एल्गोरिदम]] जैसे कोर एल्गोरिदम पर आधारित होते हैं, किन्तु इसमें कई एक्सटेंशन एवं सुविधाएं सम्मिलित होती हैं। अधिकांश सैट सॉल्वरों में टाइम-आउट सम्मिलित होता है, इसलिए वे करेक्ट समय में समाप्त हो जाएंगे, अपितु वे "अननोन" जैसे आउटपुट के साथ समाधान प्राप्त नहीं कर सकते है। प्रायः, सैट सॉल्वर केवल उत्तर ही नहीं देते हैं, अपितु यदि फॉर्मूला सटिसफाईइंग है तो उदाहरण असाइनमेंट (x, y, आदि के लिए मान) या फॉर्मूला असंतोषजनक होने पर असंतोषजनक क्लॉसेस का न्यूनतम सेट सहित अधिक जानकारी प्रदान कर सकते हैं।
कुक-लेविन थ्योरम के रूप में जाने जाने वाले परिणाम के अनुसार, बूलियन सटिस्फाबिलिटी सामान्य रूप से एनपी-पूर्ण समस्या है। परिणामस्वरूप, केवल घातीय वर्स्ट केस कम्प्लेक्सिटी एल्गोरिदम ही ज्ञात हैं। इसके अतिरिक्त, 2000 के दशक के समय सैट के लिए एफिशिएंट एवं स्केलेबल एल्गोरिदम विकसित किए गए, जिन्होंने हजारों वेरिएबल एवं लाखों बाधाओं से जुड़े समस्या उदाहरणों को स्वचालित रूप से सॉल्व करने की क्षमता में आकस्मिक प्रगति में योगदान दिया है।<ref name="Codish.Ohrimenko.Stuckey.2007">{{citation|title=Principles and Practice of Constraint Programming – CP 2007|series=Lecture Notes in Computer Science|volume=4741|year=2007|pages=544–558|contribution=Propagation = Lazy Clause Generation|first1=Olga|last1=Ohrimenko|first2=Peter J.|last2=Stuckey|first3=Michael|last3=Codish|doi=10.1007/978-3-540-74970-7_39|quote=modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables|citeseerx=10.1.1.70.5471}}</ref> सैट सॉल्वर प्रायः फार्मूला को [[संयोजक सामान्य रूप|कंजेक्टिव नॉरमल फॉर्म]] में परिवर्तित करके प्रारम्भ करते हैं। वे प्रायः [[डीपीएलएल एल्गोरिदम]] जैसे कोर एल्गोरिदम पर आधारित होते हैं, किन्तु इसमें कई एक्सटेंशन एवं सुविधाएं सम्मिलित होती हैं। अधिकांश सैट सॉल्वरों में टाइम-आउट सम्मिलित होता है, इसलिए वे ट्रू समय में समाप्त हो जाएंगे, अपितु वे "अननोन" जैसे आउटपुट के साथ समाधान प्राप्त नहीं कर सकते है। प्रायः, सैट सॉल्वर केवल उत्तर ही नहीं देते हैं, अपितु यदि फॉर्मूला सटिसफाईइंग है तो उदाहरण असाइनमेंट (x, y, आदि के लिए मान) या फॉर्मूला असंतोषजनक होने पर असंतोषजनक क्लॉसेस का न्यूनतम सेट सहित अधिक जानकारी प्रदान कर सकते हैं।


आधुनिक सैट सॉल्वरों का [[सॉफ़्टवेयर सत्यापन|सॉफ़्टवेयर वेरिफिकेशन]], प्रोग्राम एनालिसिस, [[बाधा संतुष्टि समस्या|कन्सट्रैन्ट सॉल्विंग]], आर्टिफिशियल इंटेलिजेंस, [[इलेक्ट्रॉनिक डिजाइन स्वचालन|इलेक्ट्रॉनिक डिजाइन ऑटोमेशन]]  एवं ऑपरेशन रिसर्च सहित क्षेत्रों पर महत्वपूर्ण प्रभाव पड़ा है। पावरफुल सॉल्वर [[मुफ़्त और ओपन-सोर्स सॉफ़्टवेयर|फ्री एवं ओपन-सोर्स सॉफ़्टवेयर]] के रूप में सरलता से उपलब्ध हैं एवं कुछ प्रोग्रामिंग लैंग्वेज में निर्मित होते हैं जैसे कि सैट सॉल्वर को [[बाधा तर्क प्रोग्रामिंग|कंस्ट्रेंट लॉजिक प्रोग्रामिंग]] में बाधाओं के रूप में प्रदर्शित करना है।
आधुनिक सैट सॉल्वरों का [[सॉफ़्टवेयर सत्यापन|सॉफ़्टवेयर वेरिफिकेशन]], प्रोग्राम एनालिसिस, [[बाधा संतुष्टि समस्या|कन्सट्रैन्ट सॉल्विंग]], आर्टिफिशियल इंटेलिजेंस, [[इलेक्ट्रॉनिक डिजाइन स्वचालन|इलेक्ट्रॉनिक डिजाइन ऑटोमेशन]]  एवं ऑपरेशन रिसर्च सहित क्षेत्रों पर महत्वपूर्ण प्रभाव पड़ा है। पावरफुल सॉल्वर [[मुफ़्त और ओपन-सोर्स सॉफ़्टवेयर|फ्री एवं ओपन-सोर्स सॉफ़्टवेयर]] के रूप में सरलता से उपलब्ध हैं एवं कुछ प्रोग्रामिंग लैंग्वेज में निर्मित होते हैं जैसे कि सैट सॉल्वर को [[बाधा तर्क प्रोग्रामिंग|कंस्ट्रेंट लॉजिक प्रोग्रामिंग]] में बाधाओं के रूप में प्रदर्शित करना है।
Line 13: Line 13:
डीपीएलएल सैट सॉल्वर सटिसफाईइंग असाइनमेंट की सर्च में परिवर्तनीय असाइनमेंट के (घातीय आकार के) स्पेस को ज्ञात करने के लिए व्यवस्थित बैकट्रैकिंग सर्च प्रक्रिया को नियोजित करता है। मूलरूपी सर्च प्रक्रिया 1960 दशक के प्रारम्भ में दो प्राथमिक पेपर्स में प्रस्तावित की गई थी (नीचे रिफरेन्स देखें) एवं अब इसे सामान्यतः डेविस-पुटनम-लोगमैन-लवलैंड एल्गोरिदम (डीपीएलएल या डीएलएल) के रूप में जाना जाता है।<ref>{{Cite journal | last1 = Davis | first1 = M. | last2 = Putnam | first2 = H. | title = परिमाणीकरण सिद्धांत के लिए एक कंप्यूटिंग प्रक्रिया| journal = Journal of the ACM | volume = 7 | issue = 3 | page = 201 | year = 1960 | doi = 10.1145/321033.321034| s2cid = 31888376 }}</ref><ref>{{Cite journal | last1 = Davis | first1 = M. |author-link1=Martin Davis (mathematician)| last2 = Logemann | first2 = G. | last3 = Loveland | first3 = D. | title = प्रमेय सिद्ध करने के लिए एक मशीन प्रोग्राम| journal = [[Communications of the ACM]]| volume = 5 | issue = 7 | pages = 394–397 | year = 1962 | url = http://www.ensiie.fr/~blazy/ipr/article2.pdf| doi = 10.1145/368273.368557| hdl = 2027/mdp.39015095248095 | s2cid = 15866917 | hdl-access = free }}</ref> प्रैक्टिकल सैट समाधान के लिए कई आधुनिक अप्प्रोचेस डीपीएलएल एल्गोरिथ्म से प्राप्त हुए हैं एवं समान संरचना सम्मिलित करते हैं। प्रायः वे केवल सैट समस्याओं के कुछ क्लासेज की एफिशिएंसी में सुधार करते हैं जैसे कि टेक्निकल अनुप्रयोगों में प्रदर्शित होने वाले उदाहरण या यादृच्छिक रूप से उत्पन्न उदाहरण है।<ref name=":3" /> सैद्धांतिक रूप से, एल्गोरिदम के डीपीएलएल फैमिली के लिए घातांकीय निचली सीमाएं प्रमाणित हो चुकी हैं।
डीपीएलएल सैट सॉल्वर सटिसफाईइंग असाइनमेंट की सर्च में परिवर्तनीय असाइनमेंट के (घातीय आकार के) स्पेस को ज्ञात करने के लिए व्यवस्थित बैकट्रैकिंग सर्च प्रक्रिया को नियोजित करता है। मूलरूपी सर्च प्रक्रिया 1960 दशक के प्रारम्भ में दो प्राथमिक पेपर्स में प्रस्तावित की गई थी (नीचे रिफरेन्स देखें) एवं अब इसे सामान्यतः डेविस-पुटनम-लोगमैन-लवलैंड एल्गोरिदम (डीपीएलएल या डीएलएल) के रूप में जाना जाता है।<ref>{{Cite journal | last1 = Davis | first1 = M. | last2 = Putnam | first2 = H. | title = परिमाणीकरण सिद्धांत के लिए एक कंप्यूटिंग प्रक्रिया| journal = Journal of the ACM | volume = 7 | issue = 3 | page = 201 | year = 1960 | doi = 10.1145/321033.321034| s2cid = 31888376 }}</ref><ref>{{Cite journal | last1 = Davis | first1 = M. |author-link1=Martin Davis (mathematician)| last2 = Logemann | first2 = G. | last3 = Loveland | first3 = D. | title = प्रमेय सिद्ध करने के लिए एक मशीन प्रोग्राम| journal = [[Communications of the ACM]]| volume = 5 | issue = 7 | pages = 394–397 | year = 1962 | url = http://www.ensiie.fr/~blazy/ipr/article2.pdf| doi = 10.1145/368273.368557| hdl = 2027/mdp.39015095248095 | s2cid = 15866917 | hdl-access = free }}</ref> प्रैक्टिकल सैट समाधान के लिए कई आधुनिक अप्प्रोचेस डीपीएलएल एल्गोरिथ्म से प्राप्त हुए हैं एवं समान संरचना सम्मिलित करते हैं। प्रायः वे केवल सैट समस्याओं के कुछ क्लासेज की एफिशिएंसी में सुधार करते हैं जैसे कि टेक्निकल अनुप्रयोगों में प्रदर्शित होने वाले उदाहरण या यादृच्छिक रूप से उत्पन्न उदाहरण है।<ref name=":3" /> सैद्धांतिक रूप से, एल्गोरिदम के डीपीएलएल फैमिली के लिए घातांकीय निचली सीमाएं प्रमाणित हो चुकी हैं।


जो एल्गोरिदम डीपीएलएल फैमिली का भाग नहीं हैं, उनमें [[स्टोकेस्टिक]] [[स्थानीय खोज (बाधा संतुष्टि)|लोकल सर्च]] एल्गोरिदम सम्मिलित हैं। उदाहरण [[वॉकसैट]] है। स्टोकेस्टिक विधियां सटिसफाईइंग व्याख्या का प्रयास करती हैं किन्तु यह निष्कर्ष नहीं निकाल सकती हैं कि डीपीएलएल जैसे पूर्ण एल्गोरिदम के विपरीत, सैट उदाहरण असंतोषजनक है।<ref name=":3" />
जो एल्गोरिदम डीपीएलएल फैमिली का शेयर्ड नहीं हैं, उनमें [[स्टोकेस्टिक]] [[स्थानीय खोज (बाधा संतुष्टि)|लोकल सर्च]] एल्गोरिदम सम्मिलित हैं। उदाहरण [[वॉकसैट]] है। स्टोकेस्टिक विधियां सटिसफाईइंग व्याख्या का प्रयास करती हैं किन्तु यह निष्कर्ष नहीं निकाल सकती हैं कि डीपीएलएल जैसे पूर्ण एल्गोरिदम के विपरीत, सैट उदाहरण असंतोषजनक है।<ref name=":3" />


इसके विपरीत, पटुरी, पुडलक, साक्स एवं ज़ेन द्वारा पीपीएसजेड एल्गोरिदम जैसे यादृच्छिक एल्गोरिदम कुछ अनुमानों के अनुसार रैंडमली वेरिएबल सेट करते हैं, उदाहरण के लिए बॉण्डेड विड्थ रिज़ॉल्यूशन है। यदि ह्यूरिस्टिक को करेक्ट सेटिंग नहीं प्राप्त होती है, तो वेरिएबल को यादृच्छिक रूप से असाइन किया जाता है। PPSZ एल्गोरिथ्म में <math>O(1.308^n)</math> 3-सैट के लिए  {{clarify span|runtime|I guess, for randomized algorithm, 'runtime' means 'expected runtime' or something similar, rather than 'worst case runtime'? Please qualify, and add a link to the definition, if possible.|date=February 2020}} होता है। यह 2019 तक इस समस्या के लिए सबसे प्रसिद्ध रनटाइम था, जब हैनसेन, कपलान, ज़मीर एवं ज़्विक ने रनटाइम <math>O(1.307^n)</math> 3-सैट के लिए संशोधन प्रकाशित किया, उत्तरार्द्ध वर्तमान में k के सभी मानों पर k-सैट के लिए सबसे फास्टेस्ट नोन एल्गोरिदम है। कई सटिसफाईइंग असाइनमेंट वाली सेटिंग में स्कोनिंग द्वारा रैंडमाइज्ड एल्गोरिदम की सीमा उत्तम है।<ref name="Schoning.1999">{{cite book | last1 = Schöning | first1 = Uwe| chapter = A Probabilistic Algorithm for ''k''-SAT and Constraint Satisfaction Problems | title = Proc. 40th Ann. Symp. Foundations of Computer Science| pages = 410–414 | date=Oct 1999 | chapter-url=http://homepages.cwi.nl/~rdewolf/schoning99.pdf| doi = 10.1109/SFFCS.1999.814612| isbn = 0-7695-0409-4| s2cid = 123177576}}</ref><ref name="ppsz_algorithm">[http://dl.acm.org/cition.cfm?id=1066101 k-SAT के लिए एक बेहतर घातांक-समय एल्गोरिथ्म], पटुरी, पुडलक, सैक्स, ज़ानी</ref><ref name="biased_ppsz_algorithm">[http://dl.acm.org/cation.cfm?id=3316359 बायस्ड-पीपीएसजेड का उपयोग करते हुए तेज़ के-एसएटी एल्गोरिदम], हैनसेन, कपलान, ज़मीर, ज़्विक</ref>
इसके विपरीत, पटुरी, पुडलक, साक्स एवं ज़ेन द्वारा पीपीएसजेड एल्गोरिदम जैसे यादृच्छिक एल्गोरिदम कुछ अनुमानों के अनुसार रैंडमली वेरिएबल सेट करते हैं, उदाहरण के लिए बॉण्डेड विड्थ रिज़ॉल्यूशन है। यदि ह्यूरिस्टिक को ट्रू सेटिंग नहीं प्राप्त होती है, तो वेरिएबल को यादृच्छिक रूप से असाइन किया जाता है। PPSZ एल्गोरिथ्म में <math>O(1.308^n)</math> 3-सैट के लिए  {{clarify span|runtime|I guess, for randomized algorithm, 'runtime' means 'expected runtime' or something similar, rather than 'worst case runtime'? Please qualify, and add a link to the definition, if possible.|date=February 2020}} होता है। यह 2019 तक इस समस्या के लिए सबसे प्रसिद्ध रनटाइम था, जब हैनसेन, कपलान, ज़मीर एवं ज़्विक ने रनटाइम <math>O(1.307^n)</math> 3-सैट के लिए मॉडिफिकेशन प्रकाशित किया, उत्तरार्द्ध वर्तमान में k के सभी मानों पर k-सैट के लिए सबसे फास्टेस्ट नोन एल्गोरिदम है। कई सटिसफाईइंग असाइनमेंट वाली सेटिंग में स्कोनिंग द्वारा रैंडमाइज्ड एल्गोरिदम की सीमा उत्तम है।<ref name="Schoning.1999">{{cite book | last1 = Schöning | first1 = Uwe| chapter = A Probabilistic Algorithm for ''k''-SAT and Constraint Satisfaction Problems | title = Proc. 40th Ann. Symp. Foundations of Computer Science| pages = 410–414 | date=Oct 1999 | chapter-url=http://homepages.cwi.nl/~rdewolf/schoning99.pdf| doi = 10.1109/SFFCS.1999.814612| isbn = 0-7695-0409-4| s2cid = 123177576}}</ref><ref name="ppsz_algorithm">[http://dl.acm.org/cition.cfm?id=1066101 k-SAT के लिए एक बेहतर घातांक-समय एल्गोरिथ्म], पटुरी, पुडलक, सैक्स, ज़ानी</ref><ref name="biased_ppsz_algorithm">[http://dl.acm.org/cation.cfm?id=3316359 बायस्ड-पीपीएसजेड का उपयोग करते हुए तेज़ के-एसएटी एल्गोरिदम], हैनसेन, कपलान, ज़मीर, ज़्विक</ref>


=== सीडीसीएल सॉल्वर ===
=== सीडीसीएल सॉल्वर ===
{{main|कनफ्लिक्ट-ड्रिवेन क्लॉज़ लर्निंग}}
{{main|कनफ्लिक्ट-ड्रिवेन क्लॉज़ लर्निंग}}


आधुनिक सैट सॉल्वर (2000 के दशक में विकसित) दो प्रकारों में आते हैं: कनफ्लिक्ट-ड्रिवेन एवं आगे की ओर देखने वाले। दोनों एप्रोच डीपीएलएल से उत्पन हुए हैं।<ref name=":3">{{Citation|last1=Zhang|first1=Lintao|title=The Quest for Efficient Boolean Satisfiability Solvers|date=2002|work=Computer Aided Verification|pages=17–36|publisher=Springer Berlin Heidelberg|isbn=978-3-540-43997-4|last2=Malik|first2=Sharad|doi=10.1007/3-540-45657-0_2|doi-access=free}}</ref> कनफ्लिक्ट-ड्रिवेन सॉल्वर, जैसे कनफ्लिक्ट-ड्रिवेन क्लॉज लर्निंग (सीडीसीएल), एफिशिएंट कनफ्लिक्ट एनालिसिस, क्लॉज लर्निंग, अन्य-[[कालानुक्रमिक बैकट्रैकिंग|क्रोनोलॉजिकल बैकट्रैकिंग]] के साथ-साथ वाटचेड लिटरल्स यूनिट प्रोपोगेशन, अनुकूली शाखा एवं यादृच्छिक पुनरारंभ के साथ मूलरूपी डीपीएलएल सर्च एल्गोरिदम को बढ़ाते हैं। मूलरूपी व्यवस्थित सर्च के लिए ये अतिरिक्त अनुभवजन्य रूप से इलेक्ट्रॉनिक डिज़ाइन ऑटोमेशन (EDA) में उत्पन्न होने वाले बड़े सैट उदाहरणों के लिए आवश्यक दिखाए गए हैं।<ref>{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=बूलियन संतुष्टि समाधानकर्ता और मॉडल जाँच में उनके अनुप्रयोग| pages = 2021–2035 | s2cid = 10190144 }}</ref> सुप्रसिद्ध कार्यान्वयनों में [[भूसा एल्गोरिथ्म|ग्रास्प एल्गोरिथ्म]] सम्मिलित है I<ref>{{Cite book|last1=Moskewicz|first1=M. W.|title=Proceedings of the 38th conference on Design automation (DAC)|last2=Madigan|first2=C. F.|last3=Zhao|first3=Y.|last4=Zhang|first4=L.|last5=Malik|first5=S.|year=2001|isbn=1581132972|page=530|chapter=Chaff: Engineering an Efficient SAT Solver|doi=10.1145/378239.379017|s2cid=9292941|chapter-url=http://www.princeton.edu/~chaff/publication/DAC2001v56.pdf}}</ref><ref>{{Cite journal|last1=Marques-Silva|first1=J. P.|last2=Sakallah|first2=K. A.|year=1999|title=GRASP: a search algorithm for propositional satisfiability|url=http://embedded.eecs.berkeley.edu/Alumni/wjiang/ee219b/grasp.pdf|journal=IEEE Transactions on Computers|volume=48|issue=5|page=506|doi=10.1109/12.769433|access-date=2015-08-28|archive-url=https://web.archive.org/web/20161104020512/http://embedded.eecs.berkeley.edu/Alumni/wjiang/ee219b/grasp.pdf|archive-date=2016-11-04|url-status=dead}}</ref> लुक-फॉरवर्ड सॉल्वर्स ने विशेष रूप से रिडक्शन (यूनिट-क्लॉज प्रोपोगेशन से परे) एवं अनुमानों को सशक्त किया है, एवं वे सामान्यतः कठिन उदाहरणों पर कनफ्लिक्ट-ड्रिवेन सॉल्वरों की अपेक्षा में अधिक सशक्त होते हैं (जबकि कनफ्लिक्ट-ड्रिवेन सॉल्वर बड़े उदाहरणों पर अधिक उत्तम हो सकते हैं जिनके अंदर वास्तव में सरल उदाहरण होता है)।
आधुनिक सैट सॉल्वर (2000 के दशक में विकसित) दो प्रकारों में आते हैं: कनफ्लिक्ट-ड्रिवेन एवं आगे की ओर देखने वाले। दोनों एप्रोच डीपीएलएल से उत्पन हुए हैं।<ref name=":3">{{Citation|last1=Zhang|first1=Lintao|title=The Quest for Efficient Boolean Satisfiability Solvers|date=2002|work=Computer Aided Verification|pages=17–36|publisher=Springer Berlin Heidelberg|isbn=978-3-540-43997-4|last2=Malik|first2=Sharad|doi=10.1007/3-540-45657-0_2|doi-access=free}}</ref> कनफ्लिक्ट-ड्रिवेन सॉल्वर, जैसे कनफ्लिक्ट-ड्रिवेन क्लॉज लर्निंग (सीडीसीएल), एफिशिएंट कनफ्लिक्ट एनालिसिस, क्लॉज लर्निंग, नॉन-क्रोनोलॉजिकल [[कालानुक्रमिक बैकट्रैकिंग|बैकट्रैकिंग]] के साथ-साथ वाटचेड लिटरल्स यूनिट प्रोपोगेशन, अनुकूली ब्रांच एवं यादृच्छिक पुनरारंभ के साथ मूलरूपी डीपीएलएल सर्च एल्गोरिदम को बढ़ाते हैं। मूलरूपी व्यवस्थित सर्च के लिए ये अतिरिक्त अनुभवजन्य रूप से इलेक्ट्रॉनिक डिज़ाइन ऑटोमेशन (EDA) में उत्पन्न होने वाले बड़े सैट उदाहरणों के लिए आवश्यक दिखाए गए हैं।<ref>{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=बूलियन संतुष्टि समाधानकर्ता और मॉडल जाँच में उनके अनुप्रयोग| pages = 2021–2035 | s2cid = 10190144 }}</ref> सुप्रसिद्ध कार्यान्वयनों में [[भूसा एल्गोरिथ्म|ग्रास्प एल्गोरिथ्म]] सम्मिलित है I<ref>{{Cite book|last1=Moskewicz|first1=M. W.|title=Proceedings of the 38th conference on Design automation (DAC)|last2=Madigan|first2=C. F.|last3=Zhao|first3=Y.|last4=Zhang|first4=L.|last5=Malik|first5=S.|year=2001|isbn=1581132972|page=530|chapter=Chaff: Engineering an Efficient SAT Solver|doi=10.1145/378239.379017|s2cid=9292941|chapter-url=http://www.princeton.edu/~chaff/publication/DAC2001v56.pdf}}</ref><ref>{{Cite journal|last1=Marques-Silva|first1=J. P.|last2=Sakallah|first2=K. A.|year=1999|title=GRASP: a search algorithm for propositional satisfiability|url=http://embedded.eecs.berkeley.edu/Alumni/wjiang/ee219b/grasp.pdf|journal=IEEE Transactions on Computers|volume=48|issue=5|page=506|doi=10.1109/12.769433|access-date=2015-08-28|archive-url=https://web.archive.org/web/20161104020512/http://embedded.eecs.berkeley.edu/Alumni/wjiang/ee219b/grasp.pdf|archive-date=2016-11-04|url-status=dead}}</ref> लुक-फॉरवर्ड सॉल्वर्स ने विशेष रूप से रिडक्शन (यूनिट-क्लॉज प्रोपोगेशन से परे) एवं अनुमानों को सशक्त किया है, एवं वे सामान्यतः कठिन उदाहरणों पर कनफ्लिक्ट-ड्रिवेन सॉल्वरों की अपेक्षा में अधिक सशक्त होते हैं (जबकि कनफ्लिक्ट-ड्रिवेन सॉल्वर बड़े उदाहरणों पर अधिक उत्तम हो सकते हैं जिनके अंदर रियल में सरल उदाहरण होता है)।


कनफ्लिक्ट-ड्रिवेन मिनीसैट, जो 2005 सैट प्रतियोगिता में अपेक्षाकृत सफल रहा, में कोड की केवल 600 लाइनें हैं। आधुनिक पैरेलल सैट सॉल्वर मैनीसैट है।<ref>http://www.cril.univ-artois.fr/~jabbour/manysat.htm {{Bare URL inline|date=September 2022}}</ref> यह समस्याओं के महत्वपूर्ण क्लासेज पर सुपर लीनियर स्पीड-अप प्राप्त कर सकता है। आगे बढ़ने वाले सॉल्वरों का उदाहरण मार्च_डीएल है, जिसने 2007 सैट प्रतियोगिता में पुरस्कार जीता था। गूगल के सीपी-सैट सॉल्वर, [[या-उपकरण]] के भाग, ने 2018, 2019, 2020 एवं 2021 में मिनिजिंक बाधा प्रोग्रामिंग प्रतियोगिताओं में स्वर्ण पदक जीते थे।
कनफ्लिक्ट-ड्रिवेन मिनीसैट, जो 2005 सैट प्रतियोगिता में अपेक्षाकृत सफल रहा, में कोड की केवल 600 लाइनें हैं। आधुनिक पैरेलल सैट सॉल्वर मैनीसैट है।<ref>http://www.cril.univ-artois.fr/~jabbour/manysat.htm {{Bare URL inline|date=September 2022}}</ref> यह समस्याओं के महत्वपूर्ण क्लासेज पर सुपर लीनियर स्पीड-अप प्राप्त कर सकता है। आगे बढ़ने वाले सॉल्वरों का उदाहरण मार्च_डीएल है, जिसने 2007 सैट प्रतियोगिता में पुरस्कार जीता था। गूगल के सीपी-सैट सॉल्वर, [[या-उपकरण|या डिवाइस]] के शेयर्ड, ने 2018, 2019, 2020 एवं 2021 में मिनिजिंक कन्सट्रैन्ट प्रोग्रामिंग कॉन्टेस्ट्स में स्वर्ण पदक जीते थे।


सैट के कुछ प्रकार के बड़े यादृच्छिक सटिसफाईइंग उदाहरणों का सर्वेक्षण प्रोपोगेशन (एसपी) द्वारा निवारण किया जा सकता है। विशेष रूप से [[हार्डवेयर डिज़ाइन]] एवं [[हार्डवेयर सत्यापन|हार्डवेयर वेरिफिकेशन]] अनुप्रयोगों में, किसी दिए गए प्रस्ताव फार्मूला की संतुष्टि एवं अन्य लॉजिक गुणों को कभी-कभी [[द्विआधारी निर्णय आरेख]] (बीडीडी) के रूप में फार्मूला के प्रतिनिधित्व के आधार पर सुनिश्चित किया जाता है।
सैट के कुछ प्रकार के बड़े यादृच्छिक सटिसफाईइंग उदाहरणों का सर्वेक्षण प्रोपोगेशन (एसपी) द्वारा सॉल्व किया जा सकता है। विशेष रूप से [[हार्डवेयर डिज़ाइन]] एवं [[हार्डवेयर सत्यापन|हार्डवेयर वेरिफिकेशन]] अनुप्रयोगों में, किसी दिए गए प्रस्ताव फार्मूला की संतुष्टि एवं अन्य लॉजिक गुणों को कभी-कभी [[द्विआधारी निर्णय आरेख]] (बीडीडी) के रूप में फार्मूला के प्रतिनिधित्व के आधार पर सुनिश्चित किया जाता है।


भिन्न-भिन्न सैट सॉल्वर भिन्न-भिन्न उदाहरणों को सरल या कठिन पाएंगे, एवं कुछ असंतोषजनकता प्रमाणित करने में एवं अन्य समाधान सर्च में इन्सटेंसेस प्राप्त करेंगे। ये सभी बिहेवियर सैट सोलुशन कांटेस्ट में देखे जा सकते हैं।<ref>{{cite web|url=http://www.satcompetition.org/ |title=अंतर्राष्ट्रीय SAT प्रतियोगिता वेब पेज|access-date=2007-11-15}}</ref>
भिन्न-भिन्न सैट सॉल्वर भिन्न-भिन्न उदाहरणों को सरल या कठिन पाएंगे, एवं कुछ अनसटिस्फाइयबिलिटी प्रमाणित करने में एवं अन्य समाधान सर्च में इन्सटेंसेस प्राप्त करेंगे। ये सभी बिहेवियर सैट सोलुशन कांटेस्ट में देखे जा सकते हैं।<ref>{{cite web|url=http://www.satcompetition.org/ |title=अंतर्राष्ट्रीय SAT प्रतियोगिता वेब पेज|access-date=2007-11-15}}</ref>


'''पैरेलल सैट-सॉल्विंग'''
'''पैरेलल सैट-सॉल्विंग'''
Line 35: Line 35:


=== पोर्टफोलियो ===
=== पोर्टफोलियो ===
सामान्यतः ऐसा कोई सैट सॉल्वर नहीं है जो सभी सैट समस्याओं पर अन्य सभी सॉल्वरों से उत्तम प्रदर्शन करता हो। एल्गोरिदम उन समस्या उदाहरणों के लिए करेक्ट प्रदर्शन कर सकता है जिसके लिए अन्य लोग कनफ्लिक्ट कर रहे हैं, किन्तु अन्य उदाहरणों के साथ यह व्यर्थ प्रदर्शन करता है। इसके अतिरिक्त, सैट उदाहरण को देखते हुए, यह अनुमान लगाने का कोई विश्वसनीय उपाय नहीं है कि कौन सा एल्गोरिदम इस उदाहरण में विशेष रूप से तीव्रता से निवारण करेगा। ये सीमाएँ पैरेलल पोर्टफोलियो एप्रोच को प्रेरित करती हैं। पोर्टफोलियो विभिन्न एल्गोरिदम या एल्गोरिदम के विभिन्न कॉन्फ़िगरेशन का सेट है। पैरेलल पोर्टफोलियो में सभी सॉल्वर समस्या का निवारण करने के लिए भिन्न-भिन्न प्रोसेसर पर चलते हैं। यदि सॉल्वर समाप्त हो जाता है, तो पोर्टफोलियो सॉल्वर इस सॉल्वर के अनुसार समस्या को सटिस्फाइयबल या अनसटिस्फाइयबल बताता है। अन्य सभी सॉल्वरों को समाप्त कर दिया गया है। विभिन्न प्रकार के सॉल्वरों को सम्मिलित करके पोर्टफोलियो में विविधता लाने से, जिनमें से प्रत्येक समस्या के भिन्न-भिन्न सेट पर करेक्ट प्रदर्शन करता है, सॉल्वर की पॉवर बढ़ जाती है।<ref name=":1">{{Citation|last1=Balyo|first1=Tomáš|title=Parallel Satisfiability|date=2018|work=Handbook of Parallel Constraint Reasoning|pages=3–29|publisher=Springer International Publishing|isbn=978-3-319-63515-6|last2=Sinz|first2=Carsten|doi=10.1007/978-3-319-63516-3_1}}</ref> कई सॉल्वर आंतरिक रूप से रैंडम नंबर जनरेटर का उपयोग करते हैं। अपने [[यादृच्छिक बीज|सीड्स]] में विविधता लाना पोर्टफोलियो में विविधता लाने का सरल उपाय है। अन्य विविधीकरण रणनीतियों में अनुक्रमिक सॉल्वर में कुछ अनुमानों को सक्षम करना, अक्षम करना या विविधता लाना सम्मिलित है।<ref>{{cite web|url=https://baldur.iti.kit.edu/sat-race-2010/descriptions/solver_1+2+3+6.pdf|title=Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010|last=Biere|first=Armin|website=SAT-RACE 2010}}</ref> पैरेलल पोर्टफोलियो का दोष डुप्लिकेट कार्य की मात्रा है। यदि सीक्वेंशियल सॉल्वरों में क्लॉज लर्निंग का उपयोग किया जाता है, तो पैरेलल चलने वाले सॉल्वरों के मध्य सीखे गए क्लॉज को शेयर्ड करने से डुप्लिकेट कार्य को कम किया जा सकता है एवं प्रदर्शन में वृद्धि हो सकती है। अपितु, केवल सर्वोत्तम सॉल्वरों का पोर्टफोलियो पैरेलल में चलाने से भी प्रतिस्पर्धी पैरेलल सॉल्वर बन जाता है। ऐसे सॉल्वर का उदाहरण पीपीफ़ोलियो है।<ref>{{cite web|url=http://www.cril.univ-artois.fr/~roussel/ppfolio/|title=पीपीफ़ोलियो सॉल्वर|website=www.cril.univ-artois.fr|access-date=2019-12-29}}</ref><ref>{{cite web|url=http://www.cril.univ-artois.fr/SAT11/results/ranking.php?idev=58|title=SAT 2011 Competition: 32 cores track: ranking of solvers|website=www.cril.univ-artois.fr|access-date=2020-02-13}}</ref> इसे उस प्रदर्शन के लिए निचली सीमा के लिए डिज़ाइन किया गया था जो पैरेलल सैट सॉल्वर प्रदान करने में सक्षम होना चाहिए। अनुकूलन के अभाव के कारण अधिक मात्रा में डुप्लिकेट कार्य के अतिरिक्त, इसने भाग मेमोरी मशीन पर करेक्ट प्रदर्शन किया है। होर्डेसैट<ref>{{Citation|last1=Balyo|first1=Tomáš|title=HordeSat: A Massively Parallel Portfolio SAT Solver|date=2015|work=Lecture Notes in Computer Science|pages=156–172|publisher=Springer International Publishing|isbn=978-3-319-24317-7|last2=Sanders|first2=Peter|last3=Sinz|first3=Carsten|doi=10.1007/978-3-319-24318-4_12|arxiv=1505.03340|s2cid=11507540}}</ref> कंप्यूटिंग नोड्स के बड़े समूहों के लिए पैरेलल पोर्टफोलियो सॉल्वर है। यह अपने मूल में अनुक्रमिक सॉल्वर के भिन्न-भिन्न कॉन्फ़िगर किए गए उदाहरणों का उपयोग करता है। विशेष रूप से कठिन सैट उदाहरणों के लिए होर्डेसैट रैखिक स्पीडअप उत्पन्न कर सकता है एवं इसलिए रनटाइम को अधिक कम कर सकता है।
सामान्यतः ऐसा कोई सैट सॉल्वर नहीं है जो सभी सैट समस्याओं पर अन्य सभी सॉल्वरों से उत्तम प्रदर्शन करता हो। एल्गोरिदम उन समस्या उदाहरणों के लिए ट्रू प्रदर्शन कर सकता है जिसके लिए अन्य लोग कनफ्लिक्ट कर रहे हैं, किन्तु अन्य उदाहरणों के साथ यह व्यर्थ प्रदर्शन करता है। इसके अतिरिक्त, सैट उदाहरण को देखते हुए, यह अनुमान लगाने का कोई विश्वसनीय उपाय नहीं है कि कौन सा एल्गोरिदम इस उदाहरण में विशेष रूप से तीव्रता से सॉल्व करेगा। ये सीमाएँ पैरेलल पोर्टफोलियो एप्रोच को प्रेरित करती हैं। पोर्टफोलियो विभिन्न एल्गोरिदम या एल्गोरिदम के विभिन्न कॉन्फ़िगरेशन का सेट है। पैरेलल पोर्टफोलियो में सभी सॉल्वर समस्या को सॉल्व करने के लिए भिन्न-भिन्न प्रोसेसर पर चलते हैं। यदि सॉल्वर समाप्त हो जाता है, तो पोर्टफोलियो सॉल्वर इस सॉल्वर के अनुसार समस्या को सटिस्फाइयबल या अनसटिस्फाइयबल बताता है। अन्य सभी सॉल्वरों को समाप्त कर दिया गया है। विभिन्न प्रकार के सॉल्वरों को सम्मिलित करके पोर्टफोलियो में विविधता लाने से, जिनमें से प्रत्येक समस्या के भिन्न-भिन्न सेट पर ट्रू प्रदर्शन करता है, सॉल्वर की पॉवर बढ़ जाती है।<ref name=":1">{{Citation|last1=Balyo|first1=Tomáš|title=Parallel Satisfiability|date=2018|work=Handbook of Parallel Constraint Reasoning|pages=3–29|publisher=Springer International Publishing|isbn=978-3-319-63515-6|last2=Sinz|first2=Carsten|doi=10.1007/978-3-319-63516-3_1}}</ref> कई सॉल्वर आंतरिक रूप से रैंडम नंबर जनरेटर का उपयोग करते हैं। अपने [[यादृच्छिक बीज|सीड्स]] में विविधता लाना पोर्टफोलियो में विविधता लाने का सरल उपाय है। अन्य विविधीकरण रणनीतियों में अनुक्रमिक सॉल्वर में कुछ अनुमानों को सक्षम करना, अक्षम करना या विविधता लाना सम्मिलित है।<ref>{{cite web|url=https://baldur.iti.kit.edu/sat-race-2010/descriptions/solver_1+2+3+6.pdf|title=Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010|last=Biere|first=Armin|website=SAT-RACE 2010}}</ref> पैरेलल पोर्टफोलियो का ड्राबैक डुप्लिकेट कार्य की मात्रा है। यदि सीक्वेंशियल सॉल्वरों में क्लॉज लर्निंग का उपयोग किया जाता है, तो पैरेलल चलने वाले सॉल्वरों के मध्य सीखे गए क्लॉज को शेयर्ड करने से डुप्लिकेट कार्य को कम किया जा सकता है एवं प्रदर्शन में वृद्धि हो सकती है। अपितु, केवल बेस्ट सॉल्वरों का पोर्टफोलियो पैरेलल में चलाने से भी प्रतिस्पर्धी पैरेलल सॉल्वर बन जाता है। ऐसे सॉल्वर का उदाहरण पीपीफ़ोलियो है।<ref>{{cite web|url=http://www.cril.univ-artois.fr/~roussel/ppfolio/|title=पीपीफ़ोलियो सॉल्वर|website=www.cril.univ-artois.fr|access-date=2019-12-29}}</ref><ref>{{cite web|url=http://www.cril.univ-artois.fr/SAT11/results/ranking.php?idev=58|title=SAT 2011 Competition: 32 cores track: ranking of solvers|website=www.cril.univ-artois.fr|access-date=2020-02-13}}</ref> इसे उस प्रदर्शन के लिए निचली सीमा के लिए डिज़ाइन किया गया था जो पैरेलल सैट सॉल्वर प्रदान करने में सक्षम होना चाहिए। ऑप्टिमाइजेशन के अभाव के कारण अधिक मात्रा में डुप्लिकेट कार्य के अतिरिक्त, इसने शेयर्ड मेमोरी मशीन पर ट्रू प्रदर्शन किया है। होर्डेसैट<ref>{{Citation|last1=Balyo|first1=Tomáš|title=HordeSat: A Massively Parallel Portfolio SAT Solver|date=2015|work=Lecture Notes in Computer Science|pages=156–172|publisher=Springer International Publishing|isbn=978-3-319-24317-7|last2=Sanders|first2=Peter|last3=Sinz|first3=Carsten|doi=10.1007/978-3-319-24318-4_12|arxiv=1505.03340|s2cid=11507540}}</ref> कंप्यूटिंग नोड्स के बड़े समूहों के लिए पैरेलल पोर्टफोलियो सॉल्वर है। यह अपने मूल में अनुक्रमिक सॉल्वर के भिन्न-भिन्न कॉन्फ़िगर किए गए उदाहरणों का उपयोग करता है। विशेष रूप से कठिन सैट उदाहरणों के लिए होर्डेसैट लीनियर स्पीडअप उत्पन्न कर सकता है एवं इसलिए रनटाइम को अधिक कम कर सकता है।


वर्तमान के वर्षों में पैरेलल पोर्टफोलियो सैट सॉल्वरों ने अंतर्राष्ट्रीय सैट सॉल्वर प्रतियोगिताओं के पैरेलल ट्रैक पर अपना प्रतिनिधित्व बना लिया है। ऐसे सॉल्वरों के उल्लेखनीय उदाहरणों में प्लिंगलिंग एवं पेनलेस-एमकॉमस्प्स सम्मिलित हैं।<ref>{{cite web|url=http://sat2018.forsyte.tuwien.ac.at/|title=SAT Competition 2018|website=sat2018.forsyte.tuwien.ac.at|access-date=2020-02-13}}</ref>
वर्तमान के वर्षों में पैरेलल पोर्टफोलियो सैट सॉल्वरों ने अंतर्राष्ट्रीय सैट सॉल्वर कॉन्टेस्ट्स के पैरेलल ट्रैक पर अपना प्रतिनिधित्व बना लिया है। ऐसे सॉल्वरों के उल्लेखनीय उदाहरणों में प्लिंगलिंग एवं पेनलेस-एमकॉमस्प्स सम्मिलित हैं।<ref>{{cite web|url=http://sat2018.forsyte.tuwien.ac.at/|title=SAT Competition 2018|website=sat2018.forsyte.tuwien.ac.at|access-date=2020-02-13}}</ref>


'''डिवाइड-एंड-कॉनकर'''
'''डिवाइड-एंड-कॉनकर'''


पैरेलल पोर्टफोलियो के विपरीत, पैरेलल विभाजन एवं जीत प्रसंस्करण तत्वों के मध्य सर्च समष्टि को विभाजित करने का प्रयास करता है। अनुक्रमिक डीपीएलएल जैसे डिवाइड-एंड-कॉनकर एल्गोरिदम से ही सर्च समष्टि को विभाजित करने की प्रौद्योगिकी प्रस्तावित करते हैं, इसलिए पैरेलल एल्गोरिदम की ओर उनका विस्तार सीधा है। चूँकि, विभाजन के पश्चात यूनिट प्रोपोगेशन जैसी प्रौद्योगिकी के कारण, आंशिक समस्याएं समष्टिता में अधिक भिन्न हो सकती हैं। इस प्रकार डीपीएलएल एल्गोरिदम सामान्यतः सर्च समष्टि के प्रत्येक भाग को समान समय में संसाधित नहीं करता है, जिससे चुनौतीपूर्ण [[लोड संतुलन (कंप्यूटिंग)|लोड संतुलन]] समस्या उत्पन्न होती है।<ref name=":1" />  
पैरेलल पोर्टफोलियो के विपरीत, पैरेलल डिवाइड एंड कॉन्करत प्रोसेसिंग एलिमेंट्स के मध्य सर्च स्पेस को विभाजित करने का प्रयास करता है। अनुक्रमिक डीपीएलएल जैसे डिवाइड-एंड-कॉनकर एल्गोरिदम से ही सर्च स्पेस को विभाजित करने की टेक्निक प्रस्तावित करते हैं, इसलिए पैरेलल एल्गोरिदम की ओर उनका विस्तार सीधा है। चूँकि, विभाजन के पश्चात यूनिट प्रोपोगेशन जैसी टेक्निक के कारण, पार्शियल समस्याएं कॉम्प्लेक्सिटी में अधिक भिन्न हो सकती हैं। इस प्रकार डीपीएलएल एल्गोरिदम सामान्यतः सर्च स्पेस के प्रत्येक शेयर्ड को समान समय में संसाधित नहीं करता है, जिससे चुनौतीपूर्ण [[लोड संतुलन (कंप्यूटिंग)|लोड बैलेंसिंग]] समस्या उत्पन्न होती है।<ref name=":1" />  


[[File:Cube and Conquer example.svg|alt=Tree illustrating the look-आगे चरण और परिणामी घन.|अंगूठा|348x348px|सूत्र के लिए घन चरण <math>F</math>. निर्णय अनुमानी चुनता है कि कौन से चर (सर्कल) निर्दिष्ट करने हैं। कटऑफ हेयुरिस्टिक द्वारा आगे की शाखाओं को रोकने का निर्णय लेने के बाद, सीडीसीएल का उपयोग करके आंशिक समस्याओं (आयत) को स्वतंत्र रूप से हल किया जाता है।]]
[[File:Cube and Conquer example.svg|alt=Tree illustrating the look-आगे चरण और परिणामी घन.|अंगूठा|348x348px|सूत्र के लिए घन चरण <math>F</math>. निर्णय अनुमानी चुनता है कि कौन से चर (सर्कल) निर्दिष्ट करने हैं। कटऑफ हेयुरिस्टिक द्वारा आगे की शाखाओं को रोकने का निर्णय लेने के बाद, सीडीसीएल का उपयोग करके आंशिक समस्याओं (आयत) को स्वतंत्र रूप से हल किया जाता है।]]


अन्य-क्रोनोलॉजिकल बैकट्रैकिंग के कारण, कनफ्लिक्ट-ड्रिवेन खंड सीखने का समानांतरीकरण अधिक कठिन है। इस पर नियंत्रित करने का उपाय क्यूब एंड कॉनकर प्रतिमान है।<ref name=":0">{{Citation|last1=Heule|first1=Marijn J. H.|author-link=Marijn Heule|title=Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads|date=2012|work=Hardware and Software: Verification and Testing|pages=50–65|publisher=Springer Berlin Heidelberg|isbn=978-3-642-34187-8|last2=Kullmann|first2=Oliver|last3=Wieringa|first3=Siert|last4=Biere|first4=Armin|doi=10.1007/978-3-642-34188-5_8}}</ref> यह दो चरण में समाधान करने का विचार देता है। घन चरण में समस्या को हजारों, लाखों तक क्लासेज में विभाजित किया जाता है। यह लुक-फॉरवर्ड सॉल्वर द्वारा किया जाता है, जो क्यूब्स नामक आंशिक कॉन्फ़िगरेशन का सेट ढूंढता है। घन को मूल फार्मूला के वेरिएबलों के सबसेट के [[तार्किक संयोजन|लॉजिक संयोजन]] के रूप में भी देखा जा सकता है। फार्मूला के संयोजन में, प्रत्येक घन नया फार्मूला बनाता है। इन सूत्रों को कनफ्लिक्ट-ड्रिवेन समाधानकर्ताओं द्वारा स्वतंत्र रूप से एवं समवर्ती रूप से निवारण किया जा सकता है। चूंकि इन सूत्रों का [[तार्किक विच्छेद|लॉजिक विच्छेद]]न मूल फार्मूला के लिए [[तार्किक तुल्यता|लॉजिक तुल्यता]] है, इसलिए समस्या को सटिसफाईइंग माना जाता है, यदि कोई फार्मूला सटिसफाईइंग है। आगे की ओर देखने वाला समाधानकर्ता छोटी किन्तु कठिन समस्याओं के लिए अनुकूल है,<ref>{{Cite book|last1=Heule|first1=Marijn J. H.|author-link=Marijn Heule|title=संतुष्टि की पुस्तिका|last2=van Maaren|first2=Hans|publisher=IOS Press|year=2009|isbn=978-1-58603-929-5|pages=155–184|chapter=Look-Ahead Based SAT Solvers|chapter-url=https://www.cs.utexas.edu/~marijn/publications/p01c05_lah.pdf}}</ref> इसलिए इसका उपयोग समस्या को धीरे-धीरे कई उप-समस्याओं में विभाजित करने के लिए किया जाता है। ये उप-समस्याएँ सरल हैं अपितु अधिक हैं जो कनफ्लिक्ट-ड्रिवेन समाधानकर्ता के लिए आदर्श रूप है। इसके अतिरिक्त आगे की सोच वाले समाधानकर्ता पूरी समस्या पर विचार करते हैं जबकि कनफ्लिक्टप्रेरित समाधानकर्ता अधिक लोकल जानकारी के आधार पर निर्णय लेते हैं। घन चरण में तीन अनुमान सम्मिलित हैं। घनों में वेरिएबलों को निर्णय अनुमान के अनुसार चयन होता है। दिशा अनुमान यह सुनिश्चित करता है कि किस वेरिएबल असाइनमेंट (करेक्ट या त्रुटिपूर्ण) को ज्ञात करना है। सटिसफाईइंग समस्या वाले विषयों में, सटिसफाईइंग शाखा का चयन लाभकारी होता है। कटऑफ अनुमान यह सुनिश्चित करता है कि कब क्यूब का विस्तार संवृत करना है एवं इसके अतिरिक्त इसे अनुक्रमिक कनफ्लिक्ट-ड्रिवेन सॉल्वर को अग्रेषित करना है। अधिमानतः क्यूब्स का निवारण करना समान रूप से समष्टि है।<ref name=":0" />
नॉन-क्रोनोलॉजिकल बैकट्रैकिंग के कारण, कनफ्लिक्ट-ड्रिवेन क्लॉज सीखने का समानांतरीकरण अधिक कठिन है। इस पर कंट्रोल करने का उपाय क्यूब एंड कॉनकर पैराडिग्म है।<ref name=":0">{{Citation|last1=Heule|first1=Marijn J. H.|author-link=Marijn Heule|title=Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads|date=2012|work=Hardware and Software: Verification and Testing|pages=50–65|publisher=Springer Berlin Heidelberg|isbn=978-3-642-34187-8|last2=Kullmann|first2=Oliver|last3=Wieringa|first3=Siert|last4=Biere|first4=Armin|doi=10.1007/978-3-642-34188-5_8}}</ref> यह दो चरण में समाधान करने का विचार देता है। क्यूब चरण में समस्या को हजारों, लाखों तक क्लासेज में विभाजित किया जाता है। यह लुक-फॉरवर्ड सॉल्वर द्वारा किया जाता है, जो क्यूब्स नामक पार्शियल कॉन्फ़िगरेशन का सेट ढूंढता है। क्यूब को मूल फार्मूला के वेरिएबलों के सबसेट के [[तार्किक संयोजन|लॉजिक संयोजन]] के रूप में भी देखा जा सकता है। फार्मूला के संयोजन में, प्रत्येक क्यूब नया फार्मूला बनाता है। इन फार्मूलों को कनफ्लिक्ट-ड्रिवेन सॉल्वर्स द्वारा स्वतंत्र रूप से एवं समवर्ती रूप से सॉल्व किया जा सकता है। चूंकि इन फार्मूलों का [[तार्किक विच्छेद|लॉजिक]] डिस्जंक्शन मूल फार्मूला के लिए [[तार्किक तुल्यता|एक्विवैलेन्ट]] है, इसलिए समस्या को सटिसफाईइंग माना जाता है, यदि कोई फार्मूला सटिसफाईइंग है। आगे की ओर देखने वाला सॉल्वर छोटी किन्तु कठिन समस्याओं के लिए अनुकूल है,<ref>{{Cite book|last1=Heule|first1=Marijn J. H.|author-link=Marijn Heule|title=संतुष्टि की पुस्तिका|last2=van Maaren|first2=Hans|publisher=IOS Press|year=2009|isbn=978-1-58603-929-5|pages=155–184|chapter=Look-Ahead Based SAT Solvers|chapter-url=https://www.cs.utexas.edu/~marijn/publications/p01c05_lah.pdf}}</ref> इसलिए इसका उपयोग समस्या को धीरे-धीरे कई उप-समस्याओं में विभाजित करने के लिए किया जाता है। ये उप-समस्याएँ सरल हैं अपितु अधिक हैं जो कनफ्लिक्ट-ड्रिवेन सॉल्वर के लिए आइडियल फॉर्म है। इसके अतिरिक्त आगे की सोच वाले सॉल्वर पूरी समस्या पर विचार करते हैं जबकि कनफ्लिक्टप्रेरित सॉल्वर अधिक लोकल जानकारी के आधार पर निर्णय लेते हैं। क्यूब चरण में तीन अनुमान सम्मिलित हैं। क्यूब्स में वेरिएबलों का डिसीजन हेयूरिस्टिक के अनुसार चयन होता है। दिशा अनुमान यह सुनिश्चित करता है कि किस वेरिएबल असाइनमेंट (ट्रू या फॉल्स) को ज्ञात करना है। सटिसफाईइंग समस्या वाले विषयों में, सटिसफाईइंग ब्रांच का चयन लाभकारी होता है। कटऑफ अनुमान यह सुनिश्चित करता है कि कब क्यूब का विस्तार रोकना है एवं इसके अतिरिक्त इसे अनुक्रमिक कनफ्लिक्ट-ड्रिवेन सॉल्वर को फॉरवर्ड करना है। अधिमानतः क्यूब्स का सॉल्व करना समान रूप से काम्प्लेक्स है।<ref name=":0" />


ट्रींजलिंग पैरेलल सॉल्वर का उदाहरण है जो क्यूब-एंड-कॉनकर प्रतिमान प्रस्तावित करता है। 2012 में इसके प्रारम्भ के पश्चात से इसे अंतर्राष्ट्रीय सैट सॉल्वर प्रतियोगिता में कई सफलताएँ प्राप्त हुई हैं। [[बूलियन पायथागॉरियन त्रिगुण समस्या]] का निवारण करने के लिए क्यूब-एंड-कॉन्कर का उपयोग किया गया था।<ref name=":2">{{Citation|last1=Heule|first1=Marijn J. H.|author-link=Marijn Heule|title=Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer|date=2016|work=Theory and Applications of Satisfiability Testing – SAT 2016|pages=228–245|publisher=Springer International Publishing|isbn=978-3-319-40969-6|last2=Kullmann|first2=Oliver|last3=Marek|first3=Victor W.|doi=10.1007/978-3-319-40970-2_15|arxiv=1605.00723|s2cid=7912943}}</ref>
ट्रींजलिंग पैरेलल सॉल्वर का उदाहरण है जो क्यूब-एंड-कॉनकर पैराडिग्म प्रस्तावित करता है। 2012 में इसके प्रारम्भ के पश्चात से इसे अंतर्राष्ट्रीय सैट सॉल्वर प्रतियोगिता में कई सफलताएँ प्राप्त हुई हैं। [[बूलियन पायथागॉरियन त्रिगुण समस्या|बूलियन पायथागॉरियन ट्रिपल्स प्रॉब्लम]] का सॉल्व करने के लिए क्यूब-एंड-कॉन्कर का उपयोग किया गया था।<ref name=":2">{{Citation|last1=Heule|first1=Marijn J. H.|author-link=Marijn Heule|title=Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer|date=2016|work=Theory and Applications of Satisfiability Testing – SAT 2016|pages=228–245|publisher=Springer International Publishing|isbn=978-3-319-40969-6|last2=Kullmann|first2=Oliver|last3=Marek|first3=Victor W.|doi=10.1007/978-3-319-40970-2_15|arxiv=1605.00723|s2cid=7912943}}</ref>


'''लोकल सर्च'''
'''लोकल सर्च'''

Revision as of 21:03, 15 September 2023

कंप्यूटर विज्ञान एवं फॉर्मल मेथड्स में, सैट सॉल्वर कंप्यूटर प्रोग्राम है जिसका उद्देश्य बूलियन सेटिस्फिअबिलिटी प्रॉब्लम को सॉल्व करना है। बूलियन डेटा टाइप वेरिएबल, जैसे (x या y) एवं (x या y नहीं) पर फार्मूला इनपुट करने पर, सैट सॉल्वर आउटपुट देता है कि क्या फार्मूला सेटिसफीएबल है, जिसका अर्थ है कि x एवं y की पॉसिबल वैल्यूज हैं जो फॉर्मूले को ट्रू या अनसेटिसफीएबल बनाती हैं, जिसका अर्थ है कि x एवं y की ऐसी कोई वैल्यूज नहीं हैं। इस विषय में, x ट्रू होने पर फार्मूला सेटिसफीएबल होता है, इसलिए सॉल्वर को सेटिसफीएबल रिटर्न करना चाहिए। 1960 के दशक में सैट के लिए एल्गोरिदम के प्रारम्भ के पश्चात से, आधुनिक सैट सॉल्वर कुशलतापूर्वक कार्य करने के लिए अधिक संख्या में हयूरिस्टिक्स एवं प्रोग्राम ऑप्टिमाइजेशन को सम्मिलित करते हुए काम्प्लेक्स सॉफ़्टवेयर आर्टिफैक्ट्स में विकसित हो गए हैं।

कुक-लेविन थ्योरम के रूप में जाने जाने वाले परिणाम के अनुसार, बूलियन सटिस्फाबिलिटी सामान्य रूप से एनपी-पूर्ण समस्या है। परिणामस्वरूप, केवल घातीय वर्स्ट केस कम्प्लेक्सिटी एल्गोरिदम ही ज्ञात हैं। इसके अतिरिक्त, 2000 के दशक के समय सैट के लिए एफिशिएंट एवं स्केलेबल एल्गोरिदम विकसित किए गए, जिन्होंने हजारों वेरिएबल एवं लाखों बाधाओं से जुड़े समस्या उदाहरणों को स्वचालित रूप से सॉल्व करने की क्षमता में आकस्मिक प्रगति में योगदान दिया है।[1] सैट सॉल्वर प्रायः फार्मूला को कंजेक्टिव नॉरमल फॉर्म में परिवर्तित करके प्रारम्भ करते हैं। वे प्रायः डीपीएलएल एल्गोरिदम जैसे कोर एल्गोरिदम पर आधारित होते हैं, किन्तु इसमें कई एक्सटेंशन एवं सुविधाएं सम्मिलित होती हैं। अधिकांश सैट सॉल्वरों में टाइम-आउट सम्मिलित होता है, इसलिए वे ट्रू समय में समाप्त हो जाएंगे, अपितु वे "अननोन" जैसे आउटपुट के साथ समाधान प्राप्त नहीं कर सकते है। प्रायः, सैट सॉल्वर केवल उत्तर ही नहीं देते हैं, अपितु यदि फॉर्मूला सटिसफाईइंग है तो उदाहरण असाइनमेंट (x, y, आदि के लिए मान) या फॉर्मूला असंतोषजनक होने पर असंतोषजनक क्लॉसेस का न्यूनतम सेट सहित अधिक जानकारी प्रदान कर सकते हैं।

आधुनिक सैट सॉल्वरों का सॉफ़्टवेयर वेरिफिकेशन, प्रोग्राम एनालिसिस, कन्सट्रैन्ट सॉल्विंग, आर्टिफिशियल इंटेलिजेंस, इलेक्ट्रॉनिक डिजाइन ऑटोमेशन एवं ऑपरेशन रिसर्च सहित क्षेत्रों पर महत्वपूर्ण प्रभाव पड़ा है। पावरफुल सॉल्वर फ्री एवं ओपन-सोर्स सॉफ़्टवेयर के रूप में सरलता से उपलब्ध हैं एवं कुछ प्रोग्रामिंग लैंग्वेज में निर्मित होते हैं जैसे कि सैट सॉल्वर को कंस्ट्रेंट लॉजिक प्रोग्रामिंग में बाधाओं के रूप में प्रदर्शित करना है।

अवलोकन

डीपीएलएल सॉल्वर

Main article: डीपीएलएल एल्गोरिदम

डीपीएलएल सैट सॉल्वर सटिसफाईइंग असाइनमेंट की सर्च में परिवर्तनीय असाइनमेंट के (घातीय आकार के) स्पेस को ज्ञात करने के लिए व्यवस्थित बैकट्रैकिंग सर्च प्रक्रिया को नियोजित करता है। मूलरूपी सर्च प्रक्रिया 1960 दशक के प्रारम्भ में दो प्राथमिक पेपर्स में प्रस्तावित की गई थी (नीचे रिफरेन्स देखें) एवं अब इसे सामान्यतः डेविस-पुटनम-लोगमैन-लवलैंड एल्गोरिदम (डीपीएलएल या डीएलएल) के रूप में जाना जाता है।[2][3] प्रैक्टिकल सैट समाधान के लिए कई आधुनिक अप्प्रोचेस डीपीएलएल एल्गोरिथ्म से प्राप्त हुए हैं एवं समान संरचना सम्मिलित करते हैं। प्रायः वे केवल सैट समस्याओं के कुछ क्लासेज की एफिशिएंसी में सुधार करते हैं जैसे कि टेक्निकल अनुप्रयोगों में प्रदर्शित होने वाले उदाहरण या यादृच्छिक रूप से उत्पन्न उदाहरण है।[4] सैद्धांतिक रूप से, एल्गोरिदम के डीपीएलएल फैमिली के लिए घातांकीय निचली सीमाएं प्रमाणित हो चुकी हैं।

जो एल्गोरिदम डीपीएलएल फैमिली का शेयर्ड नहीं हैं, उनमें स्टोकेस्टिक लोकल सर्च एल्गोरिदम सम्मिलित हैं। उदाहरण वॉकसैट है। स्टोकेस्टिक विधियां सटिसफाईइंग व्याख्या का प्रयास करती हैं किन्तु यह निष्कर्ष नहीं निकाल सकती हैं कि डीपीएलएल जैसे पूर्ण एल्गोरिदम के विपरीत, सैट उदाहरण असंतोषजनक है।[4]

इसके विपरीत, पटुरी, पुडलक, साक्स एवं ज़ेन द्वारा पीपीएसजेड एल्गोरिदम जैसे यादृच्छिक एल्गोरिदम कुछ अनुमानों के अनुसार रैंडमली वेरिएबल सेट करते हैं, उदाहरण के लिए बॉण्डेड विड्थ रिज़ॉल्यूशन है। यदि ह्यूरिस्टिक को ट्रू सेटिंग नहीं प्राप्त होती है, तो वेरिएबल को यादृच्छिक रूप से असाइन किया जाता है। PPSZ एल्गोरिथ्म में 3-सैट के लिए runtime[clarify] होता है। यह 2019 तक इस समस्या के लिए सबसे प्रसिद्ध रनटाइम था, जब हैनसेन, कपलान, ज़मीर एवं ज़्विक ने रनटाइम 3-सैट के लिए मॉडिफिकेशन प्रकाशित किया, उत्तरार्द्ध वर्तमान में k के सभी मानों पर k-सैट के लिए सबसे फास्टेस्ट नोन एल्गोरिदम है। कई सटिसफाईइंग असाइनमेंट वाली सेटिंग में स्कोनिंग द्वारा रैंडमाइज्ड एल्गोरिदम की सीमा उत्तम है।[5][6][7]

सीडीसीएल सॉल्वर

Main article: कनफ्लिक्ट-ड्रिवेन क्लॉज़ लर्निंग

आधुनिक सैट सॉल्वर (2000 के दशक में विकसित) दो प्रकारों में आते हैं: कनफ्लिक्ट-ड्रिवेन एवं आगे की ओर देखने वाले। दोनों एप्रोच डीपीएलएल से उत्पन हुए हैं।[4] कनफ्लिक्ट-ड्रिवेन सॉल्वर, जैसे कनफ्लिक्ट-ड्रिवेन क्लॉज लर्निंग (सीडीसीएल), एफिशिएंट कनफ्लिक्ट एनालिसिस, क्लॉज लर्निंग, नॉन-क्रोनोलॉजिकल बैकट्रैकिंग के साथ-साथ वाटचेड लिटरल्स यूनिट प्रोपोगेशन, अनुकूली ब्रांच एवं यादृच्छिक पुनरारंभ के साथ मूलरूपी डीपीएलएल सर्च एल्गोरिदम को बढ़ाते हैं। मूलरूपी व्यवस्थित सर्च के लिए ये अतिरिक्त अनुभवजन्य रूप से इलेक्ट्रॉनिक डिज़ाइन ऑटोमेशन (EDA) में उत्पन्न होने वाले बड़े सैट उदाहरणों के लिए आवश्यक दिखाए गए हैं।[8] सुप्रसिद्ध कार्यान्वयनों में ग्रास्प एल्गोरिथ्म सम्मिलित है I[9][10] लुक-फॉरवर्ड सॉल्वर्स ने विशेष रूप से रिडक्शन (यूनिट-क्लॉज प्रोपोगेशन से परे) एवं अनुमानों को सशक्त किया है, एवं वे सामान्यतः कठिन उदाहरणों पर कनफ्लिक्ट-ड्रिवेन सॉल्वरों की अपेक्षा में अधिक सशक्त होते हैं (जबकि कनफ्लिक्ट-ड्रिवेन सॉल्वर बड़े उदाहरणों पर अधिक उत्तम हो सकते हैं जिनके अंदर रियल में सरल उदाहरण होता है)।

कनफ्लिक्ट-ड्रिवेन मिनीसैट, जो 2005 सैट प्रतियोगिता में अपेक्षाकृत सफल रहा, में कोड की केवल 600 लाइनें हैं। आधुनिक पैरेलल सैट सॉल्वर मैनीसैट है।[11] यह समस्याओं के महत्वपूर्ण क्लासेज पर सुपर लीनियर स्पीड-अप प्राप्त कर सकता है। आगे बढ़ने वाले सॉल्वरों का उदाहरण मार्च_डीएल है, जिसने 2007 सैट प्रतियोगिता में पुरस्कार जीता था। गूगल के सीपी-सैट सॉल्वर, या डिवाइस के शेयर्ड, ने 2018, 2019, 2020 एवं 2021 में मिनिजिंक कन्सट्रैन्ट प्रोग्रामिंग कॉन्टेस्ट्स में स्वर्ण पदक जीते थे।

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

भिन्न-भिन्न सैट सॉल्वर भिन्न-भिन्न उदाहरणों को सरल या कठिन पाएंगे, एवं कुछ अनसटिस्फाइयबिलिटी प्रमाणित करने में एवं अन्य समाधान सर्च में इन्सटेंसेस प्राप्त करेंगे। ये सभी बिहेवियर सैट सोलुशन कांटेस्ट में देखे जा सकते हैं।[12]

पैरेलल सैट-सॉल्विंग

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

अंतर्राष्ट्रीय सैट सॉल्वर प्रतियोगिता में पैरेलल ट्रैक है जो पैरेलल सैट समाधान में वर्तमान की प्रगति को प्रदर्शित करता है। 2016 में,[13] 2017[14] एवं 2018,[15] बेंचमार्क 24 सेंट्रल प्रोसेसिंग यूनिट के साथ शेयर्ड-मेमोरी सिस्टम पर चलाए गए थे, इसलिए वितरित मेमोरी या कई कोर प्रोसेसर के लिए सॉल्वर कम पड़ गए थे।

पोर्टफोलियो

सामान्यतः ऐसा कोई सैट सॉल्वर नहीं है जो सभी सैट समस्याओं पर अन्य सभी सॉल्वरों से उत्तम प्रदर्शन करता हो। एल्गोरिदम उन समस्या उदाहरणों के लिए ट्रू प्रदर्शन कर सकता है जिसके लिए अन्य लोग कनफ्लिक्ट कर रहे हैं, किन्तु अन्य उदाहरणों के साथ यह व्यर्थ प्रदर्शन करता है। इसके अतिरिक्त, सैट उदाहरण को देखते हुए, यह अनुमान लगाने का कोई विश्वसनीय उपाय नहीं है कि कौन सा एल्गोरिदम इस उदाहरण में विशेष रूप से तीव्रता से सॉल्व करेगा। ये सीमाएँ पैरेलल पोर्टफोलियो एप्रोच को प्रेरित करती हैं। पोर्टफोलियो विभिन्न एल्गोरिदम या एल्गोरिदम के विभिन्न कॉन्फ़िगरेशन का सेट है। पैरेलल पोर्टफोलियो में सभी सॉल्वर समस्या को सॉल्व करने के लिए भिन्न-भिन्न प्रोसेसर पर चलते हैं। यदि सॉल्वर समाप्त हो जाता है, तो पोर्टफोलियो सॉल्वर इस सॉल्वर के अनुसार समस्या को सटिस्फाइयबल या अनसटिस्फाइयबल बताता है। अन्य सभी सॉल्वरों को समाप्त कर दिया गया है। विभिन्न प्रकार के सॉल्वरों को सम्मिलित करके पोर्टफोलियो में विविधता लाने से, जिनमें से प्रत्येक समस्या के भिन्न-भिन्न सेट पर ट्रू प्रदर्शन करता है, सॉल्वर की पॉवर बढ़ जाती है।[16] कई सॉल्वर आंतरिक रूप से रैंडम नंबर जनरेटर का उपयोग करते हैं। अपने सीड्स में विविधता लाना पोर्टफोलियो में विविधता लाने का सरल उपाय है। अन्य विविधीकरण रणनीतियों में अनुक्रमिक सॉल्वर में कुछ अनुमानों को सक्षम करना, अक्षम करना या विविधता लाना सम्मिलित है।[17] पैरेलल पोर्टफोलियो का ड्राबैक डुप्लिकेट कार्य की मात्रा है। यदि सीक्वेंशियल सॉल्वरों में क्लॉज लर्निंग का उपयोग किया जाता है, तो पैरेलल चलने वाले सॉल्वरों के मध्य सीखे गए क्लॉज को शेयर्ड करने से डुप्लिकेट कार्य को कम किया जा सकता है एवं प्रदर्शन में वृद्धि हो सकती है। अपितु, केवल बेस्ट सॉल्वरों का पोर्टफोलियो पैरेलल में चलाने से भी प्रतिस्पर्धी पैरेलल सॉल्वर बन जाता है। ऐसे सॉल्वर का उदाहरण पीपीफ़ोलियो है।[18][19] इसे उस प्रदर्शन के लिए निचली सीमा के लिए डिज़ाइन किया गया था जो पैरेलल सैट सॉल्वर प्रदान करने में सक्षम होना चाहिए। ऑप्टिमाइजेशन के अभाव के कारण अधिक मात्रा में डुप्लिकेट कार्य के अतिरिक्त, इसने शेयर्ड मेमोरी मशीन पर ट्रू प्रदर्शन किया है। होर्डेसैट[20] कंप्यूटिंग नोड्स के बड़े समूहों के लिए पैरेलल पोर्टफोलियो सॉल्वर है। यह अपने मूल में अनुक्रमिक सॉल्वर के भिन्न-भिन्न कॉन्फ़िगर किए गए उदाहरणों का उपयोग करता है। विशेष रूप से कठिन सैट उदाहरणों के लिए होर्डेसैट लीनियर स्पीडअप उत्पन्न कर सकता है एवं इसलिए रनटाइम को अधिक कम कर सकता है।

वर्तमान के वर्षों में पैरेलल पोर्टफोलियो सैट सॉल्वरों ने अंतर्राष्ट्रीय सैट सॉल्वर कॉन्टेस्ट्स के पैरेलल ट्रैक पर अपना प्रतिनिधित्व बना लिया है। ऐसे सॉल्वरों के उल्लेखनीय उदाहरणों में प्लिंगलिंग एवं पेनलेस-एमकॉमस्प्स सम्मिलित हैं।[21]

डिवाइड-एंड-कॉनकर

पैरेलल पोर्टफोलियो के विपरीत, पैरेलल डिवाइड एंड कॉन्करत प्रोसेसिंग एलिमेंट्स के मध्य सर्च स्पेस को विभाजित करने का प्रयास करता है। अनुक्रमिक डीपीएलएल जैसे डिवाइड-एंड-कॉनकर एल्गोरिदम से ही सर्च स्पेस को विभाजित करने की टेक्निक प्रस्तावित करते हैं, इसलिए पैरेलल एल्गोरिदम की ओर उनका विस्तार सीधा है। चूँकि, विभाजन के पश्चात यूनिट प्रोपोगेशन जैसी टेक्निक के कारण, पार्शियल समस्याएं कॉम्प्लेक्सिटी में अधिक भिन्न हो सकती हैं। इस प्रकार डीपीएलएल एल्गोरिदम सामान्यतः सर्च स्पेस के प्रत्येक शेयर्ड को समान समय में संसाधित नहीं करता है, जिससे चुनौतीपूर्ण लोड बैलेंसिंग समस्या उत्पन्न होती है।[16]

Tree illustrating the look-आगे चरण और परिणामी घन.

नॉन-क्रोनोलॉजिकल बैकट्रैकिंग के कारण, कनफ्लिक्ट-ड्रिवेन क्लॉज सीखने का समानांतरीकरण अधिक कठिन है। इस पर कंट्रोल करने का उपाय क्यूब एंड कॉनकर पैराडिग्म है।[22] यह दो चरण में समाधान करने का विचार देता है। क्यूब चरण में समस्या को हजारों, लाखों तक क्लासेज में विभाजित किया जाता है। यह लुक-फॉरवर्ड सॉल्वर द्वारा किया जाता है, जो क्यूब्स नामक पार्शियल कॉन्फ़िगरेशन का सेट ढूंढता है। क्यूब को मूल फार्मूला के वेरिएबलों के सबसेट के लॉजिक संयोजन के रूप में भी देखा जा सकता है। फार्मूला के संयोजन में, प्रत्येक क्यूब नया फार्मूला बनाता है। इन फार्मूलों को कनफ्लिक्ट-ड्रिवेन सॉल्वर्स द्वारा स्वतंत्र रूप से एवं समवर्ती रूप से सॉल्व किया जा सकता है। चूंकि इन फार्मूलों का लॉजिक डिस्जंक्शन मूल फार्मूला के लिए एक्विवैलेन्ट है, इसलिए समस्या को सटिसफाईइंग माना जाता है, यदि कोई फार्मूला सटिसफाईइंग है। आगे की ओर देखने वाला सॉल्वर छोटी किन्तु कठिन समस्याओं के लिए अनुकूल है,[23] इसलिए इसका उपयोग समस्या को धीरे-धीरे कई उप-समस्याओं में विभाजित करने के लिए किया जाता है। ये उप-समस्याएँ सरल हैं अपितु अधिक हैं जो कनफ्लिक्ट-ड्रिवेन सॉल्वर के लिए आइडियल फॉर्म है। इसके अतिरिक्त आगे की सोच वाले सॉल्वर पूरी समस्या पर विचार करते हैं जबकि कनफ्लिक्टप्रेरित सॉल्वर अधिक लोकल जानकारी के आधार पर निर्णय लेते हैं। क्यूब चरण में तीन अनुमान सम्मिलित हैं। क्यूब्स में वेरिएबलों का डिसीजन हेयूरिस्टिक के अनुसार चयन होता है। दिशा अनुमान यह सुनिश्चित करता है कि किस वेरिएबल असाइनमेंट (ट्रू या फॉल्स) को ज्ञात करना है। सटिसफाईइंग समस्या वाले विषयों में, सटिसफाईइंग ब्रांच का चयन लाभकारी होता है। कटऑफ अनुमान यह सुनिश्चित करता है कि कब क्यूब का विस्तार रोकना है एवं इसके अतिरिक्त इसे अनुक्रमिक कनफ्लिक्ट-ड्रिवेन सॉल्वर को फॉरवर्ड करना है। अधिमानतः क्यूब्स का सॉल्व करना समान रूप से काम्प्लेक्स है।[22]

ट्रींजलिंग पैरेलल सॉल्वर का उदाहरण है जो क्यूब-एंड-कॉनकर पैराडिग्म प्रस्तावित करता है। 2012 में इसके प्रारम्भ के पश्चात से इसे अंतर्राष्ट्रीय सैट सॉल्वर प्रतियोगिता में कई सफलताएँ प्राप्त हुई हैं। बूलियन पायथागॉरियन ट्रिपल्स प्रॉब्लम का सॉल्व करने के लिए क्यूब-एंड-कॉन्कर का उपयोग किया गया था।[24]

लोकल सर्च

सैट सॉल्विंग के लिए पैरेलल लोकल सर्च एल्गोरिदम की दिशा में स्ट्रेटेजी विभिन्न प्रोसेसिंग यूनिट्स पर साथ मल्टीपल वेरिएबल फ़्लिप्स को ट्राई करना है।[25] दूसरा, उपर्युक्त पोर्टफोलियो एप्रोच को प्रस्तावित करना है, चूँकि क्लॉज सम्मिलित करना संभव नहीं है क्योंकि लोकल सर्च सॉल्वर क्लॉज का उत्पादन नहीं करते हैं। वैकल्पिक रूप से, लोकल स्तर पर उत्पादित कॉन्फ़िगरेशन को सम्मिलित करना संभव है। जब कोई लोकल सॉल्वर सर्च को रीस्टार्ट करने का निर्णय लेता है तो इन कॉन्फ़िगरेशन का उपयोग नए इनिशियल कॉन्फ़िगरेशन के उत्पादन को निर्देशित करने के लिए किया जा सकता है।[26]

यह भी देखें

संदर्भ

  1. ↑ Ohrimenko, Olga; Stuckey, Peter J.; Codish, Michael (2007), "Propagation = Lazy Clause Generation", Principles and Practice of Constraint Programming – CP 2007, Lecture Notes in Computer Science, vol. 4741, pp. 544–558, CiteSeerX 10.1.1.70.5471, doi:10.1007/978-3-540-74970-7_39, modern SAT solvers can often handle problems with millions of constraints and hundreds of thousands of variables
  2. ↑ Davis, M.; Putnam, H. (1960). "परिमाणीकरण सिद्धांत के लिए एक कंप्यूटिंग प्रक्रिया". Journal of the ACM. 7 (3): 201. doi:10.1145/321033.321034. S2CID 31888376.
  3. ↑ Davis, M.; Logemann, G.; Loveland, D. (1962). "प्रमेय सिद्ध करने के लिए एक मशीन प्रोग्राम" (PDF). Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. S2CID 15866917.
  4. ↑ 4.0 4.1 4.2 Zhang, Lintao; Malik, Sharad (2002), "The Quest for Efficient Boolean Satisfiability Solvers", Computer Aided Verification, Springer Berlin Heidelberg, pp. 17–36, doi:10.1007/3-540-45657-0_2, ISBN 978-3-540-43997-4
  5. ↑ Schöning, Uwe (Oct 1999). "A Probabilistic Algorithm for k-SAT and Constraint Satisfaction Problems" (PDF). Proc. 40th Ann. Symp. Foundations of Computer Science. pp. 410–414. doi:10.1109/SFFCS.1999.814612. ISBN 0-7695-0409-4. S2CID 123177576.
  6. ↑ k-SAT के लिए एक बेहतर घातांक-समय एल्गोरिथ्म, पटुरी, पुडलक, सैक्स, ज़ानी
  7. ↑ बायस्ड-पीपीएसजेड का उपयोग करते हुए तेज़ के-एसएटी एल्गोरिदम, हैनसेन, कपलान, ज़मीर, ज़्विक
  8. ↑ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "बूलियन संतुष्टि समाधानकर्ता और मॉडल जाँच में उनके अनुप्रयोग". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.
  9. ↑ Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S. (2001). "Chaff: Engineering an Efficient SAT Solver" (PDF). Proceedings of the 38th conference on Design automation (DAC). p. 530. doi:10.1145/378239.379017. ISBN 1581132972. S2CID 9292941.
  10. ↑ Marques-Silva, J. P.; Sakallah, K. A. (1999). "GRASP: a search algorithm for propositional satisfiability" (PDF). IEEE Transactions on Computers. 48 (5): 506. doi:10.1109/12.769433. Archived from the original (PDF) on 2016-11-04. Retrieved 2015-08-28.
  11. ↑ http://www.cril.univ-artois.fr/~jabbour/manysat.htm[bare URL]
  12. ↑ "अंतर्राष्ट्रीय SAT प्रतियोगिता वेब पेज". Retrieved 2007-11-15.
  13. ↑ "SAT Competition 2016". baldur.iti.kit.edu. Retrieved 2020-02-13.
  14. ↑ "SAT Competition 2017". baldur.iti.kit.edu. Retrieved 2020-02-13.
  15. ↑ "SAT Competition 2018". sat2018.forsyte.tuwien.ac.at. Retrieved 2020-02-13.
  16. ↑ 16.0 16.1 Balyo, Tomáš; Sinz, Carsten (2018), "Parallel Satisfiability", Handbook of Parallel Constraint Reasoning, Springer International Publishing, pp. 3–29, doi:10.1007/978-3-319-63516-3_1, ISBN 978-3-319-63515-6
  17. ↑ Biere, Armin. "Lingeling, Plingeling, PicoSAT and PrecoSAT at SAT Race 2010" (PDF). SAT-RACE 2010.
  18. ↑ "पीपीफ़ोलियो सॉल्वर". www.cril.univ-artois.fr. Retrieved 2019-12-29.
  19. ↑ "SAT 2011 Competition: 32 cores track: ranking of solvers". www.cril.univ-artois.fr. Retrieved 2020-02-13.
  20. ↑ Balyo, Tomáš; Sanders, Peter; Sinz, Carsten (2015), "HordeSat: A Massively Parallel Portfolio SAT Solver", Lecture Notes in Computer Science, Springer International Publishing, pp. 156–172, arXiv:1505.03340, doi:10.1007/978-3-319-24318-4_12, ISBN 978-3-319-24317-7, S2CID 11507540
  21. ↑ "SAT Competition 2018". sat2018.forsyte.tuwien.ac.at. Retrieved 2020-02-13.
  22. ↑ 22.0 22.1 Heule, Marijn J. H.; Kullmann, Oliver; Wieringa, Siert; Biere, Armin (2012), "Cube and Conquer: Guiding CDCL SAT Solvers by Lookaheads", Hardware and Software: Verification and Testing, Springer Berlin Heidelberg, pp. 50–65, doi:10.1007/978-3-642-34188-5_8, ISBN 978-3-642-34187-8
  23. ↑ Heule, Marijn J. H.; van Maaren, Hans (2009). "Look-Ahead Based SAT Solvers" (PDF). संतुष्टि की पुस्तिका. IOS Press. pp. 155–184. ISBN 978-1-58603-929-5.
  24. ↑ Heule, Marijn J. H.; Kullmann, Oliver; Marek, Victor W. (2016), "Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer", Theory and Applications of Satisfiability Testing – SAT 2016, Springer International Publishing, pp. 228–245, arXiv:1605.00723, doi:10.1007/978-3-319-40970-2_15, ISBN 978-3-319-40969-6, S2CID 7912943
  25. ↑ Roli, Andrea (2002), "Criticality and Parallelism in Structured SAT Instances", Principles and Practice of Constraint Programming - CP 2002, Lecture Notes in Computer Science, vol. 2470, Springer Berlin Heidelberg, pp. 714–719, doi:10.1007/3-540-46135-3_51, ISBN 978-3-540-44120-5
  26. ↑ Arbelaez, Alejandro; Hamadi, Youssef (2011), "Improving Parallel Local Search for SAT", Lecture Notes in Computer Science, Springer Berlin Heidelberg, pp. 46–60, doi:10.1007/978-3-642-25566-3_4, ISBN 978-3-642-25565-6, S2CID 14735849
Retrieved from ‘https://www.vigyanwiki.in/index.php?title=सैट_सॉल्वर&oldid=281574’