बूलियन संतुष्टि समस्या: Difference between revisions

Latest revision as of 10:13, 24 February 2023

तर्क और संगणक विज्ञान में, बूलियन संतुष्टि समस्या (कभी-कभी प्रस्तावित संतुष्टि समस्या और संक्षिप्त संतुष्टि, सैट या बी-सैट कहा जाता है) यह निर्धारित करने की समस्या है कि क्या कोई व्याख्या (तर्क) सम्मलित है जो किसी दिए गए बूलियन तर्क सूत्र (गणितीय तर्क) की संतुष्टि है। . दूसरे शब्दों में, यह पूछता है कि क्या किसी दिए गए बूलियन सूत्र के चर को लगातार ट्रू या फॉल्स मानों द्वारा इस तरह से प्रतिस्थापित किया जा सकता है कि सूत्र ट्रू का मूल्यांकन करता है। यदि यह स्थिति है, तो सूत्र को 'संतोषजनक' कहा जाता है। दूसरी ओर, यदि ऐसा कोई समनुदेशन सम्मलित नहीं है, तो सूत्र द्वारा व्यक्त किया गया सभी कार्य संभावित चर समनुदेशन के लिए औपचारिक तर्क में विरोधाभास # विरोधाभास है और सूत्र असंतोषजनक है। उदाहरण के लिए, सूत्र "a और ना ही b" संतुष्ट करने योग्य है क्योंकि कोई "a = ट्रू और b = फॉल्स" मान खोज सकता है, जो (a और ना ही b) = ट्रू। इसके विपरीत, "ए और ना ही ए " असंतोषजनक है।

सैट पहली समस्या है जो एनपी-पूर्ण सिद्ध हुई थी; कुक–लेविन प्रमेय देखें। इसका मतलब यह है कि जटिलता वर्ग एनपी (जटिलता) में सभी समस्याएं, जिसमें प्राकृतिक निर्णय और अनुकूलन समस्याओं की एक विस्तृत श्रृंखला सम्मलित है, को सैट के रूप में हल करना मुश्किल है। ऐसा कोई ज्ञात कलनविधि नहीं है जो प्रत्येक सैट समस्या को कुशलतापूर्वक हल करता हो, और सामान्यत: पर यह माना जाता है कि ऐसा कोई कलनविधि सम्मलित नहीं है; अभी तक यह विश्वास गणितीय रूप से सिद्ध नहीं हुआ है, और इस सवाल को हल करना कि क्या सैट के पास बहुपद-समय कलनविधि है, P बनाम NP समस्या के बराबर है, जो कंप्यूटिंग के सिद्धांत में एक प्रसिद्ध खुली समस्या है।

फिर भी, 2007 तक, ह्यूरिस्टिक सैट-कलनविधि समस्या के उदाहरणों को हल करने में सक्षम हैं जिनमें हजारों चर सम्मलित हैं और लाखों प्रतीकों से युक्त सूत्र,^[1]जो कई व्यावहारिक सैट समस्याओं के लिए पर्याप्त है, उदाहरण के लिए, कृत्रिम बुद्धिमता, विद्युत परिपथ प्रारुप,^[2] और स्वचालित प्रमेय सिद्ध करना।

परिभाषाएँ

एक प्रस्तावपरक तर्क सूत्र, जिसे बूलियन अभिव्यक्ति भी कहा जाता है, परिवर्ती (गणित), ऑपरेटरों और (तार्किक संयोजन, जिसे ∧ द्वारा भी दर्शाया गया है), या (तार्किक विच्छेदन, ∨), नहीं (निषेध, ¬), और कोष्ठकों से बनाया गया है। एक सूत्र को संतोषजनक कहा जाता है यदि इसके चरों को उपयुक्त तार्किक मान (अर्थात ट्रू, फॉल्स) निर्दिष्ट करके इसे ट्रू बनाया जा सकता हो। बूलियन संतुष्टि समस्या (सैट) को यह जांचने के लिए एक सूत्र दिया गया है कि यह संतोषजनक है या नहीं। कंप्यूटर विज्ञान के कई क्षेत्रों में यह निर्णय समस्या केंद्रीय महत्व की है, जिसमें सैद्धांतिक कंप्यूटर विज्ञान, संगणनात्मक जटिलता सिद्धांत,^[3]^[4] कलनविधि, कूटलेखन^[5]^[6] और कृत्रिम बुद्धि।^[7]^{[additional citation(s) needed]}

संयोजक सामान्य रूप

एक शाब्दिक या तो एक चर है (जिस स्थिति में इसे एक सकारात्मक शाब्दिक कहा जाता है) या एक चर का निषेध (एक नकारात्मक शाब्दिक कहा जाता है)। एक खंड शाब्दिक (या एक शाब्दिक) का संयोजन है। एक उपवाक्य को हॉर्न उपवाक्य कहा जाता है यदि उसमें अधिक से अधिक एक धनात्मक अक्षर हो। एक सूत्र संयोजन सामान्य रूप (सीएनएफ) में है यदि यह खंड (या एक एकल खंड) का संयोजन है। उदाहरण के लिए, $x 1$ एक सकारात्मक शाब्दिक है, $\neg x 2$ एक नकारात्मक शाब्दिक है, $x 1 \lor \neg x 2$ एक खंड है। सूत्र $(x 1 \lor \neg x 2) \land (\neg x 1 \lor x 2 \lor x 3) \land \neg x 1$ संयोजन सामान्य रूप में है; इसका पहला और तीसरा उपवाक्य हॉर्न उपवाक्य हैं, लेकिन इसका दूसरा उपवाक्य नहीं है। सूत्र संतोषजनक है, x चुनकर₁= गलत, एक्स₂= फॉल्स, और x₃ मनमाने ढंग से, क्योंकि (फॉल्स ∨ ¬फॉल्स) ∧ (¬फॉल्स ∨ फॉल्स ∨ x₃) ∧ ¬फॉल्स (फॉल्स ∨ ट्रू) ∧ (ट्रू ∨ फॉल्स ∨ x) का मूल्यांकन करता है₃) ∧ ट्रू, और बदले में ट्रू ∧ ट्रू ∧ ट्रू (अर्थात ट्रू के लिए)। इसके विपरीत, सीएनएफ सूत्र a ∧ ¬a, जिसमें एक शाब्दिक के दो खंड सम्मलित हैं, असंतुष्ट है, क्योंकि a=ट्रू या a=फॉल्स के लिए यह ट्रू ∧ ¬ट्रू (अर्थात, फॉल्स) या फॉल्स ∧ ¬फॉल्स (अर्थात , फिर से फॉल्स), क्रमशः।

सैट समस्या के कुछ संस्करणों के लिए, यह एक सामान्यीकृत संयोजक सामान्य रूप सूत्र, अर्थात की धारणा को परिभाषित करने के लिए उपयोगी है। मनमाने ढंग से कई सामान्यीकृत खंडों के संयोजन के रूप में, बाद वाला फॉर्म का है $R (l 1,..., l n)$ कुछ बूलियन फंगक्शन R और (साधारण) शाब्दिक के लिए $l i$ . अनुमत बूलियन कार्यों के विभिन्न सेट विभिन्न समस्या संस्करणों की ओर ले जाते हैं। एक उदाहरण के रूप में, R(¬x,a,b) एक सामान्यीकृत खंड है, और R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z) एक सामान्यीकृत खंड है संयुक्त सामान्य रूप से। इस सूत्र का उपयोग #बिल्कुल-1 3-संतोषणीयता के साथ किया जाता है, जिसमें R टर्नरी ऑपरेटर होता है जो ट्रू होता है जब इसका कोई एक तर्क होता है। बूलियन बीजगणित (संरचना) के नियमों का उपयोग करते हुए, प्रत्येक प्रस्तावपरक तर्क सूत्र को समतुल्य संयोजन सामान्य रूप में परिवर्तित किया जा सकता है, जो कि, चूंकि, घातीय रूप से लंबा हो सकता है। उदाहरण के लिए, सूत्र को बदलना (x₁∧y₁) ∨ (x₂∧y₂) ∨ ... ∨ (x_n∧y_n) संयोजन सामान्य रूप में उत्पन्न

(x 1 \lor x 2 \lor \dots \lor x n) \land

(y 1 \lor x 2 \lor \dots \lor x n) \land

(x 1 \lor y 2 \lor \dots \lor x n) \land

(y 1 \lor y 2 \lor \dots \lor x n) \land ... \land

(x 1 \lor x 2 \lor \dots \lor y n) \land

(y 1 \lor x 2 \lor \dots \lor y n) \land

(x 1 \lor y 2 \lor \dots \lor y n) \land

(y 1 \lor y 2 \lor \dots \lor y n)

;

जबकि पूर्व 2 चर के n संयोजनों का संयोजन है, बाद वाले में 2ⁿ n चरों के उपवाक्य होते हैं।

चूंकि,टेसीटिन परिवर्तन के उपयोग के साथ, हम मूल प्रस्तावपरक तर्क सूत्र के आकार में लंबाई रैखिक के साथ एक समतुल्य संयुग्मन सामान्य रूप सूत्र पा सकते हैं।

जटिलता

सैट पहली ज्ञात एनपी-पूर्ण समस्या थी, जैसा कि 1971 में टोरंटो विश्वविद्यालय में स्टीफन कुक द्वारा सिद्ध किया गया था^[8] और स्वतंत्र रूप से 1973 में रूसी एकेडमी ऑफ साइंसेज # द एकेडमी ऑफ साइंसेज ऑफ यूएसएसआर में लियोनिद लेविन द्वारा।^[9] उस समय तक, एनपी-पूर्ण समस्या की अवधारणा सम्मलित ही नहीं थी। उदाहरण दिखाता है कि कैसे जटिलता वर्ग एनपी (जटिलता) में हर निर्णय समस्या सीएनएफ के लिए सैट समस्या में कमी (जटिलता) हो सकती है^{[note 1]} सूत्र, जिन्हें कभी-कभी सीएनएफ सैट कहा जाता है। कुक के रिडक्शन का एक उपयोगी गुण यह है कि यह स्वीकृत उत्तरों की संख्या को सुरक्षित रखता है। उदाहरण के लिए, यह तय करना कि क्या किसी दिए गए आरेख (असतत गणित) में आरेख रंग# शीर्ष् रंग 3-कलरिंग एनपी में एक और समस्या है; यदि किसी आरेख में 17 मान्य 3-रंग हैं, तो कुक-लेविन कटौती द्वारा निर्मित सैट सूत्र में 17 संतोषजनक कार्य होंगे।

एनपी-पूर्णता केवल सबसे खराब स्थिति के कार्य अवधि को संदर्भित करती है। व्यावहारिक अनुप्रयोगों में आने वाले कई उदाहरणों को और अधिक तेज़ी से हल किया जा सकता है। नीचे सैट को हल करने के लिए #कलनविधि देखें।

3-संतोषजनकता

3-सैट उदाहरण

(x \lor x \lor y) \land (\neg x \lor \neg y \lor \neg y) \land (\neg x \lor y \lor y)

एक क्लिक समस्या में कमी। हरे कोने एक 3-क्लिक बनाते हैं और संतोषजनक समनुदेशन x=फॉल्स, y=ट्रू के अनुरूप होते हैं।

मनमाने सूत्रों के लिए संतुष्टि की समस्या की तरह, संयोजन सामान्य रूप में एक सूत्र की संतुष्टि का निर्धारण करना जहां प्रत्येक खंड अधिकतम तीन शाब्दिकों तक सीमित है, एनपी-पूर्ण भी है; इस समस्या को 3-सैट, 3सीएनएफ सैट, या 3-संतोषजनकता कहा जाता है।

अप्रतिबंधित सैट समस्या को 3-सैट तक कम करने के लिए, प्रत्येक खंड को रूपांतरित करें $l 1 \lor \dots \lor l n$ के संयोजन के लिए $n - 2$ खंड

(l 1 \lor l 2 \lor x 2) \land

(\neg x 2 \lor l 3 \lor x 3) \land

(\neg x 3 \lor l 4 \lor x 4) \land \dots \land

(\neg x n - 3 \lor l n - 2 \lor x n - 2) \land

(\neg x n - 2 \lor l n - 1 \lor l n)

जहाँ $x 2, \dots , x n - 2$ ताजा चर हैं जो कहीं और नहीं होते हैं। यद्यपि दो सूत्र तार्किक रूप से समतुल्य नहीं हैं, वे समान्य: हैं। सभी खंडों को बदलने से उत्पन्न होने वाला सूत्र अपने मूल से अधिक से अधिक 3 गुना लंबा है, अर्थात लंबाई वृद्धि बहुपद है।^[10] 3-सैट कार्प की 21 एनपी-पूर्ण समस्याओं में से एक है, और यह सिद्ध करने के लिए प्रारंभिक बिंदु के रूप में प्रयोग किया जाता है कि अन्य समस्याएं भी एनपी कठिन हैं।^{[note 2]} यह 3-सैट से दूसरी समस्या में बहुपद-समय में कमी के द्वारा किया जाता है। एक समस्या का एक उदाहरण जहां इस पद्धति में उपयोग किया गया है, क्लिक समस्या है: एक सीएनएफ सूत्र दिया गया है जिसमें c खंड सम्मलित हैं, संबंधित ग्राफ (असतत गणित) में प्रत्येक शाब्दिक के लिए एक शीर्ष होता है, और प्रत्येक दो गैर-विरोधाभासी के बीच एक किनारा होता है^{[note 3]} विभिन्न खंडों से शाब्दिक, सीएफ। चित्र। आरेख में एक c-क्लिक है यदि और केवल यदि सूत्र संतोषजनक है।^[11] शॉनिंग (1999) के कारण एक सरल यादृच्छिक कलनविधि है जो समय में चलता है (4/3)ⁿ जहां n 3-सैट प्रस्ताव में चरों की संख्या है, और 3-सैट को सही ढंग से तय करने की उच्च संभावना के साथ सफल होता है।^[12] घातीय समय परिकल्पना का दावा है कि कोई भी कलनविधि 3-सैट (या वास्तव में किसी भी के लिए के-सैट) को हल नहीं कर सकता है $k>2$ ) में $exp(o (n))$ समय (अर्थात, n में घातीय से मौलिक रूप से तेज़)।

सेलमैन, मिशेल, और लेवेस्क (1996) अपने आकार के मापदंडों के आधार पर बेतरतीब ढंग से उत्पन्न 3-सैट सूत्रों की कठिनाई पर अनुभवजन्य डेटा देते हैं। कठिनाई को डीपीएलएल कलनविधि द्वारा की गई संख्या पुनरावर्ती संकेत में मापा जाता है। उन्होंने एक चरण संक्रमण क्षेत्र की पहचान लगभग निश्चित रूप से संतोषजनक से लगभग निश्चित रूप से असंतोषजनक सूत्र के खंड-दर-चर अनुपात में लगभग 4.26 पर की।^[13] 3-संतोषजनकता को k-संतोषजनकता (k-सैट, k-सीएनएफ-सैट) के लिए सामान्यीकृत किया जा सकता है, जब सीएनएफ में सूत्रों को 'k' अक्षर तक के प्रत्येक खंड के साथ माना जाता है।^{[citation needed]} चूंकि, किसी भी k ≥ 3 के लिए, यह समस्या न तो 3-सैट से आसान हो सकती है और न ही सैट से कठिन, और बाद के दो NP-पूर्ण हैं, इसलिए k-सैट होना चाहिए।

कुछ लेखक k-सैट को 'बिल्कुल k शाब्दिक' के साथ सीएनएफ सूत्र तक सीमित रखते हैं।^{[citation needed]} यह प्रत्येक खंड के रूप में एक अलग जटिलता वर्ग की ओर नहीं ले जाता है $l 1 \lor \dots \lor l j$ with j <k लिटरल को निर्धारित डमी चर के साथ पैडेड किया जा सकता है $l 1 \lor \dots \lor l j \lor d j +1 \lor \dots \lor d k$ . सभी खंडों को भरने के बाद, 2^k-1 अतिरिक्त खंड^{[note 4]} केवल यह सुनिश्चित करने के लिए संलग्न किया जाता है $d 1 = \dots = d k =FALSE$ संतोषजनक कार्य मिल सकता है। चूँकि k सूत्र की लंबाई पर निर्भर नहीं करता है, इसलिए अतिरिक्त खंड लंबाई में निरंतर वृद्धि करते हैं। उसी कारण से, इससे कोई फर्क नहीं पड़ता कि ' समरूप शाब्दिक' को खंडों में अनुमति दी जाती है, जैसा कि $\neg x \lor \neg y \lor \neg y$ .

== सैट == के विशेष स्थितियों में।

संयोजक सामान्य रूप

संयोजक सामान्य रूप (विशेष रूप से 3 शाब्दिक प्रति खंड के साथ) को अधिकांशत: सैट सूत्रों के लिए विहित प्रतिनिधित्व माना जाता है। जैसा कि ऊपर दिखाया गया है, सामान्य सैट समस्या 3-सैट तक कम हो जाती है, इस रूप में सूत्रों के लिए संतुष्टि का निर्धारण करने की समस्या।

वियोगात्मक सामान्य रूप

सैट नगण्य है यदि सूत्र उन लोगों तक सीमित हैं जो वियोगात्मक सामान्य रूप में हैं, अर्थात, वे शाब्दिक संयोजनों के संयोजन हैं। इस तरह का एक सूत्र वास्तव में संतोषजनक है यदि और केवल यदि इसके संयोजनों में से कम से कम एक संतोषजनक है, और एक संयोजन संतोषजनक है यदि और केवल यदि इसमें कुछ चर के लिए x और ना ही x दोनों सम्मलित नहीं हैं। x इसे रैखिक समय में चेक किया जा सकता है। इसके अतिरिक्त, यदि वे पूर्ण वियोगात्मक सामान्य रूप में होने के लिए प्रतिबंधित हैं, जिसमें प्रत्येक चर प्रत्येक संयुग्मन में ठीक एक बार दिखाई देता है, तो उन्हें निरंतर समय में चेक किया जा सकता है (प्रत्येक संयुग्मन एक संतोषजनक समनुदेशन का प्रतिनिधित्व करता है)। लेकिन सामान्य सैट समस्या को अलग करने वाले सामान्य रूप में परिवर्तित करने में घातीय समय और स्थान लग सकता है; उदाहरण के लिए संयोजन सामान्य रूपों के लिए #परिभाषा घातीय झटका उदाहरण में ∧ और ∨ का आदान-प्रदान करें।

