सैट सॉल्वर: Difference between revisions
From Vigyanwiki
No edit summary |
No edit summary |
||
| Line 20: | Line 20: | ||
{{main|कनफ्लिक्ट-ड्रिवेन क्लॉज़ लर्निंग}} | {{main|कनफ्लिक्ट-ड्रिवेन क्लॉज़ लर्निंग}} | ||
आधुनिक सैट सॉल्वर (2000 के दशक में विकसित) दो प्रकारों में आते हैं: कनफ्लिक्ट-ड्रिवेन एवं आगे की ओर देखने वाले। दोनों | आधुनिक सैट सॉल्वर (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 लाइनें हैं। आधुनिक | कनफ्लिक्ट-ड्रिवेन मिनीसैट, जो 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> | ||
'''पैरेलल सैट-सॉल्विंग''' | '''पैरेलल सैट-सॉल्विंग''' | ||
[[समानांतर एल्गोरिदम]] सैट सॉल्वर तीन श्रेणियों पोर्टफोलियो, [[फूट डालो और जीतो एल्गोरिथ्म|डिवाइड-एंड-कॉनकर एवं | [[समानांतर एल्गोरिदम|पैरेलल एल्गोरिदम]] सैट सॉल्वर तीन श्रेणियों पोर्टफोलियो, [[फूट डालो और जीतो एल्गोरिथ्म|डिवाइड-एंड-कॉनकर एवं पैरेलल लोकल सर्च एल्गोरिदम]] में हैं। पैरेलल पोर्टफोलियो के साथ, कई भिन्न-भिन्न सैट सॉल्वर साथ चलते हैं। उनमें से प्रत्येक सैट इन्सटेंस की कॉपी सॉल्व करता है, जबकि डिवाइड-एंड-कॉनकर एल्गोरिदम प्रोसेसर के मध्य समस्या को विभाजित करता है। लोकल सर्च एल्गोरिदम को पैरेलल करने के लिए विभिन्न एप्रोच सम्मिलित हैं। | ||
अंतर्राष्ट्रीय सैट सॉल्वर प्रतियोगिता में | अंतर्राष्ट्रीय सैट सॉल्वर प्रतियोगिता में पैरेलल ट्रैक है जो पैरेलल सैट समाधान में वर्तमान की प्रगति को प्रदर्शित करता है। 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 [[सेंट्रल प्रोसेसिंग यूनिट]] के साथ शेयर्ड-मेमोरी सिस्टम पर चलाए गए थे, इसलिए वितरित मेमोरी या कई [[कईकोर प्रोसेसर|कोर प्रोसेसर]] के लिए सॉल्वर कम पड़ गए थे। | ||
=== पोर्टफोलियो === | === पोर्टफोलियो === | ||
सामान्यतः ऐसा कोई सैट सॉल्वर नहीं है जो सभी सैट समस्याओं पर अन्य सभी सॉल्वरों से उत्तम प्रदर्शन करता हो। एल्गोरिदम उन समस्या उदाहरणों के लिए करेक्ट प्रदर्शन कर सकता है जिसके लिए अन्य लोग कनफ्लिक्ट कर रहे हैं, किन्तु अन्य उदाहरणों के साथ यह व्यर्थ प्रदर्शन करता है। इसके अतिरिक्त, सैट उदाहरण को देखते हुए, यह अनुमान लगाने का कोई विश्वसनीय उपाय नहीं है कि कौन सा एल्गोरिदम इस उदाहरण में विशेष रूप से तीव्रता से निवारण करेगा। ये सीमाएँ | सामान्यतः ऐसा कोई सैट सॉल्वर नहीं है जो सभी सैट समस्याओं पर अन्य सभी सॉल्वरों से उत्तम प्रदर्शन करता हो। एल्गोरिदम उन समस्या उदाहरणों के लिए करेक्ट प्रदर्शन कर सकता है जिसके लिए अन्य लोग कनफ्लिक्ट कर रहे हैं, किन्तु अन्य उदाहरणों के साथ यह व्यर्थ प्रदर्शन करता है। इसके अतिरिक्त, सैट उदाहरण को देखते हुए, यह अनुमान लगाने का कोई विश्वसनीय उपाय नहीं है कि कौन सा एल्गोरिदम इस उदाहरण में विशेष रूप से तीव्रता से निवारण करेगा। ये सीमाएँ पैरेलल पोर्टफोलियो एप्रोच को प्रेरित करती हैं। पोर्टफोलियो विभिन्न एल्गोरिदम या एल्गोरिदम के विभिन्न कॉन्फ़िगरेशन का सेट है। पैरेलल पोर्टफोलियो में सभी सॉल्वर समस्या का निवारण करने के लिए भिन्न-भिन्न प्रोसेसर पर चलते हैं। यदि सॉल्वर समाप्त हो जाता है, तो पोर्टफोलियो सॉल्वर इस सॉल्वर के अनुसार समस्या को सटिस्फाइयबल या अनसटिस्फाइयबल बताता है। अन्य सभी सॉल्वरों को समाप्त कर दिया गया है। विभिन्न प्रकार के सॉल्वरों को सम्मिलित करके पोर्टफोलियो में विविधता लाने से, जिनमें से प्रत्येक समस्या के भिन्न-भिन्न सेट पर करेक्ट प्रदर्शन करता है, सॉल्वर की पॉवर बढ़ जाती है।<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 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>. निर्णय अनुमानी चुनता है कि कौन से चर (सर्कल) निर्दिष्ट करने हैं। कटऑफ हेयुरिस्टिक द्वारा आगे की शाखाओं को रोकने का निर्णय लेने के बाद, सीडीसीएल का उपयोग करके आंशिक समस्याओं (आयत) को स्वतंत्र रूप से हल किया जाता है।]] | ||
| Line 47: | Line 47: | ||
अन्य-क्रोनोलॉजिकल बैकट्रैकिंग के कारण, कनफ्लिक्ट-ड्रिवेन खंड सीखने का समानांतरीकरण अधिक कठिन है। इस पर नियंत्रित करने का उपाय क्यूब एंड कॉनकर प्रतिमान है।<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> | ||
'''लोकल सर्च''' | '''लोकल सर्च''' | ||
Revision as of 20:20, 15 September 2023
कंप्यूटर विज्ञान एवं फॉर्मल मेथड्स में, सैट सॉल्वर कंप्यूटर प्रोग्राम है जिसका उद्देश्य बूलियन सेटिस्फिअबिलिटी प्रॉब्लम को सॉल्व करना है। बूलियन डेटा टाइप वेरिएबल, जैसे (x या y) एवं (x या y नहीं) पर फार्मूला इनपुट करने पर, सैट सॉल्वर आउटपुट देता है कि क्या फार्मूला सेटिसफीएबल है, जिसका अर्थ है कि x एवं y की पॉसिबल वैल्यूज हैं जो फॉर्मूले को ट्रू या अनसेटिसफीएबल बनाती हैं, जिसका अर्थ है कि x एवं y की ऐसी कोई वैल्यूज नहीं हैं। इस विषय में, x ट्रू होने पर फार्मूला सेटिसफीएबल होता है, इसलिए सॉल्वर को सेटिसफीएबल रिटर्न करना चाहिए। 1960 के दशक में सैट के लिए एल्गोरिदम के प्रारम्भ के पश्चात से, आधुनिक सैट सॉल्वर कुशलतापूर्वक कार्य करने के लिए अधिक संख्या में हयूरिस्टिक्स एवं प्रोग्राम ऑप्टिमाइजेशन को सम्मिलित करते हुए काम्प्लेक्स सॉफ़्टवेयर आर्टिफैक्ट्स में विकसित हो गए हैं।
कुक-लेविन थ्योरम के रूप में जाने जाने वाले परिणाम के अनुसार, बूलियन सटिस्फाबिलिटी सामान्य रूप से एनपी-पूर्ण समस्या है। परिणामस्वरूप, केवल घातीय वर्स्ट केस कम्प्लेक्सिटी एल्गोरिदम ही ज्ञात हैं। इसके अतिरिक्त, 2000 के दशक के समय सैट के लिए एफिशिएंट एवं स्केलेबल एल्गोरिदम विकसित किए गए, जिन्होंने हजारों वेरिएबल एवं लाखों बाधाओं से जुड़े समस्या उदाहरणों को स्वचालित रूप से निवारण करने की क्षमता में आकस्मिक प्रगति में योगदान दिया है।[1] सैट सॉल्वर प्रायः फार्मूला को कंजेक्टिव नॉरमल फॉर्म में परिवर्तित करके प्रारम्भ करते हैं। वे प्रायः डीपीएलएल एल्गोरिदम जैसे कोर एल्गोरिदम पर आधारित होते हैं, किन्तु इसमें कई एक्सटेंशन एवं सुविधाएं सम्मिलित होती हैं। अधिकांश सैट सॉल्वरों में टाइम-आउट सम्मिलित होता है, इसलिए वे करेक्ट समय में समाप्त हो जाएंगे, अपितु वे "अननोन" जैसे आउटपुट के साथ समाधान प्राप्त नहीं कर सकते है। प्रायः, सैट सॉल्वर केवल उत्तर ही नहीं देते हैं, अपितु यदि फॉर्मूला सटिसफाईइंग है तो उदाहरण असाइनमेंट (x, y, आदि के लिए मान) या फॉर्मूला असंतोषजनक होने पर असंतोषजनक क्लॉसेस का न्यूनतम सेट सहित अधिक जानकारी प्रदान कर सकते हैं।
आधुनिक सैट सॉल्वरों का सॉफ़्टवेयर वेरिफिकेशन, प्रोग्राम एनालिसिस, कन्सट्रैन्ट सॉल्विंग, आर्टिफिशियल इंटेलिजेंस, इलेक्ट्रॉनिक डिजाइन ऑटोमेशन एवं ऑपरेशन रिसर्च सहित क्षेत्रों पर महत्वपूर्ण प्रभाव पड़ा है। पावरफुल सॉल्वर फ्री एवं ओपन-सोर्स सॉफ़्टवेयर के रूप में सरलता से उपलब्ध हैं एवं कुछ प्रोग्रामिंग लैंग्वेज में निर्मित होते हैं जैसे कि सैट सॉल्वर को कंस्ट्रेंट लॉजिक प्रोग्रामिंग में बाधाओं के रूप में प्रदर्शित करना है।
अवलोकन
डीपीएलएल सॉल्वर
डीपीएलएल सैट सॉल्वर सटिसफाईइंग असाइनमेंट की सर्च में परिवर्तनीय असाइनमेंट के (घातीय आकार के) स्पेस को ज्ञात करने के लिए व्यवस्थित बैकट्रैकिंग सर्च प्रक्रिया को नियोजित करता है। मूलरूपी सर्च प्रक्रिया 1960 दशक के प्रारम्भ में दो प्राथमिक पेपर्स में प्रस्तावित की गई थी (नीचे रिफरेन्स देखें) एवं अब इसे सामान्यतः डेविस-पुटनम-लोगमैन-लवलैंड एल्गोरिदम (डीपीएलएल या डीएलएल) के रूप में जाना जाता है।[2][3] प्रैक्टिकल सैट समाधान के लिए कई आधुनिक अप्प्रोचेस डीपीएलएल एल्गोरिथ्म से प्राप्त हुए हैं एवं समान संरचना सम्मिलित करते हैं। प्रायः वे केवल सैट समस्याओं के कुछ क्लासेज की एफिशिएंसी में सुधार करते हैं जैसे कि टेक्निकल अनुप्रयोगों में प्रदर्शित होने वाले उदाहरण या यादृच्छिक रूप से उत्पन्न उदाहरण है।[4] सैद्धांतिक रूप से, एल्गोरिदम के डीपीएलएल फैमिली के लिए घातांकीय निचली सीमाएं प्रमाणित हो चुकी हैं।
जो एल्गोरिदम डीपीएलएल फैमिली का भाग नहीं हैं, उनमें स्टोकेस्टिक लोकल सर्च एल्गोरिदम सम्मिलित हैं। उदाहरण वॉकसैट है। स्टोकेस्टिक विधियां सटिसफाईइंग व्याख्या का प्रयास करती हैं किन्तु यह निष्कर्ष नहीं निकाल सकती हैं कि डीपीएलएल जैसे पूर्ण एल्गोरिदम के विपरीत, सैट उदाहरण असंतोषजनक है।[4]
इसके विपरीत, पटुरी, पुडलक, साक्स एवं ज़ेन द्वारा पीपीएसजेड एल्गोरिदम जैसे यादृच्छिक एल्गोरिदम कुछ अनुमानों के अनुसार रैंडमली वेरिएबल सेट करते हैं, उदाहरण के लिए बॉण्डेड विड्थ रिज़ॉल्यूशन है। यदि ह्यूरिस्टिक को करेक्ट सेटिंग नहीं प्राप्त होती है, तो वेरिएबल को यादृच्छिक रूप से असाइन किया जाता है। PPSZ एल्गोरिथ्म में 3-सैट के लिए runtime[clarify] होता है। यह 2019 तक इस समस्या के लिए सबसे प्रसिद्ध रनटाइम था, जब हैनसेन, कपलान, ज़मीर एवं ज़्विक ने रनटाइम 3-सैट के लिए संशोधन प्रकाशित किया, उत्तरार्द्ध वर्तमान में k के सभी मानों पर k-सैट के लिए सबसे फास्टेस्ट नोन एल्गोरिदम है। कई सटिसफाईइंग असाइनमेंट वाली सेटिंग में स्कोनिंग द्वारा रैंडमाइज्ड एल्गोरिदम की सीमा उत्तम है।[5][6][7]
सीडीसीएल सॉल्वर
आधुनिक सैट सॉल्वर (2000 के दशक में विकसित) दो प्रकारों में आते हैं: कनफ्लिक्ट-ड्रिवेन एवं आगे की ओर देखने वाले। दोनों एप्रोच डीपीएलएल से उत्पन हुए हैं।[4] कनफ्लिक्ट-ड्रिवेन सॉल्वर, जैसे कनफ्लिक्ट-ड्रिवेन क्लॉज लर्निंग (सीडीसीएल), एफिशिएंट कनफ्लिक्ट एनालिसिस, क्लॉज लर्निंग, अन्य-क्रोनोलॉजिकल बैकट्रैकिंग के साथ-साथ वाटचेड लिटरल्स यूनिट प्रोपोगेशन, अनुकूली शाखा एवं यादृच्छिक पुनरारंभ के साथ मूलरूपी डीपीएलएल सर्च एल्गोरिदम को बढ़ाते हैं। मूलरूपी व्यवस्थित सर्च के लिए ये अतिरिक्त अनुभवजन्य रूप से इलेक्ट्रॉनिक डिज़ाइन ऑटोमेशन (EDA) में उत्पन्न होने वाले बड़े सैट उदाहरणों के लिए आवश्यक दिखाए गए हैं।[8] सुप्रसिद्ध कार्यान्वयनों में ग्रास्प एल्गोरिथ्म सम्मिलित है I[9][10] लुक-फॉरवर्ड सॉल्वर्स ने विशेष रूप से रिडक्शन (यूनिट-क्लॉज प्रोपोगेशन से परे) एवं अनुमानों को सशक्त किया है, एवं वे सामान्यतः कठिन उदाहरणों पर कनफ्लिक्ट-ड्रिवेन सॉल्वरों की अपेक्षा में अधिक सशक्त होते हैं (जबकि कनफ्लिक्ट-ड्रिवेन सॉल्वर बड़े उदाहरणों पर अधिक उत्तम हो सकते हैं जिनके अंदर वास्तव में सरल उदाहरण होता है)।
कनफ्लिक्ट-ड्रिवेन मिनीसैट, जो 2005 सैट प्रतियोगिता में अपेक्षाकृत सफल रहा, में कोड की केवल 600 लाइनें हैं। आधुनिक पैरेलल सैट सॉल्वर मैनीसैट है।[11] यह समस्याओं के महत्वपूर्ण क्लासेज पर सुपर लीनियर स्पीड-अप प्राप्त कर सकता है। आगे बढ़ने वाले सॉल्वरों का उदाहरण मार्च_डीएल है, जिसने 2007 सैट प्रतियोगिता में पुरस्कार जीता था। गूगल के सीपी-सैट सॉल्वर, या-उपकरण के भाग, ने 2018, 2019, 2020 एवं 2021 में मिनिजिंक बाधा प्रोग्रामिंग प्रतियोगिताओं में स्वर्ण पदक जीते थे।
सैट के कुछ प्रकार के बड़े यादृच्छिक सटिसफाईइंग उदाहरणों का सर्वेक्षण प्रोपोगेशन (एसपी) द्वारा निवारण किया जा सकता है। विशेष रूप से हार्डवेयर डिज़ाइन एवं हार्डवेयर वेरिफिकेशन अनुप्रयोगों में, किसी दिए गए प्रस्ताव फार्मूला की संतुष्टि एवं अन्य लॉजिक गुणों को कभी-कभी द्विआधारी निर्णय आरेख (बीडीडी) के रूप में फार्मूला के प्रतिनिधित्व के आध