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

From Vigyanwiki
(Created page with "{{Short description|Computer program for the Boolean satisfiability problem}} कंप्यूटर विज्ञान और औपचारिक तरीको...")
 
No edit summary
Line 1: Line 1:
{{Short description|Computer program for the Boolean satisfiability problem}}
{{Short description|Computer program for the Boolean satisfiability problem}}
[[कंप्यूटर विज्ञान]] और औपचारिक तरीकों में, SAT सॉल्वर एक [[कंप्यूटर प्रोग्राम]] है जिसका उद्देश्य [[बूलियन [[संतुष्टि]] समस्या]] को हल करना है। [[बूलियन डेटा प्रकार]] चर, जैसे (''x'' या ''y'') और (''x'' या नहीं ''y'') पर एक सूत्र इनपुट करने पर, एक SAT सॉल्वर आउटपुट करता है कि क्या सूत्र संतोषजनक है, जिसका अर्थ है कि ''x'' और ''y'' के संभावित मान हैं जो सूत्र को सही या असंतोषजनक बनाते हैं, जिसका अर्थ है कि ''x'' और ''y'' के ऐसे कोई मान नहीं हैं। इस मामले में, ''x'' सत्य होने पर सूत्र संतोषजनक होता है, इसलिए सॉल्वर को संतोषजनक लौटना चाहिए। 1960 के दशक में SAT के लिए [[कलन विधि]] की शुरुआत के बाद से, आधुनिक SAT सॉल्वर कुशलतापूर्वक काम करने के लिए बड़ी संख्या में अनुमान और प्रोग्राम अनुकूलन को शामिल करते हुए जटिल [[सॉफ़्टवेयर]] में विकसित हो गए हैं।
[[कंप्यूटर विज्ञान]] और औपचारिक तरीकों में, SAT सॉल्वर [[कंप्यूटर प्रोग्राम]] है जिसका उद्देश्य [[बूलियन [[संतुष्टि]] समस्या]] को हल करना है। [[बूलियन डेटा प्रकार]] चर, जैसे (''x'' या ''y'') और (''x'' या नहीं ''y'') पर सूत्र इनपुट करने पर, SAT सॉल्वर आउटपुट करता है कि क्या सूत्र संतोषजनक है, जिसका अर्थ है कि ''x'' और ''y'' के संभावित मान हैं जो सूत्र को सही या असंतोषजनक बनाते हैं, जिसका अर्थ है कि ''x'' और ''y'' के ऐसे कोई मान नहीं हैं। इस मामले में, ''x'' सत्य होने पर सूत्र संतोषजनक होता है, इसलिए सॉल्वर को संतोषजनक लौटना चाहिए। 1960 के दशक में SAT के लिए [[कलन विधि]] की शुरुआत के बाद से, आधुनिक SAT सॉल्वर कुशलतापूर्वक काम करने के लिए बड़ी संख्या में अनुमान और प्रोग्राम अनुकूलन को शामिल करते हुए जटिल [[सॉफ़्टवेयर]] में विकसित हो गए हैं।


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


आधुनिक SAT सॉल्वरों का [[सॉफ़्टवेयर सत्यापन]], प्रोग्राम विश्लेषण, [[बाधा संतुष्टि समस्या]], कृत्रिम बुद्धिमत्ता[[इलेक्ट्रॉनिक डिजाइन स्वचालन]] स्वचालन और संचालन अनुसंधान सहित क्षेत्रों पर महत्वपूर्ण प्रभाव पड़ा है। शक्तिशाली सॉल्वर [[मुफ़्त और ओपन-सोर्स सॉफ़्टवेयर]] के रूप में आसानी से उपलब्ध हैं और कुछ प्रोग्रामिंग भाषाओं में निर्मित होते हैं जैसे कि SAT सॉल्वर को [[बाधा तर्क प्रोग्रामिंग]] में बाधाओं के रूप में उजागर करना।
आधुनिक SAT सॉल्वरों का [[सॉफ़्टवेयर सत्यापन]], प्रोग्राम विश्लेषण, [[बाधा संतुष्टि समस्या]], कृत्रिम बुद्धिमत्ता[[इलेक्ट्रॉनिक डिजाइन स्वचालन]] स्वचालन और संचालन अनुसंधान सहित क्षेत्रों पर महत्वपूर्ण प्रभाव पड़ा है। शक्तिशाली सॉल्वर [[मुफ़्त और ओपन-सोर्स सॉफ़्टवेयर]] के रूप में आसानी से उपलब्ध हैं और कुछ प्रोग्रामिंग भाषाओं में निर्मित होते हैं जैसे कि SAT सॉल्वर को [[बाधा तर्क प्रोग्रामिंग]] में बाधाओं के रूप में उजागर करना।
Line 12: Line 12:
{{main|DPLL algorithm}}
{{main|DPLL algorithm}}