बिल्कुल-1 3-संतोषजनकता

बायाँ: शेफ़र द्वारा 3-सैट खंड़ x ∨ y ∨ z की कमी। 'र' का परिणाम है ट्रू (1) यदि इसका एक तर्क सही है, और फॉल्स (0) अन्यथा। x,y,z के मानों के सभी 8 संयोजनों की जांच की जाती है, प्रति पंक्ति एक। ताजा चर a,...,f सभी खंडों को संतुष्ट करने के लिए चुना जा सकता है (बिल्कुल एक green प्रत्येक R के लिए तर्क) पहली पंक्ति को छोड़कर सभी पंक्तियों में, जहाँ x ∨ y ∨ z फॉल्स है। 'दाहिना:' समान गुणों वाला एक सरल अपचयन।

3-संतोषजनक समस्या का एक प्रकार एक-इन-थ्री 3-सैट है (जिसे 1-इन-3-सैट और ठीक-ठीक 1 3-सैट के रूप में भी जाना जाता है)।

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

एक-इन-थ्री 3-सैट, इसके सकारात्मक स्थितियों के साथ, मानक संदर्भ में एनपी-पूर्ण समस्या "LO4" के रूप में सूचीबद्ध है, संगणक और अव्यावहारिकता: ए गाइड टू द थ्योरी ऑफ एनपी-पूर्णता माइकल आर. गैरी और डेविड एस. जॉनसन द्वारा। एक-में-तीन 3-सैट को थॉमस जेरोम शेफर द्वारा शेफर के द्विबीज प्रमेय के एक विशेष स्थितियों के रूप में एनपी-पूर्ण सिद्ध किया गया है, जो दावा करता है कि बूलियन संतुष्टि को एक निश्चित तरीके से सामान्यीकृत करने वाली कोई भी समस्या या तो कक्षा p में है या एनपी- है। पूरा।^[14] शेफ़र 3-सैट से एक-इन-थ्री 3-सैट तक एक आसान बहुपद-समय की कमी की अनुमति देते हुए एक निर्माण देता है। मान लीजिए (x या y या z) 3सीएनएफ सूत्र में एक खंड है। इस खंड का अनुकरण करने के लिए उपयोग किए जाने वाले छह नए बूलियन चर a, b, c, d, e, और f जोड़ें और कोई अन्य नहीं। तब सूत्र R(x,a,d) ∧ R(y,b,d) ∧ R(a,b,e) ∧ R(c,d,f) ∧ R(z,c,फॉल्स) द्वारा संतोषजनक है ताज़ा चरों की कुछ विन्यास यदि और केवल यदि x, y, या z में से कम से कम एक सत्य है, चित्र देखें (बाएं)। इस प्रकार एम खंड और एन चर के साथ किसी भी 3-सैट उदाहरण को 5 एम खंड और एन + 6 एम चर के साथ तीन 3-सैट उदाहरण में एक समतुल्य में परिवर्तित किया जा सकता है।^[15] एक और कटौती में केवल चार नए चर और तीन खंड सम्मलित हैं: R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z), चित्र देखें (दाएं)।

नहीं-सब-बराबर 3-संतोषजनक

एक अन्य संस्करण नहीं-सब-बराबर 3-संतोषजनक समस्या है (जिसे एनएई 3सैट भी कहा जाता है)। तीन शाब्दिक प्रति खंड के साथ एक संयोजन सामान्य रूप दिया गया है, समस्या यह निर्धारित करने के लिए है कि क्या चर के लिए एक समनुदेशन सम्मलित है जैसे कि किसी भी खंड में सभी तीन शाब्दिक समान सत्य मूल्य नहीं हैं। यह समस्या एनपी-पूर्ण है, भले ही शेफर के द्विबीजपत्री प्रमेय द्वारा कोई निषेध प्रतीक स्वीकार न किया गया हो।^[14]

रैखिक सैट

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

2-संतुष्टि

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

हॉर्न-संतुष्टि

हॉर्न खंड के दिए गए संयोजन की संतुष्टि की समस्या को हॉर्न-संतोषजनकता या हॉर्न-सैट कहा जाता है। इसे बहुपद समय में यूनिट प्रसार कलनविधि के एक चरण द्वारा हल किया जा सकता है, जो हॉर्न खंड के सेट के एकल न्यूनतम मॉडल का उत्पादन करता है डब्ल्यू.आर.टी. ट्रू को निर्दिष्ट शाब्दिक सेट)। हॉर्न-संतोषजनकता P पूर्ण है। इसे P (जटिलता) के रूप में देखा जा सकता है। बूलियन संतुष्टि समस्या के P संस्करण। इसके अतिरिक्त, बहुपद समय में परिमाणित हॉर्न सूत्र की सच्चाई का निर्धारण किया जा सकता है। ^[17] हॉर्न खण्ड़ दिलचस्प हैं क्योंकि वे अन्य चरों के एक सेट से एक चर की प्रविष्टि को व्यक्त करने में सक्षम हैं। दरअसल, ऐसा ही एक खंड ¬x₁ ∨ ... ∨ ¬x_n ∨ y को x के रूप में फिर से लिखा जा सकता है₁ ∧ ... ∧ x_n → y, अर्थात, यदि x₁,...,x_n सभी ट्रू हैं, तो y को भी ट्रू होना चाहिए।

हॉर्न सूत्र की श्रेणी का एक सामान्यीकरण नाम बदलने योग्य-हॉर्न सूत्र का है, जो कि उन सूत्र का सेट है जिन्हें कुछ चरों को उनके संबंधित नकार के साथ बदलकर हॉर्न रूप में रखा जा सकता है। उदाहरण के लिए, (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₂ ∨ x₃) ∧ ¬x₁ हॉर्न सूत्र नहीं है, लेकिन इसका नाम बदलकर हॉर्न सूत्र (x₁ ∨ ¬x₂) ∧ (¬x₁ ∨ x₂ ∨ ¬y₃) ∧ ¬x₁ y पेश करके₃ x की अस्वीकृति के रूप में₃. इसके विपरीत, (x₁ ∨ ¬x₂ ∨ ¬x₃) ∧ (¬x₁ ∨ x₂ ∨ x₃) ∧ ¬x₁ एक हॉर्न सूत्र की ओर जाता है। ऐसे प्रतिस्थापन के अस्तित्व की जाँच रैखिक समय में की जा सकती है; इसलिए, ऐसे सूत्रों की संतुष्टि P में है क्योंकि पहले इस प्रतिस्थापन को करके और फिर परिणामी हॉर्न सूत्र की संतुष्टि की जाँच करके इसे हल किया जा सकता है।

एक्सओआर-संतुष्टि

Solving an एक्सओआर-सैट example
by Gaussian elimination

Given formula
("⊕" means एक्सओआर, the red clause is optional)
(a⊕c⊕d) ∧ (b⊕¬c⊕d) ∧ (a⊕b⊕¬d) ∧ (a⊕¬b⊕¬c) ∧ (¬a⊕b⊕c)

Equation system
("1" means ट्रू, "0" means फॉल्स)
Each clause leads to one equation.
	a	⊕		c	⊕		d	= 1
	b	⊕	¬	c	⊕		d	= 1
	a	⊕		b	⊕	¬	d	= 1
	a	⊕	¬	b	⊕	¬	c	= 1
¬	a	⊕		b	⊕		c	≃ 1

Normalized equation system
using properties of Boolean rings (¬x=1⊕x, x⊕x=0)
a	⊕	c	⊕	d	= 1
b	⊕	c	⊕	d	= 0
a	⊕	b	⊕	d	= 0
a	⊕	b	⊕	c	= 1
a	⊕	b	⊕	c	≃ 0
(If the red equation is present, it contradicts
the last black one, so the system is unsolvable.
Therefore, Gauss' algorithm is
used only for the black equations.)

Associated coefficient matrix

a	b	c	d		line

1	0	1	1	1	A
0	1	1	1	0	B
1	1	0	1	0	C
1	1	1	0	1	D

Transforming to echelon form

a	b	c	d		operation

1	0	1	1	1	A
1	1	0	1	0	C
1	1	1	0	1	D
0	1	1	1	0	B (swapped)

1	0	1	1	1	A
0	1	1	0	1	E = C⊕A
0	1	0	1	0	F = D⊕A
0	1	1	1	0	B

1	0	1	1	1	A
0	1	1	0	1	E
0	0	1	1	1	G = F⊕E
0	0	0	1	1	H = B⊕E

Transforming to diagonal form

a	b	c	d		operation

1	0	1	0	0	I = A⊕H
0	1	1	0	1	E
0	0	1	0	0	J = G⊕H
0	0	0	1	1	H

1	0	0	0	0	K = I⊕J
0	1	0	0	1	L = E⊕J
0	0	1	0	0	J
0	0	0	1	1	H

Solution:
If the red clause is present:	Unsolvable
Else:	a = 0 = फॉल्स
	b = 1 = ट्रू
	c = 0 = फॉल्स
	d = 1 = ट्रू
As a consequence:
R(a,c,d) ∧ R(b,¬c,d) ∧ R(a,b,¬d) ∧ R(a,¬b,¬c) ∧ R(¬a,b,c)
is not 1-in-3-सैटisfiable,
while (a ∨ c ∨ d) ∧ (b ∨ ¬c ∨ d) ∧ (a ∨ b ∨ ¬d) ∧ (a ∨ ¬b ∨ ¬c)
is 3-सैटisfiable with a=c=फॉल्स and b=d=ट्रू.

एक और विशेष मामला समस्याओं का वर्ग है जहां प्रत्येक खंड में (स्पष्ट) या ऑपरेटरों के अतिरिक्त एक्सओआर (अर्थात अपवर्जित ) होता है।^{[note 5]} यह p (जटिलता वर्ग) में है, चूंकि एक्सओआर-सैट सूत्र को रैखिक समीकरण मॉड 2 की प्रणाली के रूप में भी देखा जा सकता है, और गॉसियन उन्मूलन द्वारा घन काल में हल किया जा सकता है;^[18] उदाहरण के लिए डिब्बे में देखें। यह पुनर्रचना बूलियन बीजगणित (संरचना)#बूलियन वल्य पर आधारित है, और यह तथ्य कि अंकगणितीय सापेक्ष दो एक परिमित क्षेत्र बनाते हैं। चूँकि एक एक्सओआर b एक्सओआर c ट्रू का मूल्यांकन करता है यदि और केवल यदि {a,b,c} के ठीक 1 या 3 सदस्य ट्रू हैं, तो किसी दिए गए सीएनएफ सूत्र के लिए 1-इन-3-सैट समस्या का प्रत्येक समाधान भी एक समाधान है एक्सओआर-3-सैट समस्या का, और बदले में एक्सओआर-3-सैट का प्रत्येक समाधान 3-सैट, cf का समाधान है। चित्र परिणामस्वरूप, प्रत्येक सीएनएफ सूत्र के लिए, सूत्र द्वारा परिभाषित एक्सओआर-3-सैट समस्या को हल करना संभव है, और परिणाम के आधार पर अनुमान लगाया जाता है कि 3-सैट समस्या हल करने योग्य है, या 1-में-3- सैट समस्या हल करने योग्य नहीं है।

बशर्ते कि p = एनपी समस्या, न तो 2-, न ही हॉर्न-, न ही एक्सओआर-संतुष्टि, सैट के विपरीत एनपी-पूर्ण है।

शेफर का द्विभाजन प्रमेय

उपरोक्त प्रतिबंध (सीएनएफ, 2सीएनएफ, 3सीएनएफ, हॉर्न, एक्सओआर-सैट) विचार किए गए सूत्रों को उपसूत्र के संयोजन के रूप में बाध्य करते हैं; प्रत्येक प्रतिबंध सभी उपसूत्रों के लिए एक विशिष्ट रूप बताता है: उदाहरण के लिए, केवल द्विआधारी खंड 2सीएनएफ में उपसूत्र हो सकते हैं।

शेफर के द्विभाजन प्रमेय में कहा गया है कि, बूलियन कार्यों के लिए किसी भी प्रतिबंध के लिए जिसका उपयोग इन उपसूत्रों को बनाने के लिए किया जा सकता है, संबंधित संतुष्टि समस्या p या एनपी-पूर्ण में है। 2सीएनएफ, हॉर्न, और एक्सओआर-सैट सूत्रों की संतुष्टि की P में सदस्यता इस प्रमेय के विशेष स्थितियों हैं।^[14]

निम्न तालिका सैट के कुछ सामान्य रूपों का सारांश देती है।


Code	Name	Restrictions	Requirements	Class
3सैट	3- संतोषणीयता	प्रत्येक खंड में 3 शाब्दिक हैं.	कम से कम एक शाब्दिक ट्रू होना चाहिए	एनपीसी
2सैट	2- संतोषणीयता	प्रत्येक खंड में 2 शाब्दिक हैं	कम से कम एक शाब्दिक ट्रू होना चाहिए	P
1-in-3-सैट	वास्तव में-1 3-सैट	प्रत्येक खंड में 3 शाब्दिक हैं	कम से कम एक शाब्दिक ट्रू होना चाहिए	एनपीसी
1-in-3-सैट+	वास्तव में-1 सकारात्मक 3-सैट	प्रत्येक खंड में 3 सकारात्मक शाब्दिक होते हैं।	एक शाब्दिक बिल्कुल ट्रू होना चाहिए.	एनपीसी
एनएई 3सैट	सर्व-समान नहीं 3-संतोषणीयता	प्रत्येक खंड में 3 शाब्दिक हैं	या तो एक या दो शाब्दिक ट्रू होने चाहिए।	एनपीसी
एनएई 3सैट+	ना ही-सब-बराबर सकारात्मक 3-सैट	प्रत्येक खंड में 3 सकारात्मक शाब्दिक होते हैं।	या तो एक या दो शाब्दिक ट्रू होने चाहिए।	एनपीसी
पीएल-सैट	समतलीय सैट	घटना ग्राफ (क्लॉज-वेरिएबल ग्राफ) प्लेनर है।	कम से कम एक शाब्दिक ट्रू होना चाहिए।	एनपीसी
एल सैट	रेखीय सैट	प्रत्येक खंड में 3 अक्षर होते हैं, अधिकांश एक दूसरे खंड पर प्रतिच्छेद करते हैं, और प्रतिच्छेदन बिल्कुल एक शाब्दिक है।	कम से कम एक शाब्दिक ट्रू होना चाहिए।	एनपीसी
हॉर्न-सैट	हॉर्न संतोषणीयता	हॉर्न क्लॉज (ज्यादा से ज्यादा एक सकारात्मक शाब्दिक है)	कम से कम एक शाब्दिक ट्रू होना चाहिए।	P
एक्सओआर-सैट	एक्सओआर संतोषणीयता	प्रत्येक क्लॉज में OR के अतिरिक्त एक्सओआर ऑपरेशन होते हैं।	सभी शाब्दिकों का एक्सओआर ट्रू होना चाहिए।	P

सैट का विस्तार

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

संतुष्टि की समस्या और अधिक कठिन हो जाती है यदि सभी के लिए (∀) और वहाँ (∃) परिमाणक (तर्क) दोनों के लिए बूलियन चर को बाँधने की अनुमति हो। ऐसी अभिव्यक्ति का एक उदाहरण होगा $\forall x \forall y \exists z (x \lor y \lor z) \land (\neg x \lor \neg y \lor \neg z)$ ; यह मान्य है, क्योंकि x और y के सभी मानों के लिए, z का एक उपयुक्त मान पाया जा सकता है, अर्थात। z=ट्रू यदि x और y दोनों फॉल्स हैं, और z=फॉल्स अन्य। सैट स्वयं (मौन रूप से) केवल ∃ क्वांटिफायर का उपयोग करता है। यदि इसके अतिरिक्त केवल ∀ परिमाणकों की अनुमति है, तथाकथित 'पुनरुक्ति (तर्क) समस्या' प्राप्त की जाती है, जो सह-एनपी-पूर्ण है। यदि दोनों परिमाणकों की अनुमति है, तो समस्या को 'मात्राबद्ध बूलियन सूत्र समस्या' ('क्यूबीएफ') कहा जाता है, जिसे पीएसपीएसीई-पूर्ण दिखाया जा सकता है। यह व्यापक रूप से माना जाता है कि एनपी में किसी भी समस्या की तुलना में पीएसपीएसीई-पूर्ण समस्याएं सख्ती से कठिन हैं, चूंकि यह अभी तक सिद्ध नहीं हुआ है। अत्यधिक समानांतर p प्रणाली का उपयोग करके, एयुबीएफ-सैट समस्याओं को रैखिक समय में हल किया जा सकता है।^[20] सामान्य सैट पूछता है कि क्या कम से कम एक परिवर्तनीय समनुदेशन है जो सूत्र को सत्य बनाता है। विभिन्न प्रकार के प्रकारांतर ऐसे समनुदेशन की संख्या से निपटते हैं:

