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

कुक-लेविन थ्योरम के रूप में जाने जाने वाले परिणाम के अनुसार, बूलियन सटिस्फाबिलिटी सामान्य रूप से एनपी-पूर्ण समस्या है। परिणामस्वरूप, केवल घातीय वर्स्ट केस कम्प्लेक्सिटी एल्गोरिदम ही ज्ञात हैं। इसके अतिरिक्त, 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, आदि के लिए मान) या फॉर्मूला असंतोषजनक होने पर असंतोषजनक क्लॉसेस का न्यूनतम सेट सहित अधिक जानकारी प्रदान कर सकते हैं।

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

डीपीएलएल सैट सॉल्वर सटिसफाईइंग असाइनमेंट की सर्च में परिवर्तनीय असाइनमेंट के (घातीय आकार के) स्पेस को ज्ञात करने के लिए व्यवस्थित बैकट्रैकिंग सर्च प्रक्रिया को नियोजित करता है। मूलरूपी सर्च प्रक्रिया 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" />

इसके विपरीत, पटुरी, पुडलक, साक्स एवं ज़ेन द्वारा पीपीएसजेड एल्गोरिदम जैसे यादृच्छिक एल्गोरिदम कुछ अनुमानों के अनुसार यादृच्छिक क्रम में वेरिएबल सेट करते हैं, उदाहरण के लिए सीमा-चौड़ाई रिज़ॉल्यूशन है। यदि अनुमानी को उचित सेटिंग नहीं प्राप्त होती है, तो वेरिएबल को यादृच्छिक रूप से असाइन किया जाता है। 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>

आधुनिक सैट सॉल्वर (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 में मिनिजिंक बाधा प्रोग्रामिंग प्रतियोगिताओं में स्वर्ण पदक जीते थे।

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

भिन्न-भिन्न सैट सॉल्वर भिन्न-भिन्न उदाहरणों को सरल या कठिन पाएंगे, एवं कुछ असंतोषजनकता प्रमाणित करने में एवं अन्य समाधान सर्च में उत्कृष्टता प्राप्त करेंगे। ये सभी बिहेवियर सैट समाधान प्रतियोगिताओं में देखे जा सकते हैं।<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" />  

अन्य-कालानुक्रमिक बैकट्रैकिंग के कारण, संघर्ष-संचालित खंड सीखने का समानांतरीकरण अधिक कठिन है। इस पर नियंत्रित करने का उपाय क्यूब एंड कॉनकर प्रतिमान है।<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> इसलिए इसका उपयोग समस्या को धीरे-धीरे कई उप-समस्याओं में विभाजित करने के लिए किया जाता है। ये उप-समस्याएँ सरल हैं अपितु अधिक हैं जो संघर्ष-संचालित समाधानकर्ता के लिए आदर्श रूप है। इसके अतिरिक्त आगे की सोच वाले समाधानकर्ता पूरी समस्या पर विचार करते हैं जबकि संघर्ष-प्रेरित समाधानकर्ता अधिक लोकल जानकारी के आधार पर निर्णय लेते हैं। घन चरण में तीन अनुमान सम्मिलित हैं। घनों में वेरिएबलों को निर्णय अनुमान के अनुसार चयन होता है। दिशा अनुमान यह सुनिश्चित करता है कि किस वेरिएबल असाइनमेंट (उचित या त्रुटिपूर्ण) को ज्ञात करना है। सटिसफाईइंग समस्या वाले विषयों में, सटिसफाईइंग शाखा का चयन लाभकारी होता है। कटऑफ अनुमान यह सुनिश्चित करता है कि कब क्यूब का विस्तार सं