एक डीपीएलएल एसएटी सॉल्वर संतोषजनक असाइनमेंट की तलाश में परिवर्तनीय असाइनमेंट के (घातीय आकार के) स्थान का पता लगाने के लिए एक व्यवस्थित बैकट्रैकिंग खोज प्रक्रिया को नियोजित करता है। बुनियादी खोज प्रक्रिया 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> व्यावहारिक SAT समाधान के लिए कई आधुनिक दृष्टिकोण DPLL एल्गोरिथ्म से प्राप्त हुए हैं और समान संरचना साझा करते हैं। अक्सर वे केवल SAT समस्याओं के कुछ वर्गों की दक्षता में सुधार करते हैं जैसे कि औद्योगिक अनुप्रयोगों में दिखाई देने वाले उदाहरण या यादृच्छिक रूप से उत्पन्न उदाहरण।<ref name=":3" />सैद्धांतिक रूप से, एल्गोरिदम के डीपीएलएल परिवार के लिए घातांकीय निचली सीमाएं साबित हो चुकी हैं।{{citation needed|date=February 2020}}
डीपीएलएल एसएटी सॉल्वर संतोषजनक असाइनमेंट की तलाश में परिवर्तनीय असाइनमेंट के (घातीय आकार के) स्थान का पता लगाने के लिए व्यवस्थित बैकट्रैकिंग खोज प्रक्रिया को नियोजित करता है। बुनियादी खोज प्रक्रिया 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> व्यावहारिक SAT समाधान के लिए कई आधुनिक दृष्टिकोण DPLL एल्गोरिथ्म से प्राप्त हुए हैं और समान संरचना साझा करते हैं। अक्सर वे केवल SAT समस्याओं के कुछ वर्गों की दक्षता में सुधार करते हैं जैसे कि औद्योगिक अनुप्रयोगों में दिखाई देने वाले उदाहरण या यादृच्छिक रूप से उत्पन्न उदाहरण।<ref name=":3" />सैद्धांतिक रूप से, एल्गोरिदम के डीपीएलएल परिवार के लिए घातांकीय निचली सीमाएं साबित हो चुकी हैं।{{citation needed|date=February 2020}}


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


इसके विपरीत, पटुरी, पुडलक, सैक्स और ज़ेन द्वारा पीपीएसजेड एल्गोरिदम जैसे यादृच्छिक एल्गोरिदम कुछ अनुमानों के अनुसार यादृच्छिक क्रम में चर सेट करते हैं, उदाहरण के लिए सीमा-चौड़ाई रिज़ॉल्यूशन (तर्क)। यदि अनुमानी को सही सेटिंग नहीं मिल पाती है, तो वेरिएबल को यादृच्छिक रूप से असाइन किया जाता है। PPSZ एल्गोरिथ्म में एक है {{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}} का <math>O(1.308^n)</math> 3-सैट के लिए. यह 2019 तक इस समस्या के लिए सबसे प्रसिद्ध रनटाइम था, जब हैनसेन, कपलान, ज़मीर और ज़्विक ने रनटाइम के साथ उस एल्गोरिदम का एक संशोधन प्रकाशित किया <math>O(1.307^n)</math> 3-सैट के लिए. उत्तरार्द्ध वर्तमान में k के सभी मानों पर k-SAT के लिए सबसे तेज़ ज्ञात एल्गोरिदम है। कई संतोषजनक असाइनमेंट वाली सेटिंग में स्कोनिंग द्वारा यादृच्छिक एल्गोरिदम की सीमा बेहतर है।<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 एल्गोरिथ्म में है {{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}} का <math>O(1.308^n)</math> 3-सैट के लिए. यह 2019 तक इस समस्या के लिए सबसे प्रसिद्ध रनटाइम था, जब हैनसेन, कपलान, ज़मीर और ज़्विक ने रनटाइम के साथ उस एल्गोरिदम का संशोधन प्रकाशित किया <math>O(1.307^n)</math> 3-सैट के लिए. उत्तरार्द्ध वर्तमान में k के सभी मानों पर k-SAT के लिए सबसे तेज़ ज्ञात एल्गोरिदम है। कई संतोषजनक असाइनमेंट वाली सेटिंग में स्कोनिंग द्वारा यादृच्छिक एल्गोरिदम की सीमा बेहतर है।<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|Conflict-driven clause learning}}
{{main|Conflict-driven clause learning}}


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