एमएजी-सैट पूछता है कि क्या सभी समनुदेशन्स में से अधिकांश सूत्र को ट्रू बनाते हैं। यह pp (जटिलता) के लिए पूर्ण माना जाता है, एक संभाव्य वर्ग।
स्पष्ट-सैट|#सैट, गिनती की समस्या कि कितने चर समनुदेशन एक सूत्र को संतुष्ट करते हैं, एक गिनती की समस्या है, निर्णय की समस्या नहीं है, और स्पष्ट-P-पूर्ण।
अद्वितीय सैट^[21] यह निर्धारित करने की समस्या है कि क्या किसी सूत्र में ठीक एक नियत कार्य है। यह यूएस (जटिलता) के लिए पूर्ण है,^[22] एक गैर-नियतात्मक बहुपद समय ट्यूरिंग मशीन द्वारा हल की जा सकने वाली समस्याओं का वर्णन करने वाली जटिलता वर्ग, जो तब स्वीकार करती है जब वास्तव में एक गैर-नियतात्मक स्वीकार्य पथ होता है और अन्यथा अस्वीकार करता है।
स्पष्ट-सैट वह नाम है जो संतुष्टि समस्या को दिया जाता है जब निविष्ट अधिकतम एक संतोषजनक समनुदेशन वाले सूत्र के लिए संतोषजनक कार्य होता है। समस्या को यूसैट भी कहा जाता है।^[23] स्पष्ट-सैट के लिए एक सुलझाने वाली कलनविधि को कई संतोषजनक समनुदेशन वाले सूत्र पर अंतहीन पाशन सहित किसी भी व्यवहार को प्रदर्शित करने की अनुमति है। चूंकि यह समस्या आसान लगती है, वैलेंट और वज़ीरानी के पास वैलेंट-वज़ीरानी प्रमेय है^[24] कि यदि इसे हल करने के लिए एक व्यावहारिक (अर्थात परिबद्ध-त्रुटि संभाव्य बहुपद। यादृच्छिक बहुपद-समय) कलनविधि है, तो एनपी (जटिलता वर्ग) में सभी समस्याओं को आसानी से हल किया जा सकता है।
मैक्स-सैट, अधिकतम संतुष्टि की समस्या, सैट का एपएनपी (जटिलता) सामान्यीकरण है। यह अधिकतम संख्या में खंडों के लिए पूछता है जो किसी भी समनुदेशन से संतुष्ट हो सकते हैं। इसमें कुशल सन्निकटन कलनविधि हैं, लेकिन एनपी-कठिन को ठीक से हल करना है। इससे भी बदतर, यह एपीएक्स-पूर्ण है, जिसका अर्थ है कि इस समस्या के लिए कोई बहुपद-समय सन्निकटन योजना (पीटीएएस) नहीं है जब तक कि p = एनपी न हो।
डब्ल्यूएम-सैट न्यूनतम वजन का एक समनुदेशन खोजने की समस्या है जो एक एकदिष्ट बूलियन सूत्र (अर्थात बिना किसी निषेध के एक सूत्र) को संतुष्ट करता है। समस्या के निविष्ट में प्रस्तावात्मक चर के भार दिए गए हैं। समनुदेशन का वजन सही चर के वजन का योग है। वह समस्या एनपी-पूर्ण है (थ देखें। 1 का ^[25]).

अन्य सामान्यीकरणों में प्रथम-क्रम विधेय- और द्वितीय-क्रम तर्क, बाधा संतुष्टि समस्याओं, 0-1 पूर्णांक प्रोग्रामिंग के लिए संतुष्टि सम्मलित है।

एक संतोषजनक समनुदेशन ढूँढना

जबकि सैट एक निर्णय समस्या है, संतोषजनक समनुदेशन खोजने की खोज समस्या सैट तक कम हो जाती है। अर्थात्, प्रत्येक कलनविधि जो सही ढंग से उत्तर देता है कि क्या सैट का एक उदाहरण हल करने योग्य है, एक संतोषजनक समनुदेशन खोजने के लिए उपयोग किया जा सकता है। सबसे पहले दिए गए सूत्र Φ पर प्रश्न पूछा जाता है। यदि उत्तर नहीं है, तो सूत्र संतोषजनक नहीं है। अन्यथा, प्रश्न आंशिक रूप से तत्काल सूत्र Φप्रतिस्थापन (तर्क) पर पूछा जाता है|{x₁=ट्रू}, अर्थात Φ पहले चर x के साथ₁ ट्रू द्वारा प्रतिस्थापित किया गया, और तदनुसार सरलीकृत किया गया। यदि उत्तर हाँ है, तो x₁= ट्रू, अन्यथा x₁= फॉल्स है। अन्य चरों के मान बाद में उसी तरह पाए जा सकते हैं। कुल मिलाकर, कलनविधि के n+1 रन आवश्यक हैं, जहां n Φ में अलग-अलग चर की संख्या है।

इस संपत्ति का उपयोग जटिलता सिद्धांत में कई प्रमेयों में किया जाता है:

NP ⊆ P/poly ⇒ PH = Σ₂ (कार्प-लिप्टन प्रमेय)

NP ⊆ BPP ⇒ NP = RP

P = NP ⇒ FP = FNP

सैट को हल करने के लिए कलनविधि

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

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

यह भी देखें

अतृप्त कोर
संतोषजनक मॉड्यूल सिद्धांत
तीव्र-सत
प्लानर सैट
कार्लोफ-ज़्विक कलनविधि
सर्किट संतुष्टि

↑ The SAT problem for arbitrary formulas is NP-complete, too, since it is easily shown to be in NP, and it cannot be easier than SAT for CNF formulas.
↑ i.e. at least as hard as every other problem in NP. A decision problem is NP-complete if and only if it is in NP and is NP-hard.
↑ i.e. such that one literal is not the negation of the other
↑ viz. all maxterms that can be built with $d 1,\dots, d k$ , except $d 1 \lor\dots\lor d k$
↑ Formally, generalized conjunctive normal forms with a ternary boolean function R are employed, which is TRUE just if 1 or 3 of its arguments is. An input clause with more than 3 literals can be transformed into an equisatisfiable conjunction of clauses á 3 literals similar to above; i.e. XOR-SAT can be reduced to XOR-3-SAT.

बाहरी संबंध

सैट Game: try solving a Boolean सैटisfiability problem yourself
The international सैट competition website
International Conference on Theory and Applications of सैटisfiability Testing
Journal on सैटisfiability, Boolean Modeling and Computation
सैट Live, an aggregate website for research on the सैटisfiability problem
Yearly evaluation of Maxसैट solvers

संदर्भ

↑ ^1.0 ^1.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.
↑ Hong, Ted; Li, Yanjing; Park, Sung-Boem; Mui, Diana; Lin, David; Kaleq, Ziyad Abdel; Hakim, Nagib; Naeimi, Helia; Gardner, Donald S.; Mitra, Subhasish (November 2010). "QED: Quick Error Detection tests for effective post-silicon validation". 2010 IEEE International Test Conference: 1–10. doi:10.1109/TEST.2010.5699215. ISBN 978-1-4244-7206-2. S2CID 7909084.
↑ Karp, Richard M. (1972). "Reducibility Among Combinatorial Problems" (PDF). In Raymond E. Miller; James W. Thatcher (eds.). Complexity of Computer Computations. New York: Plenum. pp. 85–103. ISBN 0-306-30707-3. Archived from the original (PDF) on 2011-06-29. Retrieved 2020-05-07. Here: p.86
↑ Aho, Alfred V.; Hopcroft, John E.; Ullman, Jeffrey D. (1974). The Design and Analysis of Computer Algorithms. Addison-Wesley. p. 403. ISBN 0-201-00029-6.
↑ Massacci, Fabio; Marraro, Laura (2000-02-01). "Logical Cryptanalysis as a SAT Problem". Journal of Automated Reasoning. 24 (1): 165–203. doi:10.1023/A:1006326723002. S2CID 3114247.
↑ Mironov, Ilya; Zhang, Lintao (2006). Biere, Armin; Gomes, Carla P. (eds.). "Applications of SAT Solvers to Cryptanalysis of Hash Functions". Theory and Applications of Satisfiability Testing — SAT 2006. Lecture Notes in Computer Science. Springer. 4121: 102–115. doi:10.1007/11814948_13. ISBN 978-3-540-37207-3.
↑ Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.
↑ Cook, Stephen A. (1971). "The Complexity of Theorem-Proving Procedures" (PDF). Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158. CiteSeerX 10.1.1.406.395. doi:10.1145/800157.805047. S2CID 7573663. Archived (PDF) from the original on 2022-10-09.
↑ Levin, Leonid (1973). "Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)". Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii). 9 (3): 115–116. (pdf) (in Russian), translated into English by Trakhtenbrot, B. A. (1984). "A survey of Russian approaches to perebor (brute-force searches) algorithms". Annals of the History of Computing. 6 (4): 384–400. doi:10.1109/MAHC.1984.10036. S2CID 950581.
↑ Aho, Hopcroft & Ullman (1974), Theorem 10.4.
↑ Aho, Hopcroft & Ullman (1974), Theorem 10.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. Archived (PDF) from the original on 2022-10-09.
↑ Selman, Bart; Mitchell, David; Levesque, Hector (1996). "Generating Hard Satisfiability Problems". Artificial Intelligence. 81 (1–2): 17–29. CiteSeerX 10.1.1.37.7362. doi:10.1016/0004-3702(95)00045-3.
↑ ^14.0 ^14.1 ^14.2 Schaefer, Thomas J. (1978). "The complexity of satisfiability problems" (PDF). Proceedings of the 10th Annual ACM Symposium on Theory of Computing. San Diego, California. pp. 216–226. CiteSeerX 10.1.1.393.8951. doi:10.1145/800133.804350.
↑ Schaefer (1978), p. 222, Lemma 3.5.
↑ Arkin, Esther M.; Banik, Aritra; Carmi, Paz; Citovsky, Gui; Katz, Matthew J.; Mitchell, Joseph S. B.; Simakov, Marina (2018-12-11). "Selecting and covering colored points". Discrete Applied Mathematics (in English). 250: 75–86. doi:10.1016/j.dam.2018.05.011. ISSN 0166-218X.
↑ Buning, H.K.; Karpinski, Marek; Flogel, A. (1995). "Resolution for Quantified Boolean Formulas". Information and Computation. Elsevier. 117 (1): 12–18. doi:10.1006/inco.1995.1025.
↑ Moore, Cristopher; Mertens, Stephan (2011), The Nature of Computation, Oxford University Press, p. 366, ISBN 9780199233212.
↑ ^19.0 ^19.1 R. E. Bryant, S. M. German, and M. N. Velev, Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions, in Analytic Tableaux and Related Methods, pp. 1–13, 1999.
↑ Alhazov, Artiom; Martín-Vide, Carlos; Pan, Linqiang (2003). "Solving a PSPACE-Complete Problem by Recognizing P Systems with Restricted Active Membranes". Fundamenta Informaticae. 58: 67–77. Here: Sect.3, Thm.3.1
↑ Blass, Andreas; Gurevich, Yuri (1982-10-01). "On the unique satisfiability problem". Information and Control. 55 (1): 80–88. doi:10.1016/S0019-9958(82)90439-9. ISSN 0019-9958.
↑ "Complexity Zoo:U - Complexity Zoo". complexityzoo.uwaterloo.ca. Archived from the original on 2019-07-09. Retrieved 2019-12-05.
↑ Kozen, Dexter C. (2006). "Supplementary Lecture F: Unique Satisfiability". Theory of Computation. Texts in Computer Science (in English). Springer. p. 180. ISBN 9781846282973.
↑ Valiant, L.; Vazirani, V. (1986). "NP is as easy as detecting unique solutions" (PDF). Theoretical Computer Science. 47: 85–93. doi:10.1016/0304-3975(86)90135-0.
↑ Buldas, Ahto; Lenin, Aleksandr; Willemson, Jan; Charnamord, Anton (2017). Obana, Satoshi; Chida, Koji (eds.). "Simple Infeasibility Certificates for Attack Trees". Advances in Information and Computer Security. Lecture Notes in Computer Science (in English). Springer International Publishing. 10418: 39–55. doi:10.1007/978-3-319-64200-0_3. ISBN 9783319642000.
↑ Gi-Joon Nam; Sakallah, K. A.; Rutenbar, R. A. (2002). "A new FPGA detailed routing approach via search-based Boolean satisfiability" (PDF). IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 21 (6): 674. doi:10.1109/TCAD.2002.1004311.
↑ Selsam, Daniel; Lamm, Matthew; Bünz, Benedikt; Liang, Percy; de Moura, Leonardo; Dill, David L. (11 March 2019). "Learning a SAT Solver from Single-Bit Supervision". arXiv:1802.03685 [cs.AI].
↑ "The international SAT Competitions web page". Retrieved 2007-11-15.

अग्रिम पठन

(by date of publication)

Garey, Michael R.; Johnson, David S. (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman. pp. A9.1: LO1–LO7, pp. 259–260. ISBN 0-7167-1045-5.
Marques-Silva, J.; Glass, T. (1999). "Combinational equivalence checking using satisfiability and recursive learning". Design, Automation and Test in Europe Conference and Exhibition, 1999. Proceedings (Cat. No. PR00078) (PDF). p. 145. doi:10.1109/DATE.1999.761110. ISBN 0-7695-0078-1. Archived (PDF) from the original on 2022-10-09.
Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). "Bounded Model Checking Using Satisfiability Solving". Formal Methods in System Design. 19: 7–34. doi:10.1023/A:1011276507260. S2CID 2484208.
Giunchiglia, E.; Tacchella, A. (2004). Giunchiglia, Enrico; Tacchella, Armando (eds.). Theory and Applications of Satisfiability Testing. Lecture Notes in Computer Science. Vol. 2919. doi:10.1007/b95238. ISBN 978-3-540-20851-8. S2CID 31129008.
Babic, D.; Bingham, J.; Hu, A. J. (2006). "B-Cubing: New Possibilities for Efficient SAT-Solving" (PDF). IEEE Transactions on Computers. 55 (11): 1315. doi:10.1109/TC.2006.175. S2CID 14819050.
Rodriguez, C.; Villagra, M.; Baran, B. (2007). "Asynchronous team algorithms for Boolean Satisfiability" (PDF). 2007 2nd Bio-Inspired Models of Network, Information and Computing Systems. pp. 66–69. doi:10.1109/BIMNICS.2007.4610083. S2CID 15185219.
Gomes, Carla P.; Kautz, Henry; Sabharwal, Ashish; Selman, Bart (2008). "Satisfiability Solvers". In Harmelen, Frank Van; Lifschitz, Vladimir; Porter, Bruce (eds.). Handbook of knowledge representation. Foundations of Artificial Intelligence. Vol. 3. Elsevier. pp. 89–134. doi:10.1016/S1574-6526(07)03002-7. ISBN 978-0-444-52211-5.
Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.
Knuth, Donald E. (2022). "Chapter 7.2.2.2: Satifiability". The Art of Computer Programming. Vol. 4B: Combinatorial Algorithms, Part 2. Addison-Wesley Professional. pp. 185–369. ISBN 978-0-201-03806-4.

This article includes material from a column in the ACM SIGDA e-newsletter by Prof. Karem Sakallah
Original text is available here

[10] The SAT problem for arbitrary formulas is NP-complete, too, since it is easily shown to be in NP, and it cannot be easier than SAT for CNF formulas.

[12] .e. at least as hard as every other problem in NP. A decision problem is NP-complete if and only if it is in NP and is NP-hard.

[13] .e. such that one literal is not the negation of the other

[17] viz. all maxterms that can be built with $d 1,\dots, d k$ , except $d 1 \lor\dots\lor d k$

[22] Formally, generalized conjunctive normal forms with a ternary boolean function R are employed, which is TRUE just if 1 or 3 of its arguments is. An input clause with more than 3 literals can be transformed into an equisatisfiable conjunction of clauses á 3 literals similar to above; i.e. XOR-SAT can be reduced to XOR-3-SAT.

[Codish.Ohrimenko.Stuckey.2007-1] 1.0 ^1.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] Hong, Ted; Li, Yanjing; Park, Sung-Boem; Mui, Diana; Lin, David; Kaleq, Ziyad Abdel; Hakim, Nagib; Naeimi, Helia; Gardner, Donald S.; Mitra, Subhasish (November 2010). "QED: Quick Error Detection tests for effective post-silicon validation". 2010 IEEE International Test Conference: 1–10. doi:10.1109/TEST.2010.5699215. ISBN 978-1-4244-7206-2. S2CID 7909084.

[3] Karp, Richard M. (1972). "Reducibility Among Combinatorial Problems" (PDF). In Raymond E. Miller; James W. Thatcher (eds.). Complexity of Computer Computations. New York: Plenum. pp. 85–103. ISBN 0-306-30707-3. Archived from the original (PDF) on 2011-06-29. Retrieved 2020-05-07. Here: p.86

[4] Aho, Alfred V.; Hopcroft, John E.; Ullman, Jeffrey D. (1974). The Design and Analysis of Computer Algorithms. Addison-Wesley. p. 403. ISBN 0-201-00029-6.

[5] Massacci, Fabio; Marraro, Laura (2000-02-01). "Logical Cryptanalysis as a SAT Problem". Journal of Automated Reasoning. 24 (1): 165–203. doi:10.1023/A:1006326723002. S2CID 3114247.

[6] Mironov, Ilya; Zhang, Lintao (2006). Biere, Armin; Gomes, Carla P. (eds.). "Applications of SAT Solvers to Cryptanalysis of Hash Functions". Theory and Applications of Satisfiability Testing — SAT 2006. Lecture Notes in Computer Science. Springer. 4121: 102–115. doi:10.1007/11814948_13. ISBN 978-3-540-37207-3.

[7] Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE. 103 (11): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID 10190144.

[8] Cook, Stephen A. (1971). "The Complexity of Theorem-Proving Procedures" (PDF). Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158. CiteSeerX 10.1.1.406.395. doi:10.1145/800157.805047. S2CID 7573663. Archived (PDF) from the original on 2022-10-09.

[9] Levin, Leonid (1973). "Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)". Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii). 9 (3): 115–116. (pdf) (in Russian), translated into English by Trakhtenbrot, B. A. (1984). "A survey of Russian approaches to perebor (brute-force searches) algorithms". Annals of the History of Computing. 6 (4): 384–400. doi:10.1109/MAHC.1984.10036. S2CID 950581.

[FOOTNOTEAhoHopcroftUllman1974Theorem_10.4-11] Aho, Hopcroft & Ullman (1974), Theorem 10.4.

[FOOTNOTEAhoHopcroftUllman1974Theorem_10.5-14] Aho, Hopcroft & Ullman (1974), Theorem 10.5.

[Schoning.1999-15] 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. Archived (PDF) from the original on 2022-10-09.

[16] Selman, Bart; Mitchell, David; Levesque, Hector (1996). "Generating Hard Satisfiability Problems". Artificial Intelligence. 81 (1–2): 17–29. CiteSeerX 10.1.1.37.7362. doi:10.1016/0004-3702(95)00045-3.