SAT के कुछ प्रकार के बड़े यादृच्छिक संतोषजनक उदाहरणों को सर्वेक्षण प्रसार (एसपी) द्वारा हल किया जा सकता है।{{citation needed|date=December 2021}} विशेष रूप से [[हार्डवेयर डिज़ाइन]] और [[हार्डवेयर सत्यापन]] अनुप्रयोगों में, किसी दिए गए प्रस्ताव सूत्र की संतुष्टि और अन्य तार्किक गुणों को कभी-कभी [[द्विआधारी निर्णय आरेख]] (बीडीडी) के रूप में सूत्र के प्रतिनिधित्व के आधार पर तय किया जाता है।
SAT के कुछ प्रकार के बड़े यादृच्छिक संतोषजनक उदाहरणों को सर्वेक्षण प्रसार (एसपी) द्वारा हल किया जा सकता है।{{citation needed|date=December 2021}} विशेष रूप से [[हार्डवेयर डिज़ाइन]] और [[हार्डवेयर सत्यापन]] अनुप्रयोगों में, किसी दिए गए प्रस्ताव सूत्र की संतुष्टि और अन्य तार्किक गुणों को कभी-कभी [[द्विआधारी निर्णय आरेख]] (बीडीडी) के रूप में सूत्र के प्रतिनिधित्व के आधार पर तय किया जाता है।
Line 30: Line 30:
ये सभी व्यवहार SAT समाधान प्रतियोगिताओं में देखे जा सकते हैं।<ref>{{cite web|url=http://www.satcompetition.org/ |title=अंतर्राष्ट्रीय SAT प्रतियोगिता वेब पेज|access-date=2007-11-15}}</ref>
ये सभी व्यवहार SAT समाधान प्रतियोगिताओं में देखे जा सकते हैं।<ref>{{cite web|url=http://www.satcompetition.org/ |title=अंतर्राष्ट्रीय SAT प्रतियोगिता वेब पेज|access-date=2007-11-15}}</ref>


'''समानांतर सैट-समाधान'''


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


अंतर्राष्ट्रीय एसएटी सॉल्वर प्रतियोगिता में एक समानांतर ट्रैक है जो समानांतर एसएटी समाधान में हाल की प्रगति को दर्शाता है। 2016 में,<ref>{{cite web|url=https://baldur.iti.kit.edu/sat-competition-2016/index.php?cat=tracks|title=SAT Competition 2016|website=baldur.iti.kit.edu|access-date=2020-02-13}}</ref> 2017<ref>{{cite web|url=https://baldur.iti.kit.edu/sat-competition-2017/index.php?cat=tracks|title=SAT Competition 2017|website=baldur.iti.kit.edu|access-date=2020-02-13}}</ref> और 2018,<ref>{{cite web|url=http://sat2018.forsyte.tuwien.ac.at/index.php?cat=tracks|title=SAT Competition 2018|website=sat2018.forsyte.tuwien.ac.at|access-date=2020-02-13}}</ref> बेंचमार्क 24 [[सेंट्रल प्रोसेसिंग यूनिट]] के साथ एक साझा मेमोरी | साझा-मेमोरी सिस्टम पर चलाए गए थे, इसलिए वितरित मेमोरी या कई [[कईकोर प्रोसेसर]] के लिए सॉल्वर कम पड़ गए होंगे।
अंतर्राष्ट्रीय एसएटी सॉल्वर प्रतियोगिता में समानांतर ट्रैक है जो समानांतर एसएटी समाधान में हाल की प्रगति को दर्शाता है। 2016 में,<ref>{{cite web|url=https://baldur.iti.kit.edu/sat-competition-2016/index.php?cat=tracks|title=SAT Competition 2016|website=baldur.iti.kit.edu|access-date=2020-02-13}}</ref> 2017<ref>{{cite web|url=https://baldur.iti.kit.edu/sat-competition-2017/index.php?cat=tracks|title=SAT Competition 2017|website=baldur.iti.kit.edu|access-date=2020-02-13}}</ref> और 2018,<ref>{{cite web|url=http://sat2018.forsyte.tuwien.ac.at/index.php?cat=tracks|title=SAT Competition 2018|website=sat2018.forsyte.tuwien.ac.at|access-date=2020-02-13}}</ref> बेंचमार्क 24 [[सेंट्रल प्रोसेसिंग यूनिट]] के साथ साझा मेमोरी | साझा-मेमोरी सिस्टम पर चलाए गए थे, इसलिए वितरित मेमोरी या कई [[कईकोर प्रोसेसर]] के लिए सॉल्वर कम पड़ गए होंगे।


=== पोर्टफोलियो ===
=== पोर्टफोलियो ===
सामान्य तौर पर ऐसा कोई SAT सॉल्वर नहीं है जो सभी SAT समस्याओं पर अन्य सभी सॉल्वरों से बेहतर प्रदर्शन करता हो। एक एल्गोरिदम उन समस्या उदाहरणों के लिए अच्छा प्रदर्शन कर सकता है जिनसे अन्य लोग जूझ रहे हैं, लेकिन अन्य उदाहरणों के साथ यह बदतर प्रदर्शन करेगा। इसके अलावा, SAT उदाहरण को देखते हुए, यह अनुमान लगाने का कोई विश्वसनीय तरीका नहीं है कि कौन सा एल्गोरिदम इस उदाहरण को विशेष रूप से तेजी से हल करेगा। ये सीमाएँ समानांतर पोर्टफोलियो दृष्टिकोण को प्रेरित करती हैं। एक पोर्टफोलियो विभिन्न एल्गोरिदम या एक ही एल्गोरिदम के विभिन्न कॉन्फ़िगरेशन का एक सेट है। एक समानांतर पोर्टफोलियो में सभी सॉल्वर एक ही समस्या को हल करने के लिए अलग-अलग प्रोसेसर पर चलते हैं। यदि एक सॉल्वर समाप्त हो जाता है, तो पोर्टफोलियो सॉल्वर इस एक सॉल्वर के अनुसार समस्या को संतोषजनक या असंतोषजनक बताता है। अन्य सभी सॉल्वरों को समाप्त कर दिया गया है। विभिन्न प्रकार के सॉल्वरों को शामिल करके पोर्टफोलियो में विविधता लाने से, जिनमें से प्रत्येक समस्या के अलग-अलग सेट पर अच्छा प्रदर्शन करता है, सॉल्वर की मजबूती बढ़ जाती है।<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>
सामान्य तौर पर ऐसा कोई SAT सॉल्वर नहीं है जो सभी SAT समस्याओं पर अन्य सभी सॉल्वरों से बेहतर प्रदर्शन करता हो। एल्गोरिदम उन समस्या उदाहरणों के लिए अच्छा प्रदर्शन कर सकता है जिनसे अन्य लोग जूझ रहे हैं, लेकिन अन्य उदाहरणों के साथ यह बदतर प्रदर्शन करेगा। इसके अलावा, SAT उदाहरण को देखते हुए, यह अनुमान लगाने का कोई विश्वसनीय तरीका नहीं है कि कौन सा एल्गोरिदम इस उदाहरण को विशेष रूप से तेजी से हल करेगा। ये सीमाएँ समानांतर पोर्टफोलियो दृष्टिकोण को प्रेरित करती हैं। पोर्टफोलियो विभिन्न एल्गोरिदम या ही एल्गोरिदम के विभिन्न कॉन्फ़िगरेशन का सेट है। समानांतर पोर्टफोलियो में सभी सॉल्वर ही समस्या को हल करने के लिए अलग-अलग प्रोसेसर पर चलते हैं। यदि सॉल्वर समाप्त हो जाता है, तो पोर्टफोलियो सॉल्वर इस सॉल्वर के अनुसार समस्या को संतोषजनक या असंतोषजनक बताता है। अन्य सभी सॉल्वरों को समाप्त कर दिया गया है। विभिन्न प्रकार के सॉल्वरों को शामिल करके पोर्टफोलियो में विविधता लाने से, जिनमें से प्रत्येक समस्या के अलग-अलग सेट पर अच्छा प्रदर्शन करता है, सॉल्वर की मजबूती बढ़ जाती है।<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=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> इसे उस प्रदर्शन के लिए निचली सीमा खोजने के लिए डिज़ाइन किया गया था जो एक समानांतर SAT सॉल्वर प्रदान करने में सक्षम होना चाहिए। अनुकूलन की कमी के कारण बड़ी मात्रा में डुप्लिकेट कार्य के बावजूद, इसने साझा मेमोरी मशीन पर अच्छा प्रदर्शन किया। होर्डेसैट<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> कंप्यूटिंग नोड्स के बड़े समूहों के लिए एक समानांतर पोर्टफोलियो सॉल्वर है। यह अपने मूल में एक ही अनुक्रमिक सॉल्वर के अलग-अलग कॉन्फ़िगर किए गए उदाहरणों का उपयोग करता है। विशेष रूप से कठिन SAT उदाहरणों के लिए होर्डेसैट रैखिक स्पीडअप उत्पन्न कर सकता है और इसलिए रनटाइम को काफी कम कर सकता है।
समानांतर पोर्टफोलियो का दोष डुप्लिकेट कार्य की मात्रा है। यदि अनुक्रमिक सॉल्वरों में क्लॉज लर्निंग का उपयोग किया जाता है, तो समानांतर चलने वाले सॉल्वरों के बीच सीखे गए क्लॉज को साझा करने से डुप्लिकेट कार्य को कम किया जा सकता है और प्रदर्शन में वृद्धि हो सकती है। फिर भी, केवल सर्वोत्तम सॉल्वरों का पोर्टफोलियो समानांतर में चलाने से भी प्रतिस्पर्धी समानांतर सॉल्वर बन जाता है। ऐसे सॉल्वर का उदाहरण पीपीफ़ोलियो है।<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> इसे उस प्रदर्शन के लिए निचली सीमा खोजने के लिए डिज़ाइन किया गया था जो समानांतर SAT सॉल्वर प्रदान करने में सक्षम होना चाहिए। अनुकूलन की कमी के कारण बड़ी मात्रा में डुप्लिकेट कार्य के बावजूद, इसने साझा मेमोरी मशीन पर अच्छा प्रदर्शन किया। होर्डेसैट<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> कंप्यूटिंग नोड्स के बड़े समूहों के लिए समानांतर पोर्टफोलियो सॉल्वर है। यह अपने मूल में ही अनुक्रमिक सॉल्वर के अलग-अलग कॉन्फ़िगर किए गए उदाहरणों का उपयोग करता है। विशेष रूप से कठिन SAT उदाहरणों के लिए होर्डेसैट रैखिक स्पीडअप उत्पन्न कर सकता है और इसलिए रनटाइम को काफी कम कर सकता है।


हाल के वर्षों में समानांतर पोर्टफोलियो एसएटी सॉल्वरों ने अंतर्राष्ट्रीय एसएटी सॉल्वर प्रतियोगिताओं के समानांतर ट्रैक पर अपना दबदबा बना लिया है। ऐसे सॉल्वरों के उल्लेखनीय उदाहरणों में प्लिंगलिंग और पेनलेस-एमकॉमस्प्स शामिल हैं।<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" /> [[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=":1" /> [[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" />
ट्रींजलिंग  समानांतर सॉल्वर का उदाहरण है जो क्यूब-एंड-कॉनकर प्रतिमान लागू करता है। 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>
'''स्थानीय खोज'''
 
 
=== स्थानीय खोज ===
SAT समाधान के लिए एक समानांतर स्थानीय खोज एल्गोरिदम की दिशा में एक रणनीति विभिन्न प्रसंस्करण इकाइयों पर एक साथ कई चर फ़्लिप की कोशिश करना है।<ref>{{Citation|last=Roli|first=Andrea|title=Principles and Practice of Constraint Programming - CP 2002|chapter=Criticality and Parallelism in Structured SAT Instances|volume=2470|date=2002|pages=714–719|publisher=Springer Berlin Heidelberg|isbn=978-3-540-44120-5|doi=10.1007/3-540-46135-3_51|series=Lecture Notes in Computer Science}}</ref> दूसरा, उपर्युक्त पोर्टफोलियो दृष्टिकोण को लागू करना है, हालांकि क्लॉज साझा करना संभव नहीं है क्योंकि स्थानीय खोज सॉल्वर क्लॉज का उत्पादन नहीं करते हैं। वैकल्पिक रूप से, स्थानीय स्तर पर उत्पादित कॉन्फ़िगरेशन को साझा करना संभव है। जब कोई स्थानीय सॉल्वर अपनी खोज को फिर से शुरू करने का निर्णय लेता है तो इन कॉन्फ़िगरेशन का उपयोग नए प्रारंभिक कॉन्फ़िगरेशन के उत्पादन को निर्देशित करने के लिए किया जा सकता है।<ref>{{Citation|last1=Arbelaez|first1=Alejandro|title=Improving Parallel Local Search for SAT|date=2011|work=Lecture Notes in Computer Science|pages=46–60|publisher=Springer Berlin Heidelberg|isbn=978-3-642-25565-6|last2=Hamadi|first2=Youssef|doi=10.1007/978-3-642-25566-3_4|s2cid=14735849 }}</ref>


SAT समाधान के लिए  समानांतर स्थानीय खोज एल्गोरिदम की दिशा में  रणनीति विभिन्न प्रसंस्करण इकाइयों पर  साथ कई चर फ़्लिप की कोशिश करना है।<ref>{{Citation|last=Roli|first=Andrea|title=Principles and Practice of Constraint Programming - CP 2002|chapter=Criticality and Parallelism in Structured SAT Instances|volume=2470|date=2002|pages=714–719|publisher=Springer Berlin Heidelberg|isbn=978-3-540-44120-5|doi=10.1007/3-540-46135-3_51|series=Lecture Notes in Computer Science}}</ref> दूसरा, उपर्युक्त पोर्टफोलियो दृष्टिकोण को लागू करना है, हालांकि क्लॉज साझा करना संभव नहीं है क्योंकि स्थानीय खोज सॉल्वर क्लॉज का उत्पादन नहीं करते हैं। वैकल्पिक रूप से, स्थानीय स्तर पर उत्पादित कॉन्फ़िगरेशन को साझा करना संभव है। जब कोई स्थानीय सॉल्वर अपनी खोज को फिर से शुरू करने का निर्णय लेता है तो इन कॉन्फ़िगरेशन का उपयोग नए प्रारंभिक कॉन्फ़िगरेशन के उत्पादन को निर्देशित करने के लिए किया जा सकता है।<ref>{{Citation|last1=Arbelaez|first1=Alejandro|title=Improving Parallel Local Search for SAT|date=2011|work=Lecture Notes in Computer Science|pages=46–60|publisher=Springer Berlin Heidelberg|isbn=978-3-642-25565-6|last2=Hamadi|first2=Youssef|doi=10.1007/978-3-642-25566-3_4|s2cid=14735849 }}</ref>


== यह भी देखें ==
== यह भी देखें ==
* बूलियन संतुष्टि समस्या
* बूलियन संतुष्टि समस्या
* [[संतुष्टि मॉड्यूलो सिद्धांत]]
* [[संतुष्टि मॉड्यूलो सिद्धांत]]

Revision as of 23:47, 4 August 2023

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

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

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

सिंहावलोकन

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

Main article: DPLL algorithm

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

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

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

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

Main article: Conflict-driven clause learning

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

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

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

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

समानांतर सैट-समाधान

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

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

पोर्टफोलियो

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

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

फूट डालो और राज करो

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

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

स्थानीय खोज

SAT समाधान के लिए समानांतर स्थानीय खोज एल्गोरिदम की दिशा में रणनीति विभिन्न प्रसंस्करण इकाइयों पर साथ कई चर फ़्लिप की कोशिश करना है।[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=281555’