[schaefer-18] 14.0 ^14.1 ^14.2 Schaefer, Thomas J. (1978). "The complexity of satisfiability problems" (PDF). Proceedings of the 10th Annual ACM Symposium on Theory of Computing. San Diego, California. pp. 216–226. CiteSeerX 10.1.1.393.8951. doi:10.1145/800133.804350.

[FOOTNOTESchaefer1978222,_Lemma_3.5-19] Schaefer (1978), p. 222, Lemma 3.5.

[20] Arkin, Esther M.; Banik, Aritra; Carmi, Paz; Citovsky, Gui; Katz, Matthew J.; Mitchell, Joseph S. B.; Simakov, Marina (2018-12-11). "Selecting and covering colored points". Discrete Applied Mathematics (in English). 250: 75–86. doi:10.1016/j.dam.2018.05.011. ISSN 0166-218X.

[buningkarpinski-21] Buning, H.K.; Karpinski, Marek; Flogel, A. (1995). "Resolution for Quantified Boolean Formulas". Information and Computation. Elsevier. 117 (1): 12–18. doi:10.1006/inco.1995.1025.

[23] Moore, Cristopher; Mertens, Stephan (2011), The Nature of Computation, Oxford University Press, p. 366, ISBN 9780199233212.

[Bryant.German.Velev.1999-24] 19.0 ^19.1 R. E. Bryant, S. M. German, and M. N. Velev, Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions, in Analytic Tableaux and Related Methods, pp. 1–13, 1999.

[25] Alhazov, Artiom; Martín-Vide, Carlos; Pan, Linqiang (2003). "Solving a PSPACE-Complete Problem by Recognizing P Systems with Restricted Active Membranes". Fundamenta Informaticae. 58: 67–77. Here: Sect.3, Thm.3.1

[26] Blass, Andreas; Gurevich, Yuri (1982-10-01). "On the unique satisfiability problem". Information and Control. 55 (1): 80–88. doi:10.1016/S0019-9958(82)90439-9. ISSN 0019-9958.

[27] "Complexity Zoo:U - Complexity Zoo". complexityzoo.uwaterloo.ca. Archived from the original on 2019-07-09. Retrieved 2019-12-05.

[28] Kozen, Dexter C. (2006). "Supplementary Lecture F: Unique Satisfiability". Theory of Computation. Texts in Computer Science (in English). Springer. p. 180. ISBN 9781846282973.

[29] Valiant, L.; Vazirani, V. (1986). "NP is as easy as detecting unique solutions" (PDF). Theoretical Computer Science. 47: 85–93. doi:10.1016/0304-3975(86)90135-0.

[30] Buldas, Ahto; Lenin, Aleksandr; Willemson, Jan; Charnamord, Anton (2017). Obana, Satoshi; Chida, Koji (eds.). "Simple Infeasibility Certificates for Attack Trees". Advances in Information and Computer Security. Lecture Notes in Computer Science (in English). Springer International Publishing. 10418: 39–55. doi:10.1007/978-3-319-64200-0_3. ISBN 9783319642000.

[31] Gi-Joon Nam; Sakallah, K. A.; Rutenbar, R. A. (2002). "A new FPGA detailed routing approach via search-based Boolean satisfiability" (PDF). IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 21 (6): 674. doi:10.1109/TCAD.2002.1004311.

[32] Selsam, Daniel; Lamm, Matthew; Bünz, Benedikt; Liang, Percy; de Moura, Leonardo; Dill, David L. (11 March 2019). "Learning a SAT Solver from Single-Bit Supervision". arXiv:1802.03685 [cs.AI].

[33] "The international SAT Competitions web page". Retrieved 2007-11-15.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[note 1]

[10]

[note 2]

[note 3]

[11]

[12]

[13]

[note 4]

[14]

[15]

[16]

[17]

[note 5]

[18]

[19]

[20]

[21]

[22]

[23]

[24]

[25]

[26]

[27]

[28]

@@ Line 1: / Line 1: @@
 {{Redirect|3SAT|मध्य यूरोपीय टेलीविजन नेटवर्क|3sat}}
 {{short description|Problem of determining if a Boolean formula could be made true}}
-[[तर्क]] और [[Index.php?title= संगणक विज्ञान|संगणक विज्ञान]] में, बूलियन [[संतुष्टि]] समस्या (कभी-कभी प्रस्तावित संतुष्टि समस्या और संक्षिप्त संतुष्टि, सैट या बी-सैट कहा जाता है) यह निर्धारित करने की समस्या है कि क्या कोई [[व्याख्या (तर्क)]] मौजूद है जो किसी दिए गए [[बूलियन तर्क]] [[सूत्र (गणितीय तर्क)]] की संतुष्टि है। . दूसरे शब्दों में, यह पूछता है कि क्या किसी दिए गए बूलियन सूत्र के चर को लगातार ट्रू या फॉल्स मानों द्वारा इस तरह से प्रतिस्थापित किया जा सकता है कि सूत्र ट्रू का मूल्यांकन करता है। यदि यह स्थिति है, तो सूत्र को 'संतोषजनक' कहा जाता है। दूसरी ओर, यदि ऐसा कोई समनुदेशन मौजूद नहीं है, तो सूत्र द्वारा व्यक्त किया गया सभी कार्य संभावित चर समनुदेशन के लिए औपचारिक तर्क में विरोधाभास # विरोधाभास है और सूत्र ''असंतोषजनक'' है। उदाहरण के लिए, सूत्र "''a'' और ना ही ''b"'' संतुष्ट करने योग्य है क्योंकि कोई "''a'' = ट्रू और ''b'' = फॉल्स" मान खोज सकता है, जो (''a'' और ना ही ''b'') = ट्रू। इसके विपरीत, "''ए'' और ना ही ''ए'' " असंतोषजनक है।
+[[तर्क]] और [[Index.php?title= संगणक विज्ञान|संगणक विज्ञान]] में, बूलियन [[संतुष्टि]] समस्या (कभी-कभी प्रस्तावित संतुष्टि समस्या और संक्षिप्त संतुष्टि, सैट या बी-सैट कहा जाता है) यह निर्धारित करने की समस्या है कि क्या कोई [[व्याख्या (तर्क)]] सम्मलित है जो किसी दिए गए [[बूलियन तर्क]] [[सूत्र (गणितीय तर्क)]] की संतुष्टि है। . दूसरे शब्दों में, यह पूछता है कि क्या किसी दिए गए बूलियन सूत्र के चर को लगातार ट्रू या फॉल्स मानों द्वारा इस तरह से प्रतिस्थापित किया जा सकता है कि सूत्र ट्रू का मूल्यांकन करता है। यदि यह स्थिति है, तो सूत्र को 'संतोषजनक' कहा जाता है। दूसरी ओर, यदि ऐसा कोई समनुदेशन सम्मलित नहीं है, तो सूत्र द्वारा व्यक्त किया गया सभी कार्य संभावित चर समनुदेशन के लिए औपचारिक तर्क में विरोधाभास # विरोधाभास है और सूत्र ''असंतोषजनक'' है। उदाहरण के लिए, सूत्र "''a'' और ना ही ''b"'' संतुष्ट करने योग्य है क्योंकि कोई "''a'' = ट्रू और ''b'' = फॉल्स" मान खोज सकता है, जो (''a'' और ना ही ''b'') = ट्रू। इसके विपरीत, "''ए'' और ना ही ''ए'' " असंतोषजनक है।
-सैट पहली समस्या है जो एनपी-पूर्ण साबित हुई थी; कुक–लेविन प्रमेय देखें। इसका मतलब यह है कि जटिलता वर्ग [[एनपी (जटिलता)]] में सभी समस्याएं, जिसमें प्राकृतिक निर्णय और अनुकूलन समस्याओं की एक विस्तृत श्रृंखला शामिल है, को सैट के रूप में हल करना मुश्किल है। ऐसा कोई ज्ञात कलनविधि नहीं है जो प्रत्येक सैट समस्या को कुशलतापूर्वक हल करता हो, और आमतौर पर यह माना जाता है कि ऐसा कोई कलनविधि मौजूद नहीं है; अभी तक यह विश्वास गणितीय रूप से सिद्ध नहीं हुआ है, और इस सवाल को हल करना कि क्या सैट के पास बहुपद-समय कलनविधि है, P बनाम NP समस्या के बराबर है, जो कंप्यूटिंग के सिद्धांत में एक प्रसिद्ध खुली समस्या है।
+सैट पहली समस्या है जो एनपी-पूर्ण सिद्ध हुई थी; कुक–लेविन प्रमेय देखें। इसका मतलब यह है कि जटिलता वर्ग [[एनपी (जटिलता)]] में सभी समस्याएं, जिसमें प्राकृतिक निर्णय और अनुकूलन समस्याओं की एक विस्तृत श्रृंखला सम्मलित है, को सैट के रूप में हल करना मुश्किल है। ऐसा कोई ज्ञात कलनविधि नहीं है जो प्रत्येक सैट समस्या को कुशलतापूर्वक हल करता हो, और सामान्यत: पर यह माना जाता है कि ऐसा कोई कलनविधि सम्मलित नहीं है; अभी तक यह विश्वास गणितीय रूप से सिद्ध नहीं हुआ है, और इस सवाल को हल करना कि क्या सैट के पास बहुपद-समय कलनविधि है, P बनाम NP समस्या के बराबर है, जो कंप्यूटिंग के सिद्धांत में एक प्रसिद्ध खुली समस्या है।
-फिर भी, 2007 तक, ह्यूरिस्टिक सैट-कलनविधि समस्या के उदाहरणों को हल करने में सक्षम हैं जिनमें हजारों चर शामिल हैं और <!---"clauses" hasn't been introduced here:--->लाखों प्रतीकों से युक्त सूत्र,<ref name="Codish.Ohrimenko.Stuckey.2007"/>जो कई व्यावहारिक सैट समस्याओं के लिए पर्याप्त है, उदाहरण के लिए, [[Index.php?title=कृत्रिम बुद्धिमता|कृत्रिम बुद्धिमता]], [[Index.php?title= विद्युत परिपथ प्रारुप|विद्युत परिपथ प्रारुप]],<ref>{{Cite journal|last1=Hong|first1=Ted|last2=Li|first2=Yanjing|last3=Park|first3=Sung-Boem|last4=Mui|first4=Diana|last5=Lin|first5=David|last6=Kaleq|first6=Ziyad Abdel|last7=Hakim|first7=Nagib|last8=Naeimi|first8=Helia|last9=Gardner|first9=Donald S.|last10=Mitra|first10=Subhasish|date=November 2010|title=QED: Quick Error Detection tests for effective post-silicon validation|journal=2010 IEEE International Test Conference|pages=1–10|doi=10.1109/TEST.2010.5699215|isbn=978-1-4244-7206-2|s2cid=7909084}}</ref> और [[स्वचालित प्रमेय साबित करना]]।
+फिर भी, 2007 तक, ह्यूरिस्टिक सैट-कलनविधि समस्या के उदाहरणों को हल करने में सक्षम हैं जिनमें हजारों चर सम्मलित हैं और <!---"clauses" hasn't been introduced here:--->लाखों प्रतीकों से युक्त सूत्र,<ref name="Codish.Ohrimenko.Stuckey.2007"/>जो कई व्यावहारिक सैट समस्याओं के लिए पर्याप्त है, उदाहरण के लिए, [[Index.php?title=कृत्रिम बुद्धिमता|कृत्रिम बुद्धिमता]], [[Index.php?title= विद्युत परिपथ प्रारुप|विद्युत परिपथ प्रारुप]],<ref>{{Cite journal|last1=Hong|first1=Ted|last2=Li|first2=Yanjing|last3=Park|first3=Sung-Boem|last4=Mui|first4=Diana|last5=Lin|first5=David|last6=Kaleq|first6=Ziyad Abdel|last7=Hakim|first7=Nagib|last8=Naeimi|first8=Helia|last9=Gardner|first9=Donald S.|last10=Mitra|first10=Subhasish|date=November 2010|title=QED: Quick Error Detection tests for effective post-silicon validation|journal=2010 IEEE International Test Conference|pages=1–10|doi=10.1109/TEST.2010.5699215|isbn=978-1-4244-7206-2|s2cid=7909084}}</ref> और [[स्वचालित प्रमेय साबित करना|स्वचालित प्रमेय सिद्ध करना]]।
 == परिभाषाएँ ==
@@ Line 19: / Line 19: @@
 एक खंड शाब्दिक (या एक शाब्दिक) का संयोजन है। एक उपवाक्य को हॉर्न उपवाक्य कहा जाता है यदि उसमें अधिक से अधिक एक धनात्मक अक्षर हो।
 एक सूत्र संयोजन सामान्य रूप (सीएनएफ) में है यदि यह खंड (या एक एकल खंड) का संयोजन है।
-उदाहरण के लिए, {{math|size=100%|''x''<sub>1</sub>}} एक सकारात्मक शाब्दिक है, {{math|size=100%|¬''x''<sub>2</sub>}} एक नकारात्मक शाब्दिक है, {{math|size=100%|''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub>}} एक खंड है। सूत्र {{math|size=100%|(''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub>) ∧ (¬''x''<sub>1</sub> ∨ ''x''<sub>2</sub> ∨ ''x''<sub>3</sub>) ∧ ¬''x''<sub>1</sub>}} संयोजन सामान्य रूप में है; इसका पहला और तीसरा उपवाक्य हॉर्न उपवाक्य हैं, लेकिन इसका दूसरा उपवाक्य नहीं है। सूत्र संतोषजनक है, x चुनकर<sub>1</sub>= गलत, एक्स<sub>2</sub>= फॉल्स, और x<sub>3</sub> मनमाने ढंग से, क्योंकि (फॉल्स ∨ ¬फॉल्स) ∧ (¬फॉल्स ∨ फॉल्स ∨ x<sub>3</sub>) ∧ ¬फॉल्स (फॉल्स ∨ ट्रू) ∧ (ट्रू ∨ फॉल्स ∨ x) का मूल्यांकन करता है<sub>3</sub>) ∧ ट्रू, और बदले में ट्रू ∧ ट्रू ∧ ट्रू (यानी ट्रू के लिए)। इसके विपरीत, सीएनएफ सूत्र a ∧ ¬a, जिसमें एक शाब्दिक के दो खंड शामिल हैं, असंतुष्ट है, क्योंकि a=ट्रू या a=फॉल्स के लिए यह ट्रू ∧ ¬ट्रू (अर्थात, फॉल्स) या फॉल्स ∧ ¬फॉल्स (यानी , फिर से फॉल्स), क्रमशः।
+उदाहरण के लिए, {{math|size=100%|''x''<sub>1</sub>}} एक सकारात्मक शाब्दिक है, {{math|size=100%|¬''x''<sub>2</sub>}} एक नकारात्मक शाब्दिक है, {{math|size=100%|''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub>}} एक खंड है। सूत्र {{math|size=100%|(''x''<sub>1</sub> ∨ ¬''x''<sub>2</sub>) ∧ (¬''x''<sub>1</sub> ∨ ''x''<sub>2</sub> ∨ ''x''<sub>3</sub>) ∧ ¬''x''<sub>1</sub>}} संयोजन सामान्य रूप में है; इसका पहला और तीसरा उपवाक्य हॉर्न उपवाक्य हैं, लेकिन इसका दूसरा उपवाक्य नहीं है। सूत्र संतोषजनक है, x चुनकर<sub>1</sub>= गलत, एक्स<sub>2</sub>= फॉल्स, और x<sub>3</sub> मनमाने ढंग से, क्योंकि (फॉल्स ∨ ¬फॉल्स) ∧ (¬फॉल्स ∨ फॉल्स ∨ x<sub>3</sub>) ∧ ¬फॉल्स (फॉल्स ∨ ट्रू) ∧ (ट्रू ∨ फॉल्स ∨ x) का मूल्यांकन करता है<sub>3</sub>) ∧ ट्रू, और बदले में ट्रू ∧ ट्रू ∧ ट्रू (अर्थात ट्रू के लिए)। इसके विपरीत, सीएनएफ सूत्र a ∧ ¬a, जिसमें एक शाब्दिक के दो खंड सम्मलित हैं, असंतुष्ट है, क्योंकि a=ट्रू या a=फॉल्स के लिए यह ट्रू ∧ ¬ट्रू (अर्थात, फॉल्स) या फॉल्स ∧ ¬फॉल्स (अर्थात , फिर से फॉल्स), क्रमशः।
 सैट समस्या के कुछ संस्करणों के लिए,<!---need not list them in detail here---(viz. [[#Exactly-1 3-satisfiability|Exactly-1 3-satisfiability]], [[#XOR-satisfiability|XOR-satisfiability]], and, more general, [[#Schaefer's dichotomy theorem|Schaefer's dichotomy theorem]], discussed below),---> यह एक सामान्यीकृत संयोजक सामान्य रूप सूत्र, अर्थात की धारणा को परिभाषित करने के लिए उपयोगी है। मनमाने ढंग से कई सामान्यीकृत खंडों के संयोजन के रूप में, बाद वाला फॉर्म का है {{math|''R''(''l''<sub>1</sub>,...,''l''<sub>''n''</sub>)}} कुछ [[Index.php?title=बूलियन फंगक्शन|बूलियन फंगक्शन]] R और (साधारण) शाब्दिक के लिए {{mvar|''l''<sub>''i''</sub>}}. अनुमत बूलियन कार्यों के विभिन्न सेट विभिन्न समस्या संस्करणों की ओर ले जाते हैं।<!---, see [[#Complexity and restricted versions|below]].---> एक उदाहरण के रूप में, R(¬x,a,b) एक सामान्यीकृत खंड है, और R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z) एक सामान्यीकृत खंड है संयुक्त सामान्य रूप से। इस सूत्र का उपयोग #बिल्कुल-1 3-संतोषणीयता के साथ किया जाता है, जिसमें R टर्नरी ऑपरेटर होता है जो ट्रू होता है जब इसका कोई एक तर्क होता है।
 <!---need not explain that already here---If ''R'' is the ternary operator that is TRUE just if exactly one of its arguments is, then a satisfying assignment for the latter formula can be found starting from every possible combination of truth values for ''x'', ''y'', ''z'', except ''x''&nbsp;=&nbsp;''y''&nbsp;=&nbsp;''z''&nbsp;=&nbsp;FALSE, and choosing the values of ''a'', ''b'', ''c'', ''d'' appropriately; cf. the left table under [[#Exactly-1 3-satisfiability|Exactly-1 3-satisfiability]] below.--->
-[[बूलियन बीजगणित (संरचना)]] के नियमों का उपयोग करते हुए, प्रत्येक प्रस्तावपरक तर्क सूत्र को समतुल्य संयोजन सामान्य रूप में परिवर्तित किया जा सकता है, जो कि, हालांकि, घातीय रूप से लंबा हो सकता है। उदाहरण के लिए, सूत्र को बदलना
+[[बूलियन बीजगणित (संरचना)]] के नियमों का उपयोग करते हुए, प्रत्येक प्रस्तावपरक तर्क सूत्र को समतुल्य संयोजन सामान्य रूप में परिवर्तित किया जा सकता है, जो कि, चूंकि, घातीय रूप से लंबा हो सकता है। उदाहरण के लिए, सूत्र को बदलना
 (x<sub>1</sub>∧y<sub>1</sub>) ∨ (x<sub>2</sub>∧y<sub>2</sub>) ∨ ... ∨ (x<sub>''n''</sub>∧y<sub>''n''</sub>)
 संयोजन सामान्य रूप में उत्पन्न
@@ Line 36: / Line 36: @@
 जबकि पूर्व 2 चर के n संयोजनों का संयोजन है, बाद वाले में 2<sup>n</sup> n चरों के उपवाक्य होते हैं।
-हालांकि,टेसीटिन परिवर्तन के उपयोग के साथ, हम मूल प्रस्तावपरक तर्क सूत्र के आकार में लंबाई रैखिक के साथ एक समतुल्य संयुग्मन सामान्य रूप सूत्र पा सकते हैं।
+चूंकि,टेसीटिन परिवर्तन के उपयोग के साथ, हम मूल प्रस्तावपरक तर्क सूत्र के आकार में लंबाई रैखिक के साथ एक समतुल्य संयुग्मन सामान्य रूप सूत्र पा सकते हैं।
 == जटिलता ==
 {{Main|कुक-लेविन प्रमेय}}
-सैट पहली ज्ञात एनपी-पूर्ण समस्या थी, जैसा कि 1971 में टोरंटो विश्वविद्यालय में [[स्टीफन कुक]] द्वारा सिद्ध किया गया था<ref>{{Cite journal | last1 = Cook | first1 = Stephen A. | author-link1=Stephen Cook| title = The Complexity of Theorem-Proving Procedures | pages = 151–158 | year = 1971 | url=http://www.cs.toronto.edu/~sacook/homepage/1971.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://www.cs.toronto.edu/~sacook/homepage/1971.pdf |archive-date=2022-10-09 |url-status=live| doi = 10.1145/800157.805047| citeseerx = 10.1.1.406.395 | journal = Proceedings of the 3rd Annual ACM Symposium on Theory of Computing| s2cid = 7573663 }}</ref> और स्वतंत्र रूप से 1973 में रूसी एकेडमी ऑफ साइंसेज # द एकेडमी ऑफ साइंसेज ऑफ यूएसएसआर में [[लियोनिद लेविन]] द्वारा।<ref>{{cite journal|last=Levin|first=Leonid|author-link=Leonid Levin|title = Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)|journal = Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii)|volume = 9|issue = 3|pages = 115–116|year = 1973}} [http://www.mathnet.ru/php/getFT.phtml?jrnid=ppi&paperid=914&volume=9&year=1973&issue=3&fpage=115&what=fullt&option_lang=eng (pdf)] {{in lang|ru}}, translated into English by {{cite journal|last=Trakhtenbrot|first=B. A.|title = A survey of Russian approaches to ''perebor'' (brute-force searches) algorithms|journal = Annals of the History of Computing |volume = 6|issue = 4|pages = 384–400|year = 1984|doi=10.1109/MAHC.1984.10036|s2cid=950581}}</ref> उस समय तक, एनपी-पूर्ण समस्या की अवधारणा मौजूद ही नहीं थी।
+सैट पहली ज्ञात एनपी-पूर्ण समस्या थी, जैसा कि 1971 में टोरंटो विश्वविद्यालय में [[स्टीफन कुक]] द्वारा सिद्ध किया गया था<ref>{{Cite journal | last1 = Cook | first1 = Stephen A. | author-link1=Stephen Cook| title = The Complexity of Theorem-Proving Procedures | pages = 151–158 | year = 1971 | url=http://www.cs.toronto.edu/~sacook/homepage/1971.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://www.cs.toronto.edu/~sacook/homepage/1971.pdf |archive-date=2022-10-09 |url-status=live| doi = 10.1145/800157.805047| citeseerx = 10.1.1.406.395 | journal = Proceedings of the 3rd Annual ACM Symposium on Theory of Computing| s2cid = 7573663 }}</ref> और स्वतंत्र रूप से 1973 में रूसी एकेडमी ऑफ साइंसेज # द एकेडमी ऑफ साइंसेज ऑफ यूएसएसआर में [[लियोनिद लेविन]] द्वारा।<ref>{{cite journal|last=Levin|first=Leonid|author-link=Leonid Levin|title = Universal search problems (Russian: Универсальные задачи перебора, Universal'nye perebornye zadachi)|journal = Problems of Information Transmission (Russian: Проблемы передачи информа́ции, Problemy Peredachi Informatsii)|volume = 9|issue = 3|pages = 115–116|year = 1973}} [http://www.mathnet.ru/php/getFT.phtml?jrnid=ppi&paperid=914&volume=9&year=1973&issue=3&fpage=115&what=fullt&option_lang=eng (pdf)] {{in lang|ru}}, translated into English by {{cite journal|last=Trakhtenbrot|first=B. A.|title = A survey of Russian approaches to ''perebor'' (brute-force searches) algorithms|journal = Annals of the History of Computing |volume = 6|issue = 4|pages = 384–400|year = 1984|doi=10.1109/MAHC.1984.10036|s2cid=950581}}</ref> उस समय तक, एनपी-पूर्ण समस्या की अवधारणा सम्मलित ही नहीं थी।
 उदाहरण दिखाता है कि कैसे [[जटिलता वर्ग]] एनपी (जटिलता) में हर निर्णय समस्या सीएनएफ के लिए सैट समस्या में [[कमी (जटिलता)]] हो सकती है<ref group=note>The SAT problem for ''arbitrary'' formulas is NP-complete, too, since it is easily shown to be in NP, and it cannot be easier than SAT for CNF formulas.</ref> सूत्र, जिन्हें कभी-कभी सीएनएफ सैट  कहा जाता है।
 कुक के रिडक्शन का एक उपयोगी गुण यह है कि यह स्वीकृत उत्तरों की संख्या को सुरक्षित रखता है। उदाहरण के लिए, यह तय करना कि क्या किसी दिए गए आरेख (असतत गणित) में आरेख रंग# शीर्ष् रंग 3-कलरिंग एनपी में एक और समस्या है; यदि किसी आरेख में 17 मान्य 3-रंग हैं, तो कुक-लेविन कटौती द्वारा निर्मित सैट सूत्र में 17 संतोषजनक कार्य होंगे।
@@ Line 57: / Line 57: @@
 जहाँ {{math|''x''<sub>2</sub>,&thinsp;⋯&thinsp;,&thinsp;''x''<sub>''n'' − 2</sub>}} ताजा चर हैं जो कहीं और नहीं होते हैं।
 यद्यपि दो सूत्र तार्किक रूप से समतुल्य नहीं हैं, वे समान्य: हैं। सभी खंडों को बदलने से उत्पन्न होने वाला सूत्र अपने मूल से अधिक से अधिक 3 गुना लंबा है, अर्थात लंबाई वृद्धि बहुपद है।{{sfnp|Aho|Hopcroft|Ullman|1974|loc=Theorem 10.4}}
--सैट कार्प की 21 एनपी-पूर्ण समस्याओं में से एक है, और यह साबित करने के लिए शुरुआती बिंदु के रूप में प्रयोग किया जाता है कि अन्य समस्याएं भी [[एनपी कठिन]] हैं।<ref group=note>i.e. at least as hard as every other problem in NP. A decision problem is NP-complete if and only if it is in NP and is NP-hard.</ref> यह 3-सैट से दूसरी समस्या में [[बहुपद-समय में कमी]] के द्वारा किया जाता है। एक समस्या का एक उदाहरण जहां इस पद्धति में उपयोग किया गया है, क्लिक समस्या है: एक सीएनएफ सूत्र दिया गया है जिसमें c खंड शामिल हैं, संबंधित ग्राफ (असतत गणित) में प्रत्येक शाब्दिक के लिए एक शीर्ष होता है, और प्रत्येक दो गैर-विरोधाभासी के बीच एक किनारा होता है<ref group=note>i.e. such that one literal is not the negation of the other</ref> विभिन्न खंडों से शाब्दिक, सीएफ। चित्र। आरेख में एक c-क्लिक है अगर और केवल अगर सूत्र संतोषजनक है।{{sfnp|Aho|Hopcroft|Ullman|1974|loc=Theorem 10.5}}
+-सैट कार्प की 21 एनपी-पूर्ण समस्याओं में से एक है, और यह सिद्ध करने के लिए प्रारंभिक बिंदु के रूप में प्रयोग किया जाता है कि अन्य समस्याएं भी [[एनपी कठिन]] हैं।<ref group=note>i.e. at least as hard as every other problem in NP. A decision problem is NP-complete if and only if it is in NP and is NP-hard.</ref> यह 3-सैट से दूसरी समस्या में [[बहुपद-समय में कमी]] के द्वारा किया जाता है। एक समस्या का एक उदाहरण जहां इस पद्धति में उपयोग किया गया है, क्लिक समस्या है: एक सीएनएफ सूत्र दिया गया है जिसमें c खंड सम्मलित हैं, संबंधित ग्राफ (असतत गणित) में प्रत्येक शाब्दिक के लिए एक शीर्ष होता है, और प्रत्येक दो गैर-विरोधाभासी के बीच एक किनारा होता है<ref group=note>i.e. such that one literal is not the negation of the other</ref> विभिन्न खंडों से शाब्दिक, सीएफ। चित्र। आरेख में एक c-क्लिक है यदि और केवल यदि सूत्र संतोषजनक है।{{sfnp|Aho|Hopcroft|Ullman|1974|loc=Theorem 10.5}}
 शॉनिंग (1999) के कारण एक सरल यादृच्छिक कलनविधि है जो समय में चलता है (4/3)<sup>n</sup> जहां n 3-सैट प्रस्ताव में चरों की संख्या है, और 3-सैट को सही ढंग से तय करने की उच्च संभावना के साथ सफल होता है।<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| isbn=0-7695-0409-4| chapter-url=http://homepages.cwi.nl/~rdewolf/schoning99.pdf |archive-url=https://ghostarchive.org/archive/20221009/http://homepages.cwi.nl/~rdewolf/schoning99.pdf |archive-date=2022-10-09 |url-status=live| doi=10.1109/SFFCS.1999.814612| s2cid=123177576}}</ref>
-[[घातीय समय परिकल्पना]] का दावा है कि कोई भी कलनविधि 3-सैट (या वास्तव में किसी भी के लिए के-सैट) को हल नहीं कर सकता है {{tmath|k > 2}}) में {{math|exp([[Small o notation#Little-o notation|''o'']](''n''))}} समय (यानी, n में घातीय से मौलिक रूप से तेज़)।
+[[घातीय समय परिकल्पना]] का दावा है कि कोई भी कलनविधि 3-सैट (या वास्तव में किसी भी के लिए के-सैट) को हल नहीं कर सकता है {{tmath|k > 2}}) में {{math|exp([[Small o notation#Little-o notation|''o'']](''n''))}} समय (अर्थात, n में घातीय से मौलिक रूप से तेज़)।
 सेलमैन, मिशेल, और लेवेस्क (1996) अपने आकार के मापदंडों के आधार पर बेतरतीब ढंग से उत्पन्न 3-सैट सूत्रों की कठिनाई पर अनुभवजन्य डेटा देते हैं।
 कठिनाई को [[डीपीएलएल एल्गोरिदम|डीपीएलएल कलनविधि]] द्वारा की गई संख्या पुनरावर्ती संकेत में मापा जाता है। उन्होंने एक चरण संक्रमण क्षेत्र की पहचान लगभग निश्चित रूप से संतोषजनक से लगभग निश्चित रूप से असंतोषजनक सूत्र के खंड-दर-चर अनुपात में लगभग 4.26 पर की।<ref>{{cite journal|first1=Bart |last1=Selman |first2=David |last2=Mitchell |first3=Hector |last3=Levesque | title=Generating Hard Satisfiability Problems| journal=Artificial Intelligence| year=1996| volume=81|issue=1–2 | pages=17–29| doi=10.1016/0004-3702(95)00045-3|citeseerx=10.1.1.37.7362 }}</ref>
 -संतोषजनकता को '''k'''-संतोषजनकता ('''k'''-सैट, '''k'''-सीएनएफ-सैट) के लिए सामान्यीकृत किया जा सकता है, जब सीएनएफ में सूत्रों को ''''k'''<nowiki/>' अक्षर तक के प्रत्येक खंड के साथ माना जाता है।{{citation needed|date=May 2020}}
-हालाँकि, किसी भी k ≥ 3 के लिए, यह समस्या न तो 3-सैट से आसान हो सकती है और न ही सैट से कठिन, और बाद के दो NP-पूर्ण हैं, इसलिए k-सैट होना चाहिए।
+चूंकि, किसी भी k ≥ 3 के लिए, यह समस्या न तो 3-सैट से आसान हो सकती है और न ही सैट से कठिन, और बाद के दो NP-पूर्ण हैं, इसलिए k-सैट होना चाहिए।
 कुछ लेखक k-सैट को 'बिल्कुल k शाब्दिक' के साथ सीएनएफ सूत्र तक सीमित रखते हैं।{{citation needed|date=May 2020}} यह प्रत्येक खंड के रूप में एक अलग जटिलता वर्ग की ओर नहीं ले जाता है {{math|''l''<sub>1</sub> ∨ ⋯ ∨ ''l''<sub>''j''</sub>}} with j <k लिटरल को निर्धारित डमी चर के साथ पैडेड किया जा सकता है
@@ Line 70: / Line 70: @@
 सभी खंडों को भरने के बाद, 2<sup>k</sup>-1 अतिरिक्त खंड<ref group=note>viz. all [[Canonical form (Boolean algebra)#Maxterms|maxterms]] that can be built with {{math|''d''<sub>1</sub>,⋯,''d''<sub>''k''</sub>}}, except {{math|''d''<sub>1</sub>∨⋯∨''d''<sub>''k''</sub>}}</ref> केवल यह सुनिश्चित करने के लिए संलग्न किया जाता है {{math|1=''d''<sub>1</sub> = ⋯ = ''d''<sub>''k''</sub>=FALSE}} संतोषजनक कार्य मिल सकता है। चूँकि k सूत्र की लंबाई पर निर्भर नहीं करता है, इसलिए अतिरिक्त खंड लंबाई में निरंतर वृद्धि करते हैं। उसी कारण से, इससे कोई फर्क नहीं पड़ता कि ' समरूप शाब्दिक' को खंडों में अनुमति दी जाती है, जैसा कि {{math|¬''x'' ∨ ¬''y'' ∨ ¬''y''}}.
-== सैट == के विशेष मामले में।
+== सैट == के विशेष स्थितियों में।
 === संयोजक सामान्य रूप ===
-संयोजक सामान्य रूप (विशेष रूप से 3 शाब्दिक प्रति खंड के साथ) को अक्सर सैट सूत्रों के लिए विहित प्रतिनिधित्व माना जाता है। जैसा कि ऊपर दिखाया गया है, सामान्य सैट समस्या 3-सैट तक कम हो जाती है, इस रूप में सूत्रों के लिए संतुष्टि का निर्धारण करने की समस्या।
+संयोजक सामान्य रूप (विशेष रूप से 3 शाब्दिक प्रति खंड के साथ) को अधिकांशत: सैट सूत्रों के लिए विहित प्रतिनिधित्व माना जाता है। जैसा कि ऊपर दिखाया गया है, सामान्य सैट समस्या 3-सैट तक कम हो जाती है, इस रूप में सूत्रों के लिए संतुष्टि का निर्धारण करने की समस्या।
 === वियोगात्मक सामान्य रूप ===
-सैट नगण्य है यदि सूत्र उन लोगों तक सीमित हैं जो वियोगात्मक सामान्य रूप में हैं, अर्थात, वे शाब्दिक संयोजनों के संयोजन हैं। इस तरह का एक सूत्र वास्तव में संतोषजनक है अगर और केवल अगर इसके संयोजनों में से कम से कम एक संतोषजनक है, और एक संयोजन संतोषजनक है अगर और केवल अगर इसमें कुछ चर '' के लिए '' x '' और ना ही '' x '' दोनों शामिल नहीं हैं। x'' इसे रैखिक समय में चेक किया जा सकता है। इसके अलावा, यदि वे पूर्ण वियोगात्मक सामान्य रूप में होने के लिए प्रतिबंधित हैं, जिसमें प्रत्येक चर प्रत्येक संयुग्मन में ठीक एक बार दिखाई देता है, तो उन्हें निरंतर समय में चेक किया जा सकता है (प्रत्येक संयुग्मन एक संतोषजनक समनुदेशन का प्रतिनिधित्व करता है)। लेकिन सामान्य सैट समस्या को अलग करने वाले सामान्य रूप में परिवर्तित करने में घातीय समय और स्थान लग सकता है; उदाहरण के लिए संयोजन सामान्य रूपों के लिए #परिभाषा घातीय झटका उदाहरण में ∧ और ∨ का आदान-प्रदान करें।
+सैट नगण्य है यदि सूत्र उन लोगों तक सीमित हैं जो वियोगात्मक सामान्य रूप में हैं, अर्थात, वे शाब्दिक संयोजनों के संयोजन हैं। इस तरह का एक सूत्र वास्तव में संतोषजनक है यदि और केवल यदि इसके संयोजनों में से कम से कम एक संतोषजनक है, और एक संयोजन संतोषजनक है यदि और केवल यदि इसमें कुछ चर '' के लिए '' x '' और ना ही '' x '' दोनों सम्मलित नहीं हैं। x'' इसे रैखिक समय में चेक किया जा सकता है। इसके अतिरिक्त, यदि वे पूर्ण वियोगात्मक सामान्य रूप में होने के लिए प्रतिबंधित हैं, जिसमें प्रत्येक चर प्रत्येक संयुग्मन में ठीक एक बार दिखाई देता है, तो उन्हें निरंतर समय में चेक किया जा सकता है (प्रत्येक संयुग्मन एक संतोषजनक समनुदेशन का प्रतिनिधित्व करता है)। लेकिन सामान्य सैट समस्या को अलग करने वाले सामान्य रूप में परिवर्तित करने में घातीय समय और स्थान लग सकता है; उदाहरण के लिए संयोजन सामान्य रूपों के लिए #परिभाषा घातीय झटका उदाहरण में ∧ और ∨ का आदान-प्रदान करें।
 ===बिल्कुल-1 3-संतोषजनकता===
-[[File:Schaefer's 3-SAT to 1-in-3-SAT reduction.gif|thumb|x100px|बायाँ: शेफ़र द्वारा 3-सैट खंड़ ''x'' ∨ ''y'' ∨ ''z'' की कमी। 'र' का परिणाम है {{fontcolor|#00a000|TRUE (1)}} यदि इसका एक तर्क सही है, और {{fontcolor|#a00000|FALSE (0)}} अन्यथा। x,y,z के मानों के सभी 8 संयोजनों की जांच की जाती है, प्रति पंक्ति एक। ताजा चर a,...,f सभी खंडों को संतुष्ट करने के लिए चुना जा सकता है (बिल्कुल एक {{fontcolor|#00a000|green}} प्रत्येक R के लिए तर्क) पहली पंक्ति को छोड़कर सभी पंक्तियों में, जहाँ x ∨ y ∨ z फॉल्स है। 'दाहिना:' समान गुणों वाला एक सरल अपचयन।]]3-संतोषजनक समस्या का एक प्रकार एक-इन-थ्री 3-सैट है (जिसे 1-इन-3-सैट और ठीक-ठीक 1 3-सैट के रूप में भी जाना जाता है)।
+[[File:Schaefer's 3-SAT to 1-in-3-SAT reduction.gif|thumb|x100px|बायाँ: शेफ़र द्वारा 3-सैट खंड़ ''x'' ∨ ''y'' ∨ ''z'' की कमी। 'र' का परिणाम है {{fontcolor|#00a000|ट्रू (1)}} यदि इसका एक तर्क सही है, और {{fontcolor|#a00000|फॉल्स (0)}} अन्यथा। x,y,z के मानों के सभी 8 संयोजनों की जांच की जाती है, प्रति पंक्ति एक। ताजा चर a,...,f सभी खंडों को संतुष्ट करने के लिए चुना जा सकता है (बिल्कुल एक {{fontcolor|#00a000|green}} प्रत्येक R के लिए तर्क) पहली पंक्ति को छोड़कर सभी पंक्तियों में, जहाँ x ∨ y ∨ z फॉल्स है। 'दाहिना:' समान गुणों वाला एक सरल अपचयन।]]3-संतोषजनक समस्या का एक प्रकार एक-इन-थ्री 3-सैट है (जिसे 1-इन-3-सैट और ठीक-ठीक 1 3-सैट के रूप में भी जाना जाता है)।
-तीन शाब्दिक प्रति खंड के साथ एक सामान्य रूप को देखते हुए, समस्या यह निर्धारित करने के लिए है कि क्या चर के लिए एक सत्य समनुदेशन मौजूद है, ताकि प्रत्येक खंड में ''बिल्कुल '' एक ट्रू शाब्दिक (और इस प्रकार बिल्कुल दो फॉल्स शाब्दिक) हो। इसके विपरीत, साधारण 3-सैट के लिए आवश्यक है कि प्रत्येक खंड में ''कम से कम''  एक ट्रू शाब्दिक हो।
+तीन शाब्दिक प्रति खंड के साथ एक सामान्य रूप को देखते हुए, समस्या यह निर्धारित करने के लिए है कि क्या चर के लिए एक सत्य समनुदेशन सम्मलित है, जिससे कि प्रत्येक खंड में ''बिल्कुल '' एक ट्रू शाब्दिक (और इस प्रकार बिल्कुल दो फॉल्स शाब्दिक) हो। इसके विपरीत, साधारण 3-सैट के लिए आवश्यक है कि प्रत्येक खंड में ''कम से कम''  एक ट्रू शाब्दिक हो।
-औपचारिक रूप से, एक-में-तीन 3-सैट समस्या को एक सामान्यीकृत संयोजक सामान्य रूप के रूप में दिया जाता है जिसमें सभी सामान्यीकृत खंडों के साथ एक  त्रिआधारी ऑपरेटर 'आर' का उपयोग किया जाता है जो सही है, अगर इसका कोई तर्क है। जब एक-इन-थ्री 3-सैट सूत्र के सभी शाब्दिक धनात्मक होते हैं, तो संतुष्टि समस्या को एक-इन-थ्री सकारात्मक 3-सैट कहा जाता है।
+औपचारिक रूप से, एक-में-तीन 3-सैट समस्या को एक सामान्यीकृत संयोजक सामान्य रूप के रूप में दिया जाता है जिसमें सभी सामान्यीकृत खंडों के साथ एक  त्रिआधारी ऑपरेटर 'आर' का उपयोग किया जाता है जो सही है, यदि इसका कोई तर्क है। जब एक-इन-थ्री 3-सैट सूत्र के सभी शाब्दिक धनात्मक होते हैं, तो संतुष्टि समस्या को एक-इन-थ्री सकारात्मक 3-सैट कहा जाता है।
-एक-इन-थ्री 3-सैट, इसके सकारात्मक मामले के साथ, मानक संदर्भ में एनपी-पूर्ण समस्या "LO4" के रूप में सूचीबद्ध है, ''संगणक और अव्यावहारिकता: ए गाइड टू द थ्योरी ऑफ एनपी-पूर्णता''
+एक-इन-थ्री 3-सैट, इसके सकारात्मक स्थितियों के साथ, मानक संदर्भ में एनपी-पूर्ण समस्या "LO4" के रूप में सूचीबद्ध है, ''संगणक और अव्यावहारिकता: ए गाइड टू द थ्योरी ऑफ एनपी-पूर्णता''
-माइकल आर. गैरी और डेविड एस. जॉनसन द्वारा। एक-में-तीन 3-सैट को [[थॉमस जेरोम शेफर]] द्वारा शेफर के द्विबीज प्रमेय के एक विशेष मामले के रूप में एनपी-पूर्ण साबित किया गया है, जो दावा करता है कि बूलियन संतुष्टि को एक निश्चित तरीके से सामान्यीकृत करने वाली कोई भी समस्या या तो कक्षा p में है या एनपी- है। पूरा।<ref name="schaefer">{{Cite conference | last1 = Schaefer | first1 = Thomas J. | year = 1978 | title = The complexity of satisfiability problems | book-title = Proceedings of the 10th Annual ACM Symposium on Theory of Computing | place = San Diego, California | pages = 216–226 | url = http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/materials/papers/max-sat/p216-schaefer.pdf |doi=10.1145/800133.804350 |citeseerx=10.1.1.393.8951 }}</ref>
+माइकल आर. गैरी और डेविड एस. जॉनसन द्वारा। एक-में-तीन 3-सैट को [[थॉमस जेरोम शेफर]] द्वारा शेफर के द्विबीज प्रमेय के एक विशेष स्थितियों के रूप में एनपी-पूर्ण सिद्ध किया गया है, जो दावा करता है कि बूलियन संतुष्टि को एक निश्चित तरीके से सामान्यीकृत करने वाली कोई भी समस्या या तो कक्षा p में है या एनपी- है। पूरा।<ref name="schaefer">{{Cite conference | last1 = Schaefer | first1 = Thomas J. | year = 1978 | title = The complexity of satisfiability problems | book-title = Proceedings of the 10th Annual ACM Symposium on Theory of Computing | place = San Diego, California | pages = 216–226 | url = http://www.ccs.neu.edu/home/lieber/courses/csg260/f06/materials/papers/max-sat/p216-schaefer.pdf |doi=10.1145/800133.804350 |citeseerx=10.1.1.393.8951 }}</ref>
 शेफ़र 3-सैट से एक-इन-थ्री 3-सैट तक एक आसान बहुपद-समय की कमी की अनुमति देते हुए एक निर्माण देता है। मान लीजिए (x या y या z) 3सीएनएफ सूत्र में एक खंड है। इस खंड का अनुकरण करने के लिए उपयोग किए जाने वाले छह नए बूलियन चर a, b, c, d, e, और f जोड़ें और कोई अन्य नहीं।
 <!---now introduced already above---Let ''R''(''u'',''v'',''w'') be a predicate that is TRUE if and only if exactly one of the booleans ''u'', ''v'', and ''w''
 is TRUE.--->
 तब सूत्र R(x,a,d) ∧ R(y,b,d) ∧ R(a,b,e) ∧ R(c,d,f) ∧ R(z,c,फॉल्स) द्वारा संतोषजनक है ताज़ा चरों की कुछ विन्यास यदि और केवल यदि x, y, या z में से कम से कम एक सत्य है, चित्र देखें (बाएं)। इस प्रकार एम खंड और एन चर के साथ किसी भी 3-सैट उदाहरण को 5 एम खंड और एन + 6 एम चर के साथ तीन 3-सैट उदाहरण में एक समतुल्य में परिवर्तित किया जा सकता है।{{sfnp|Schaefer|1978|p=222, Lemma 3.5}}
-एक और कटौती में केवल चार नए चर और तीन खंड शामिल हैं: R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z), चित्र देखें (दाएं)।
+एक और कटौती में केवल चार नए चर और तीन खंड सम्मलित हैं: R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z), चित्र देखें (दाएं)।
 ===नहीं-सब-बराबर 3-संतोषजनक===
@@ Line 95: / Line 95: @@
 एक अन्य संस्करण नहीं-सब-बराबर 3-संतोषजनक समस्या है (जिसे एनएई 3सैट भी कहा जाता है)।
-तीन शाब्दिक प्रति खंड के साथ एक संयोजन सामान्य रूप दिया गया है, समस्या यह निर्धारित करने के लिए है कि क्या चर के लिए एक समनुदेशन मौजूद है जैसे कि किसी भी खंड में सभी तीन शाब्दिक समान सत्य मूल्य नहीं हैं। यह समस्या एनपी-पूर्ण है, भले ही शेफर के द्विबीजपत्री प्रमेय द्वारा कोई निषेध प्रतीक स्वीकार न किया गया हो।<ref name="schaefer"/>
+तीन शाब्दिक प्रति खंड के साथ एक संयोजन सामान्य रूप दिया गया है, समस्या यह निर्धारित करने के लिए है कि क्या चर के लिए एक समनुदेशन सम्मलित है जैसे कि किसी भी खंड में सभी तीन शाब्दिक समान सत्य मूल्य नहीं हैं। यह समस्या एनपी-पूर्ण है, भले ही शेफर के द्विबीजपत्री प्रमेय द्वारा कोई निषेध प्रतीक स्वीकार न किया गया हो।<ref name="schaefer"/>
 === रैखिक सैट ===
-एक 3-सैट सूत्र रैखिक सैट (एलसैट) है यदि प्रत्येक खंड (शाब्दिक के एक सेट के रूप में देखा जाता है) एक दूसरे खंड पर प्रतिच्छेद करता है, और, इसके अलावा, यदि दो खंड प्रतिच्छेद करते हैं, तो उनके पास वास्तव में एक शाब्दिक समान है। एक एलसैट सूत्र को एक रेखा पर असंयुक्त अर्ध-बंद अंतराल के सेट के रूप में चित्रित किया जा सकता है। यह तय करना कि एलसैट सूत्र संतोषजनक है या नहीं, एनपी-पूर्ण है।<ref>{{Cite journal|last1=Arkin|first1=Esther M.|last2=Banik|first2=Aritra|last3=Carmi|first3=Paz|last4=Citovsky|first4=Gui|last5=Katz|first5=Matthew J.|last6=Mitchell|first6=Joseph S. B.|last7=Simakov|first7=Marina|date=2018-12-11|title=Selecting and covering colored points|journal=Discrete Applied Mathematics|language=en|volume=250|pages=75–86|doi=10.1016/j.dam.2018.05.011|issn=0166-218X|doi-access=free}}</ref>
+एक 3-सैट सूत्र रैखिक सैट (एलसैट) है यदि प्रत्येक खंड (शाब्दिक के एक सेट के रूप में देखा जाता है) एक दूसरे खंड पर प्रतिच्छेद करता है, और, इसके अतिरिक्त, यदि दो खंड प्रतिच्छेद करते हैं, तो उनके पास वास्तव में एक शाब्दिक समान है। एक एलसैट सूत्र को एक रेखा पर असंयुक्त अर्ध-बंद अंतराल के सेट के रूप में चित्रित किया जा सकता है। यह तय करना कि एलसैट सूत्र संतोषजनक है या नहीं, एनपी-पूर्ण है।<ref>{{Cite journal|last1=Arkin|first1=Esther M.|last2=Banik|first2=Aritra|last3=Carmi|first3=Paz|last4=Citovsky|first4=Gui|last5=Katz|first5=Matthew J.|last6=Mitchell|first6=Joseph S. B.|last7=Simakov|first7=Marina|date=2018-12-11|title=Selecting and covering colored points|journal=Discrete Applied Mathematics|language=en|volume=250|pages=75–86|doi=10.1016/j.dam.2018.05.011|issn=0166-218X|doi-access=free}}</ref>
@@ Line 105: / Line 105: @@
 {{Main|2-संतुष्टि}}
-सैट आसान है अगर एक खंड में अक्षर की संख्या अधिकतम 2 तक सीमित है, इस मामले में समस्या को 2-सैट कहा जाता है। इस समस्या को बहुपद समय में हल किया जा सकता है, और वास्तव में जटिलता वर्ग एन[[एल (जटिलता)]] के लिए [[एनएल-पूर्ण]] है। यदि अतिरिक्त रूप से शाब्दिक रूप से सभी या संचालन को अनन्य या संचालन में बदल दिया जाता है, तो परिणाम को अनन्य-या 2-संतोषजनकता कहा जाता है, जो कि जटिलता वर्ग एसएल (जटिलता) = एल (जटिलता) के लिए पूर्ण समस्या है।
+सैट आसान है यदि एक खंड में अक्षर की संख्या अधिकतम 2 तक सीमित है, इस स्थितियों में समस्या को 2-सैट कहा जाता है। इस समस्या को बहुपद समय में हल किया जा सकता है, और वास्तव में जटिलता वर्ग एन[[एल (जटिलता)]] के लिए [[एनएल-पूर्ण]] है। यदि अतिरिक्त रूप से शाब्दिक रूप से सभी या संचालन को अनन्य या संचालन में बदल दिया जाता है, तो परिणाम को अनन्य-या 2-संतोषजनकता कहा जाता है, जो कि जटिलता वर्ग एसएल (जटिलता) = एल (जटिलता) के लिए पूर्ण समस्या है।
 === हॉर्न-संतुष्टि ===
@@ Line 113: / Line 113: @@
 इसे बहुपद समय में यूनिट प्रसार कलनविधि के एक चरण द्वारा हल किया जा सकता है, जो हॉर्न खंड के सेट के एकल न्यूनतम मॉडल का उत्पादन करता है डब्ल्यू.आर.टी. ट्रू को निर्दिष्ट शाब्दिक सेट)।
 हॉर्न-संतोषजनकता [[Index.php?title=P पूर्ण|P पूर्ण]] है। इसे P (जटिलता) के रूप में देखा जा सकता है। बूलियन संतुष्टि समस्या के P संस्करण।
-इसके अलावा, बहुपद समय में परिमाणित हॉर्न सूत्र की सच्चाई का निर्धारण किया जा सकता है।
+इसके अतिरिक्त, बहुपद समय में परिमाणित हॉर्न सूत्र की सच्चाई का निर्धारण किया जा सकता है।
 <ref name="buningkarpinski">{{Cite journal | last1 = Buning | first1 = H.K. | last2 = Karpinski| first2 =  Marek| last3=Flogel|first3=A.|year = 1995 | title = Resolution for Quantified Boolean Formulas | journal = Information and Computation | volume = 117 | issue = 1 | pages = 12–18 | publisher = Elsevier | doi= 10.1006/inco.1995.1025| doi-access = free }}</ref>
-हॉर्न खण्ड़ दिलचस्प हैं क्योंकि वे अन्य चरों के एक सेट से एक चर की प्रविष्टि को व्यक्त करने में सक्षम हैं। दरअसल, ऐसा ही एक खंड ¬x<sub>1</sub> ∨ ... ∨ ¬x<sub>''n''</sub> ∨ y को x के रूप में फिर से लिखा जा सकता है<sub>1</sub> ∧ ... ∧ x<sub>''n''</sub> → y, यानी, अगर x<sub>1</sub>,...,x<sub>''n''</sub> सभी ट्रू हैं, तो y को भी ट्रू होना चाहिए।
+हॉर्न खण्ड़ दिलचस्प हैं क्योंकि वे अन्य चरों के एक सेट से एक चर की प्रविष्टि को व्यक्त करने में सक्षम हैं। दरअसल, ऐसा ही एक खंड ¬x<sub>1</sub> ∨ ... ∨ ¬x<sub>''n''</sub> ∨ y को x के रूप में फिर से लिखा जा सकता है<sub>1</sub> ∧ ... ∧ x<sub>''n''</sub> → y, अर्थात, यदि x<sub>1</sub>,...,x<sub>''n''</sub> सभी ट्रू हैं, तो y को भी ट्रू होना चाहिए।
 हॉर्न सूत्र की श्रेणी का एक सामान्यीकरण नाम बदलने योग्य-हॉर्न सूत्र का है, जो कि उन सूत्र का सेट है जिन्हें कुछ चरों को उनके संबंधित नकार के साथ बदलकर हॉर्न रूप में रखा जा सकता है।
@@ Line 355: / Line 355: @@
 |}
-एक और विशेष मामला समस्याओं का वर्ग है जहां प्रत्येक खंड में (स्पष्ट) या ऑपरेटरों के बजाय एक्सओआर (यानी अपवर्जित ) होता है।<ref group=note>Formally, generalized conjunctive normal forms with a ternary boolean function ''R'' are employed, which is TRUE just if 1 or 3 of its arguments is. An input clause with more than 3 literals can be transformed into an equisatisfiable conjunction of clauses á 3 literals similar to [[#3-satisfiability|above]]; i.e. XOR-SAT can be reduced to XOR-3-SAT.</ref>
+एक और विशेष मामला समस्याओं का वर्ग है जहां प्रत्येक खंड में (स्पष्ट) या ऑपरेटरों के अतिरिक्त एक्सओआर (अर्थात अपवर्जित ) होता है।<ref group=note>Formally, generalized conjunctive normal forms with a ternary boolean function ''R'' are employed, which is TRUE just if 1 or 3 of its arguments is. An input clause with more than 3 literals can be transformed into an equisatisfiable conjunction of clauses á 3 literals similar to [[#3-satisfiability|above]]; i.e. XOR-SAT can be reduced to XOR-3-SAT.</ref>
 यह [[Index.php?title=p (जटिलता वर्ग)|p (जटिलता वर्ग)]] में है, चूंकि एक्सओआर-सैट सूत्र को रैखिक समीकरण मॉड 2 की प्रणाली के रूप में भी देखा जा सकता है, और गॉसियन उन्मूलन द्वारा घन काल में हल किया जा सकता है;<ref>{{citation|title=The Nature of Computation|first1=Cristopher|last1=Moore|author1-link=Cristopher Moore|first2=Stephan|last2=Mertens|publisher=Oxford University Press|year=2011|isbn=9780199233212|page=366|url=https://books.google.com/books?id=z4zMiZyAE1kC&pg=PA366}}.</ref> उदाहरण के लिए डिब्बे में देखें। यह पुनर्रचना बूलियन बीजगणित (संरचना)#बूलियन वल्य पर आधारित है, और यह तथ्य कि अंकगणितीय सापेक्ष दो एक [[परिमित क्षेत्र]] बनाते हैं। चूँकि एक एक्सओआर ''b'' एक्सओआर ''c'' ट्रू का मूल्यांकन करता है यदि और केवल यदि {a,b,c} के ठीक 1 या 3 सदस्य ट्रू हैं, तो किसी दिए गए सीएनएफ सूत्र के लिए 1-इन-3-सैट समस्या का प्रत्येक समाधान भी एक समाधान है एक्सओआर-3-सैट समस्या का, और बदले में एक्सओआर-3-सैट का प्रत्येक समाधान 3-सैट, ''cf'' का समाधान है। चित्र परिणामस्वरूप, प्रत्येक सीएनएफ सूत्र के लिए, सूत्र द्वारा परिभाषित एक्सओआर-3-सैट समस्या को हल करना संभव है, और परिणाम के आधार पर अनुमान लगाया जाता है कि 3-सैट समस्या हल करने योग्य है, या 1-में-3- सैट समस्या हल करने योग्य नहीं है।
@@ Line 365: / Line 365: @@
 उपरोक्त प्रतिबंध (सीएनएफ, 2सीएनएफ, 3सीएनएफ, हॉर्न, एक्सओआर-सैट) विचार किए गए सूत्रों को उपसूत्र के संयोजन के रूप में बाध्य करते हैं; प्रत्येक प्रतिबंध सभी उपसूत्रों के लिए एक विशिष्ट रूप बताता है: उदाहरण के लिए, केवल द्विआधारी खंड 2सीएनएफ में उपसूत्र हो सकते हैं।
-शेफर के द्विभाजन प्रमेय में कहा गया है कि, बूलियन कार्यों के लिए किसी भी प्रतिबंध के लिए जिसका उपयोग इन उपसूत्रों को बनाने के लिए किया जा सकता है, संबंधित संतुष्टि समस्या ''p'' या एनपी-पूर्ण में है। 2सीएनएफ, हॉर्न, और एक्सओआर-सैट सूत्रों की संतुष्टि की P में सदस्यता इस प्रमेय के विशेष मामले हैं।<ref name="schaefer"/>
+शेफर के द्विभाजन प्रमेय में कहा गया है कि, बूलियन कार्यों के लिए किसी भी प्रतिबंध के लिए जिसका उपयोग इन उपसूत्रों को बनाने के लिए किया जा सकता है, संबंधित संतुष्टि समस्या ''p'' या एनपी-पूर्ण में है। 2सीएनएफ, हॉर्न, और एक्सओआर-सैट सूत्रों की संतुष्टि की P में सदस्यता इस प्रमेय के विशेष स्थितियों हैं।<ref name="schaefer"/>
 निम्न तालिका सैट के कुछ सामान्य रूपों का सारांश देती है।
@@ Line 432: / Line 432: @@
 |एक्सओआर-सैट
 |एक्सओआर संतोषणीयता
-|प्रत्येक क्लॉज में OR के बजाय एक्सओआर ऑपरेशन होते हैं।
+|प्रत्येक क्लॉज में OR के अतिरिक्त एक्सओआर ऑपरेशन होते हैं।
 |सभी शाब्दिकों का एक्सओआर ट्रू होना चाहिए।
 |P
@@ Line 438: / Line 438: @@
 == सैट का विस्तार ==
-एक्सटेंशन जिसने 2003 के बाद से महत्वपूर्ण लोकप्रियता हासिल की है, वह है संतुष्टि मोडुलो सिद्धांत (एसएमटी) जो सीएनएफ सूत्रों को रैखिक बाधाओं, सरणियों, सभी अलग-अलग बाधाओं, अबाधित कार्यों के साथ समृद्ध कर सकता है।<ref name="Bryant.German.Velev.1999">R. E. Bryant, S. M. German, and M. N. Velev, [http://portal.acm.org/citation.cfm?id=709275 Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions], in Analytic Tableaux and Related Methods, pp.&nbsp;1–13, 1999.</ref> आदि। इस तरह के विस्तार आम तौर पर एनपी-पूर्ण रहते हैं, लेकिन अब बहुत कुशल समाधानकर्ता उपलब्ध हैं जो इस तरह की कई बाधाओं को संभाल सकते हैं।
+एक्सटेंशन जिसने 2003 के बाद से महत्वपूर्ण लोकप्रियता हासिल की है, वह है संतुष्टि मोडुलो सिद्धांत (एसएमटी) जो सीएनएफ सूत्रों को रैखिक बाधाओं, सरणियों, सभी अलग-अलग बाधाओं, अबाधित कार्यों के साथ समृद्ध कर सकता है।<ref name="Bryant.German.Velev.1999">R. E. Bryant, S. M. German, and M. N. Velev, [http://portal.acm.org/citation.cfm?id=709275 Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions], in Analytic Tableaux and Related Methods, pp.&nbsp;1–13, 1999.</ref> आदि। इस तरह के विस्तार सामान्यत: पर एनपी-पूर्ण रहते हैं, लेकिन अब बहुत कुशल समाधानकर्ता उपलब्ध हैं जो इस तरह की कई बाधाओं को संभाल सकते हैं।
 संतुष्टि की समस्या और अधिक कठिन हो जाती है यदि सभी के लिए (∀) और वहाँ (∃) [[परिमाणक (तर्क)]] दोनों के लिए बूलियन चर को बाँधने की अनुमति हो।
 ऐसी अभिव्यक्ति का एक उदाहरण होगा {{math|size=100%|∀''x'' ∀''y'' ∃''z'' (''x'' ∨ ''y'' ∨ ''z'') ∧ (¬''x'' ∨ ¬''y'' ∨ ¬''z'')}}; यह मान्य है, क्योंकि x और y के सभी मानों के लिए, z का एक उपयुक्त मान पाया जा सकता है, अर्थात। z=ट्रू यदि x और y दोनों फॉल्स हैं, और z=फॉल्स अन्य।
 सैट स्वयं (मौन रूप से) केवल ∃ क्वांटिफायर का उपयोग करता है।
-यदि इसके बजाय केवल ∀ परिमाणकों की अनुमति है, तथाकथित '[[Index.php?title= पुनरुक्ति (तर्क)|पुनरुक्ति (तर्क)]] समस्या' प्राप्त की जाती है, जो [[सह-एनपी-पूर्ण]] है।
+यदि इसके अतिरिक्त केवल ∀ परिमाणकों की अनुमति है, तथाकथित '[[Index.php?title= पुनरुक्ति (तर्क)|पुनरुक्ति (तर्क)]] समस्या' प्राप्त की जाती है, जो [[सह-एनपी-पूर्ण]] है।
-यदि दोनों परिमाणकों की अनुमति है, तो समस्या को 'मात्राबद्ध बूलियन सूत्र समस्या' ('क्यूबीएफ') कहा जाता है, जिसे पीएसपीएसीई-पूर्ण दिखाया जा सकता है। यह व्यापक रूप से माना जाता है कि एनपी में किसी भी समस्या की तुलना में पीएसपीएसीई-पूर्ण समस्याएं सख्ती से कठिन हैं, हालांकि यह अभी तक सिद्ध नहीं हुआ है। अत्यधिक समानांतर [[Index.php?title=p प्रणाली|p प्रणाली]] का उपयोग करके, एयुबीएफ-सैट समस्याओं को रैखिक समय में हल किया जा सकता है।<ref>{{Cite journal | last1 = Alhazov | first1 = Artiom | last2 = Martín-Vide | first2 = Carlos | last3 = Pan | first3 = Linqiang | title = Solving a PSPACE-Complete Problem by Recognizing P Systems with Restricted Active Membranes |  url=https://www.researchgate.net/publication/220444503 | journal = Fundamenta Informaticae | volume = 58 | pages = 67–77 | year = 2003 }} Here: Sect.3, Thm.3.1</ref>
+यदि दोनों परिमाणकों की अनुमति है, तो समस्या को 'मात्राबद्ध बूलियन सूत्र समस्या' ('क्यूबीएफ') कहा जाता है, जिसे पीएसपीएसीई-पूर्ण दिखाया जा सकता है। यह व्यापक रूप से माना जाता है कि एनपी में किसी भी समस्या की तुलना में पीएसपीएसीई-पूर्ण समस्याएं सख्ती से कठिन हैं, चूंकि यह अभी तक सिद्ध नहीं हुआ है। अत्यधिक समानांतर [[Index.php?title=p प्रणाली|p प्रणाली]] का उपयोग करके, एयुबीएफ-सैट समस्याओं को रैखिक समय में हल किया जा सकता है।<ref>{{Cite journal | last1 = Alhazov | first1 = Artiom | last2 = Martín-Vide | first2 = Carlos | last3 = Pan | first3 = Linqiang | title = Solving a PSPACE-Complete Problem by Recognizing P Systems with Restricted Active Membranes |  url=https://www.researchgate.net/publication/220444503 | journal = Fundamenta Informaticae | volume = 58 | pages = 67–77 | year = 2003 }} Here: Sect.3, Thm.3.1</ref>
 सामान्य सैट पूछता है कि क्या कम से कम एक परिवर्तनीय समनुदेशन है जो सूत्र को सत्य बनाता है। विभिन्न प्रकार के प्रकारांतर ऐसे समनुदेशन की संख्या से निपटते हैं:
 * एमएजी-सैट पूछता है कि क्या सभी समनुदेशन्स में से अधिकांश सूत्र को ट्रू बनाते हैं। यह [[Index.php?title=pp (जटिलता)|pp (जटिलता)]] के लिए पूर्ण माना जाता है, एक संभाव्य वर्ग।
 * स्पष्ट-सैट|#सैट, गिनती की समस्या कि कितने चर समनुदेशन एक सूत्र को संतुष्ट करते हैं, एक गिनती की समस्या है, निर्णय की समस्या नहीं है, और  स्पष्ट-P-पूर्ण।
 * अद्वितीय सैट<ref>{{Cite journal|last1=Blass|first1=Andreas|last2=Gurevich|first2=Yuri|date=1982-10-01|title=On the unique satisfiability problem|journal=Information and Control|volume=55|issue=1|pages=80–88|doi=10.1016/S0019-9958(82)90439-9|issn=0019-9958|doi-access=free}}</ref> यह निर्धारित करने की समस्या है कि क्या किसी सूत्र में ठीक एक नियत कार्य है। यह [[यूएस (जटिलता)]] के लिए पूर्ण है,<ref>{{Cite web|url=https://complexityzoo.uwaterloo.ca/Complexity_Zoo:U#US|title=Complexity Zoo:U - Complexity Zoo|website=complexityzoo.uwaterloo.ca|access-date=2019-12-05|archive-date=2019-07-09|archive-url=https://web.archive.org/web/20190709142353/https://complexityzoo.uwaterloo.ca/Complexity_Zoo:U#US|url-status=dead}}</ref> एक गैर-नियतात्मक बहुपद समय [[ट्यूरिंग मशीन]] द्वारा हल की जा सकने वाली समस्याओं का वर्णन करने वाली जटिलता वर्ग, जो तब स्वीकार करती है जब वास्तव में एक गैर-नियतात्मक स्वीकार्य पथ होता है और अन्यथा अस्वीकार करता है।
-*स्पष्ट-सैट वह नाम है जो संतुष्टि समस्या को दिया जाता है जब निविष्ट अधिकतम एक संतोषजनक समनुदेशन वाले सूत्र के लिए संतोषजनक कार्य होता है। समस्या को यूसैट भी कहा जाता है।<ref>{{Cite book |chapter-url=https://www.springer.com/gp/book/9781846282973 |chapter=Supplementary Lecture F: Unique Satisfiability |title=Theory of Computation |last=Kozen |first=Dexter C. |date=2006 |publisher=Springer  |isbn=9781846282973 |series=Texts in Computer Science |page=180 |language=en}}</ref>  स्पष्ट-सैट के लिए एक सुलझाने वाली कलनविधि को कई संतोषजनक समनुदेशन वाले सूत्र पर अंतहीन पाशन सहित किसी भी व्यवहार को प्रदर्शित करने की अनुमति है। हालाँकि यह समस्या आसान लगती है, वैलेंट और वज़ीरानी के पास वैलेंट-वज़ीरानी प्रमेय है<ref>{{Cite journal | last1 = Valiant | first1 = L. | last2 = Vazirani | first2 = V.| doi = 10.1016/0304-3975(86)90135-0 | title = NP is as easy as detecting unique solutions | url = http://www.cs.princeton.edu/courses/archive/fall05/cos528/handouts/NP_is_as.pdf| journal = Theoretical Computer Science | volume = 47 | pages = 85–93 | year = 1986 | doi-access = free }}</ref> कि अगर इसे हल करने के लिए एक व्यावहारिक (यानी [[परिबद्ध-त्रुटि संभाव्य बहुपद]]। यादृच्छिक बहुपद-समय) कलनविधि है, तो [[एनपी (जटिलता वर्ग)]] में सभी समस्याओं को आसानी से हल किया जा सकता है।
+*स्पष्ट-सैट वह नाम है जो संतुष्टि समस्या को दिया जाता है जब निविष्ट अधिकतम एक संतोषजनक समनुदेशन वाले सूत्र के लिए संतोषजनक कार्य होता है। समस्या को यूसैट भी कहा जाता है।<ref>{{Cite book |chapter-url=https://www.springer.com/gp/book/9781846282973 |chapter=Supplementary Lecture F: Unique Satisfiability |title=Theory of Computation |last=Kozen |first=Dexter C. |date=2006 |publisher=Springer  |isbn=9781846282973 |series=Texts in Computer Science |page=180 |language=en}}</ref>  स्पष्ट-सैट के लिए एक सुलझाने वाली कलनविधि को कई संतोषजनक समनुदेशन वाले सूत्र पर अंतहीन पाशन सहित किसी भी व्यवहार को प्रदर्शित करने की अनुमति है। चूंकि यह समस्या आसान लगती है, वैलेंट और वज़ीरानी के पास वैलेंट-वज़ीरानी प्रमेय है<ref>{{Cite journal | last1 = Valiant | first1 = L. | last2 = Vazirani | first2 = V.| doi = 10.1016/0304-3975(86)90135-0 | title = NP is as easy as detecting unique solutions | url = http://www.cs.princeton.edu/courses/archive/fall05/cos528/handouts/NP_is_as.pdf| journal = Theoretical Computer Science | volume = 47 | pages = 85–93 | year = 1986 | doi-access = free }}</ref> कि यदि इसे हल करने के लिए एक व्यावहारिक (अर्थात [[परिबद्ध-त्रुटि संभाव्य बहुपद]]। यादृच्छिक बहुपद-समय) कलनविधि है, तो [[एनपी (जटिलता वर्ग)]] में सभी समस्याओं को आसानी से हल किया जा सकता है।
 * मैक्स-सैट, [[अधिकतम संतुष्टि की समस्या]], सैट का एपएनपी (जटिलता) सामान्यीकरण है। यह अधिकतम संख्या में खंडों के लिए पूछता है जो किसी भी समनुदेशन से संतुष्ट हो सकते हैं। इसमें कुशल सन्निकटन कलनविधि हैं, लेकिन एनपी-कठिन को ठीक से हल करना है। इससे भी बदतर, यह [[एपीएक्स]]-पूर्ण है, जिसका अर्थ है कि इस समस्या के लिए कोई [[बहुपद-समय सन्निकटन योजना]] (पीटीएएस) नहीं है जब तक कि p = एनपी न हो।
-*डब्ल्यूएम-सैट न्यूनतम वजन का एक समनुदेशन खोजने की समस्या है जो एक एकदिष्ट बूलियन सूत्र (यानी बिना किसी निषेध के एक सूत्र) को संतुष्ट करता है। समस्या के निविष्ट में प्रस्तावात्मक चर के भार दिए गए हैं। समनुदेशन का वजन सही चर के वजन का योग है। वह समस्या एनपी-पूर्ण है (थ देखें। 1 का <ref>{{Cite journal|last1=Buldas|first1=Ahto|last2=Lenin|first2=Aleksandr|last3=Willemson|first3=Jan|last4=Charnamord|first4=Anton|date=2017|editor-last=Obana|editor-first=Satoshi|editor2-last=Chida|editor2-first=Koji|title=Simple Infeasibility Certificates for Attack Trees|journal=Advances in Information and Computer Security|volume=10418|series=Lecture Notes in Computer Science|language=en|publisher=Springer International Publishing|pages=39–55|doi=10.1007/978-3-319-64200-0_3|isbn=9783319642000}}</ref>).
+*डब्ल्यूएम-सैट न्यूनतम वजन का एक समनुदेशन खोजने की समस्या है जो एक एकदिष्ट बूलियन सूत्र (अर्थात बिना किसी निषेध के एक सूत्र) को संतुष्ट करता है। समस्या के निविष्ट में प्रस्तावात्मक चर के भार दिए गए हैं। समनुदेशन का वजन सही चर के वजन का योग है। वह समस्या एनपी-पूर्ण है (थ देखें। 1 का <ref>{{Cite journal|last1=Buldas|first1=Ahto|last2=Lenin|first2=Aleksandr|last3=Willemson|first3=Jan|last4=Charnamord|first4=Anton|date=2017|editor-last=Obana|editor-first=Satoshi|editor2-last=Chida|editor2-first=Koji|title=Simple Infeasibility Certificates for Attack Trees|journal=Advances in Information and Computer Security|volume=10418|series=Lecture Notes in Computer Science|language=en|publisher=Springer International Publishing|pages=39–55|doi=10.1007/978-3-319-64200-0_3|isbn=9783319642000}}</ref>).
-अन्य सामान्यीकरणों में प्रथम-क्रम विधेय- और द्वितीय-क्रम तर्क, [[बाधा संतुष्टि समस्या]]ओं, [[0-1 पूर्णांक प्रोग्रामिंग]] के लिए संतुष्टि शामिल है।
+अन्य सामान्यीकरणों में प्रथम-क्रम विधेय- और द्वितीय-क्रम तर्क, [[बाधा संतुष्टि समस्या]]ओं, [[0-1 पूर्णांक प्रोग्रामिंग]] के लिए संतुष्टि सम्मलित है।
 == एक संतोषजनक समनुदेशन ढूँढना ==
-जबकि सैट एक निर्णय समस्या है, संतोषजनक समनुदेशन खोजने की [[खोज समस्या]] सैट तक कम हो जाती है। अर्थात्, प्रत्येक कलनविधि जो सही ढंग से उत्तर देता है कि क्या सैट का एक उदाहरण हल करने योग्य है, एक संतोषजनक समनुदेशन खोजने के लिए इस्तेमाल किया जा सकता है। सबसे पहले दिए गए सूत्र Φ पर प्रश्न पूछा जाता है। यदि उत्तर नहीं है, तो सूत्र संतोषजनक नहीं है। अन्यथा, प्रश्न आंशिक रूप से तत्काल सूत्र Φप्रतिस्थापन (तर्क) पर पूछा जाता है|{x<sub>1</sub>=ट्रू}, यानी Φ पहले चर x के साथ<sub>1</sub> ट्रू द्वारा प्रतिस्थापित किया गया, और तदनुसार सरलीकृत किया गया। यदि उत्तर हाँ है, तो x<sub>1</sub>= ट्रू, अन्यथा x<sub>1</sub>= फॉल्स है। अन्य चरों के मान बाद में उसी तरह पाए जा सकते हैं। कुल मिलाकर, कलनविधि के n+1 रन आवश्यक हैं, जहां n Φ में अलग-अलग चर की संख्या है।
+जबकि सैट एक निर्णय समस्या है, संतोषजनक समनुदेशन खोजने की [[खोज समस्या]] सैट तक कम हो जाती है। अर्थात्, प्रत्येक कलनविधि जो सही ढंग से उत्तर देता है कि क्या सैट का एक उदाहरण हल करने योग्य है, एक संतोषजनक समनुदेशन खोजने के लिए उपयोग किया जा सकता है। सबसे पहले दिए गए सूत्र Φ पर प्रश्न पूछा जाता है। यदि उत्तर नहीं है, तो सूत्र संतोषजनक नहीं है। अन्यथा, प्रश्न आंशिक रूप से तत्काल सूत्र Φप्रतिस्थापन (तर्क) पर पूछा जाता है|{x<sub>1</sub>=ट्रू}, अर्थात Φ पहले चर x के साथ<sub>1</sub> ट्रू द्वारा प्रतिस्थापित किया गया, और तदनुसार सरलीकृत किया गया। यदि उत्तर हाँ है, तो x<sub>1</sub>= ट्रू, अन्यथा x<sub>1</sub>= फॉल्स है। अन्य चरों के मान बाद में उसी तरह पाए जा सकते हैं। कुल मिलाकर, कलनविधि के n+1 रन आवश्यक हैं, जहां n Φ में अलग-अलग चर की संख्या है।
 इस संपत्ति का उपयोग जटिलता सिद्धांत में कई प्रमेयों में किया जाता है:
@@ Line 466: / Line 466: @@
 == सैट को हल करने के लिए कलनविधि ==
 {{main| सैट समाधानकर्ता}}
-चूंकि सैट समस्या एनपी-पूर्ण है, केवल घातीय सबसे खराब स्थिति वाले कलनविधि इसके लिए जाने जाते हैं। इसके बावजूद, सैट के लिए कुशल और मापनीय कलनविधि 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> [[Index.php?title=इलेक्ट्रॉनिक अभिकल्पन स्वचालन|इलेक्ट्रॉनिक अभिकल्पन स्वचालन]] (ईडीए) में ऐसी समस्याओं के उदाहरणों में [[औपचारिक तुल्यता जाँच]], मॉडल जाँच, [[Index.php?title= सूक्ष्मप्रक्रमक|सूक्ष्मप्रक्रमक]] का [[औपचारिक सत्यापन]],<ref name="Bryant.German.Velev.1999" />स्वत: परीक्षण प्रारूप पीढ़ी, [[एफपीजीए]] की [[Index.php?title= क्रम (इलेक्ट्रॉनिक अभिकल्पन स्वचालन)|क्रम (इलेक्ट्रॉनिक अभिकल्पन स्वचालन)]],<ref>{{Cite journal |last1=Gi-Joon Nam |last2=Sakallah |first2=K. A. |last3=Rutenbar |first3=R. A. |title=A new FPGA detailed routing approach via search-based Boolean satisfiability |journal=IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |volume=21 |issue=6 |pages=674 |year=2002 |url=http://cs-rutenbar.web.engr.illinois.edu/wp-content/uploads/2012/10/rutenbar-sattranscad02.pdf| doi=10.1109/TCAD.2002.1004311}}</ref> [[Index.php?title=स्वचालित योजना और अनुसूचन|स्वचालित योजना और अनुसूचन]], और [[Index.php?title=अनुसूचन कलनविधि|अनुसूचन कलनविधि]], और इसी तरह। इलेक्ट्रॉनिक अभिकल्पन स्वचालन उपकरण पेटी में एक सैट-सॉल्विंग इंजन को भी एक आवश्यक घटक माना जाता है।
+चूंकि सैट समस्या एनपी-पूर्ण है, केवल घातीय सबसे खराब स्थिति वाले कलनविधि इसके लिए जाने जाते हैं। इसके बावजूद, सैट के लिए कुशल और मापनीय कलनविधि 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> [[Index.php?title=इलेक्ट्रॉनिक अभिकल्पन स्वचालन|इलेक्ट्रॉनिक अभिकल्पन स्वचालन]] (ईडीए) में ऐसी समस्याओं के उदाहरणों में [[औपचारिक तुल्यता जाँच]], मॉडल जाँच, [[Index.php?title= सूक्ष्मप्रक्रमक|सूक्ष्मप्रक्रमक]] का [[औपचारिक सत्यापन]],<ref name="Bryant.German.Velev.1999" />स्वत: परीक्षण प्रारूप पीढ़ी, [[एफपीजीए]] की [[Index.php?title= क्रम (इलेक्ट्रॉनिक अभिकल्पन स्वचालन)|क्रम (इलेक्ट्रॉनिक अभिकल्पन स्वचालन)]],<ref>{{Cite journal |last1=Gi-Joon Nam |last2=Sakallah |first2=K. A. |last3=Rutenbar |first3=R. A. |title=A new FPGA detailed routing approach via search-based Boolean satisfiability |journal=IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |volume=21 |issue=6 |pages=674 |year=2002 |url=http://cs-rutenbar.web.engr.illinois.edu/wp-content/uploads/2012/10/rutenbar-sattranscad02.pdf| doi=10.1109/TCAD.2002.1004311}}</ref> [[Index.php?title=स्वचालित योजना और अनुसूचन|स्वचालित योजना और अनुसूचन]], और [[Index.php?title=अनुसूचन कलनविधि|अनुसूचन कलनविधि]], और इसी तरह। इलेक्ट्रॉनिक अभिकल्पन स्वचालन उपकरण पेटी में एक सैट-सॉल्विंग इंजन को भी एक आवश्यक घटक माना जाता है।
-आधुनिक सैट समाधानकर्ता द्वारा उपयोग की जाने वाली प्रमुख तकनीकों में डेविस-पुटनम-लॉगमैन-लवलैंड कलनविधि (या डीपीएलएल), [[संघर्ष-संचालित क्लॉज लर्निंग|संघर्ष-संचालित खंड लर्निंग]] (सीडीसीएल), और [[वॉकसैट]] जैसे [[स्टोकेस्टिक]] लोकल सर्च (कंस्ट्रेंट संतुष्टि) कलनविधि शामिल हैं। लगभग सभी सैट समाधानकर्ता में समय समाप्त शामिल है, इसलिए वे उचित समय में समाप्त हो जाएंगे, भले ही उन्हें समाधान नहीं मिल रहा हो।
+आधुनिक सैट समाधानकर्ता द्वारा उपयोग की जाने वाली प्रमुख तकनीकों में डेविस-पुटनम-लॉगमैन-लवलैंड कलनविधि (या डीपीएलएल), [[संघर्ष-संचालित क्लॉज लर्निंग|संघर्ष-संचालित खंड लर्निंग]] (सीडीसीएल), और [[वॉकसैट]] जैसे [[स्टोकेस्टिक]] लोकल सर्च (कंस्ट्रेंट संतुष्टि) कलनविधि सम्मलित हैं। लगभग सभी सैट समाधानकर्ता में समय समाप्त सम्मलित है, इसलिए वे उचित समय में समाप्त हो जाएंगे, भले ही उन्हें समाधान नहीं मिल रहा हो।
-अलग-अलग सैट  समाधानकर्ता अलग-अलग उदाहरणों को आसान या कठिन पाएंगे, और कुछ असंतोष साबित करने में उत्कृष्ट होंगे, और अन्य समाधान खोजने में। गहन शिक्षण तकनीकों का उपयोग करके एक उदाहरण की संतुष्टि को जानने के लिए हाल ही में प्रयास किए गए हैं।<ref>{{cite arXiv |last1=Selsam |first1=Daniel |last2=Lamm |first2=Matthew |last3=Bünz |first3=Benedikt |last4=Liang |first4=Percy |last5=de Moura |first5=Leonardo |last6=Dill |first6=David L. |title=Learning a SAT Solver from Single-Bit Supervision |eprint=1802.03685 |date=11 March 2019|class=cs.AI }}</ref>
+अलग-अलग सैट  समाधानकर्ता अलग-अलग उदाहरणों को आसान या कठिन पाएंगे, और कुछ असंतोष सिद्ध करने में उत्कृष्ट होंगे, और अन्य समाधान खोजने में। गहन शिक्षण तकनीकों का उपयोग करके एक उदाहरण की संतुष्टि को जानने के लिए हाल ही में प्रयास किए गए हैं।<ref>{{cite arXiv |last1=Selsam |first1=Daniel |last2=Lamm |first2=Matthew |last3=Bünz |first3=Benedikt |last4=Liang |first4=Percy |last5=de Moura |first5=Leonardo |last6=Dill |first6=David L. |title=Learning a SAT Solver from Single-Bit Supervision |eprint=1802.03685 |date=11 March 2019|class=cs.AI }}</ref>
 सैट समाधानकर्ता विकसित किए जाते हैं और सैट-सॉल्विंग प्रतियोगिताओं में उनकी तुलना की जाती है।<ref>{{cite web|url=http://www.satcompetition.org/ |title=The international SAT Competitions web page|access-date=2007-11-15}}</ref> आधुनिक सैट समाधानकर्ता का सॉफ्टवेयर सत्यापन, कृत्रिम बुद्धि में बाधाओं को हल करने, और संचालन अनुसंधान सहित अन्य क्षेत्रों पर भी महत्वपूर्ण प्रभाव पड़ रहा है।
@@ Line 519: / Line 519: @@
 {{Logic}}
-{{DEFAULTSORT:Boolean Satisfiability Problem}}[[Category: बूलियन बीजगणित]] [[Category: इलेक्ट्रॉनिक डिजाइन स्वचालन]] [[Category: औपचारिक तरीके]] [[Category: कंप्यूटर विज्ञान में तर्क]] [[Category: एनपी-पूर्ण समस्याएं]] [[Category: संतुष्टि की समस्या]]
+{{DEFAULTSORT:Boolean Satisfiability Problem}}
+[[Category:All articles needing additional references|Boolean Satisfiability Problem]]
+[[Category:All articles with unsourced statements|Boolean Satisfiability Problem]]
-[[Category: Machine Translated Page]]
+[[Category:Articles needing additional references from May 2020|Boolean Satisfiability Problem]]
-[[Category:Created On 13/02/2023]]
+[[Category:Articles with hatnote templates targeting a nonexistent page|Boolean Satisfiability Problem]]
+[[Category:Articles with invalid date parameter in template|Boolean Satisfiability Problem]]
+[[Category:Articles with unsourced statements from May 2020|Boolean Satisfiability Problem]]
+[[Category:CS1|Boolean Satisfiability Problem]]
+[[Category:CS1 English-language sources (en)]]
+[[Category:Collapse templates|Boolean Satisfiability Problem]]
+[[Category:Commons category link is the pagename|Boolean Satisfiability Problem]]
+[[Category:Created On 13/02/2023|Boolean Satisfiability Problem]]
+[[Category:Lua-based templates|Boolean Satisfiability Problem]]
+[[Category:Machine Translated Page|Boolean Satisfiability Problem]]
+[[Category:Missing redirects|Boolean Satisfiability Problem]]
+[[Category:Navigational boxes| ]]
+[[Category:Navigational boxes without horizontal lists|Boolean Satisfiability Problem]]
+[[Category:Pages with empty portal template|Boolean Satisfiability Problem]]
+[[Category:Pages with script errors|Boolean Satisfiability Problem]]
+[[Category:Portal-inline template with redlinked portals|Boolean Satisfiability Problem]]
+[[Category:Short description with empty Wikidata description|Boolean Satisfiability Problem]]
+[[Category:Sidebars with styles needing conversion|Boolean Satisfiability Problem]]
+[[Category:Template documentation pages|Documentation/doc]]
+[[Category:Templates Vigyan Ready|Boolean Satisfiability Problem]]
+[[Category:Templates generating microformats|Boolean Satisfiability Problem]]
+[[Category:Templates that add a tracking category|Boolean Satisfiability Problem]]
+[[Category:Templates that are not mobile friendly|Boolean Satisfiability Problem]]
+[[Category:Templates that generate short descriptions|Boolean Satisfiability Problem]]
+[[Category:Templates using TemplateData|Boolean Satisfiability Problem]]
+[[Category:Wikipedia metatemplates|Boolean Satisfiability Problem]]
+[[Category:इलेक्ट्रॉनिक डिजाइन स्वचालन|Boolean Satisfiability Problem]]
+[[Category:एनपी-पूर्ण समस्याएं|Boolean Satisfiability Problem]]
+[[Category:औपचारिक तरीके|Boolean Satisfiability Problem]]
+[[Category:कंप्यूटर विज्ञान में तर्क|Boolean Satisfiability Problem]]
+[[Category:बूलियन बीजगणित|Boolean Satisfiability Problem]]
+[[Category:संतुष्टि की समस्या|Boolean Satisfiability Problem]]

Anonymous

Search

बूलियन संतुष्टि समस्या: Difference between revisions

Namespaces

More

Page actions

Latest revision as of 10:13, 24 February 2023

Contents

परिभाषाएँ

संयोजक सामान्य रूप

जटिलता

3-संतोषजनकता

संयोजक सामान्य रूप

वियोगात्मक सामान्य रूप

बिल्कुल-1 3-संतोषजनकता

नहीं-सब-बराबर 3-संतोषजनक

रैखिक सैट

2-संतुष्टि

हॉर्न-संतुष्टि

एक्सओआर-संतुष्टि

शेफर का द्विभाजन प्रमेय

सैट का विस्तार

एक संतोषजनक समनुदेशन ढूँढना

सैट को हल करने के लिए कलनविधि

यह भी देखें

टिप्पणियाँ

बाहरी संबंध

संदर्भ

अग्रिम पठन

Navigation

Navigation

Wiki tools

Wiki tools

Anonymous

Search

बूलियन संतुष्टि समस्या: Difference between revisions

Latest revision as of 10:13, 24 February 2023

परिभाषाएँ

संयोजक सामान्य रूप

जटिलता

3-संतोषजनकता

संयोजक सामान्य रूप

वियोगात्मक सामान्य रूप

बिल्कुल-1 3-संतोषजनकता

नहीं-सब-बराबर 3-संतोषजनक

रैखिक सैट

2-संतुष्टि

हॉर्न-संतुष्टि

एक्सओआर-संतुष्टि

शेफर का द्विभाजन प्रमेय

सैट का विस्तार

एक संतोषजनक समनुदेशन ढूँढना

सैट को हल करने के लिए कलनविधि

यह भी देखें

टिप्पणियाँ

बाहरी संबंध

संदर्भ

अग्रिम पठन

Navigation

Wiki tools

Page tools

Other projects

Categories