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

Revision as of 16:53, 17 February 2023

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

सैट पहली समस्या है जो एनपी-पूर्ण साबित हुई थी; कुक–लेविन प्रमेय देखें। इसका मतलब यह है कि जटिलता वर्ग एनपी (जटिलता) में सभी समस्याएं, जिसमें प्राकृतिक निर्णय और अनुकूलन समस्याओं की एक विस्तृत श्रृंखला शामिल है, को सैट के रूप में हल करना मुश्किल है। ऐसा कोई ज्ञात कलनविधि नहीं है जो प्रत्येक सैट समस्या को कुशलतापूर्वक हल करता हो, और आमतौर पर यह माना जाता है कि ऐसा कोई कलनविधि मौजूद नहीं है; अभी तक यह विश्वास गणितीय रूप से सिद्ध नहीं हुआ है, और इस सवाल को हल करना कि क्या सैट के पास बहुपद-समय कलनविधि है, 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 की कमी। 'र' का परिणाम है TRUE (1) यदि इसका एक तर्क सही है, और FALSE (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 XOR-सैट example
by Gaussian elimination

Given formula
("⊕" means XOR, 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]} यह पी (जटिलता वर्ग) में है, चूंकि एक्सओआर-सैट सूत्र को रैखिक समीकरण मॉड 2 की प्रणाली के रूप में भी देखा जा सकता है, और गॉसियन उन्मूलन द्वारा क्यूबिक समय में हल किया जा सकता है;^[18] उदाहरण के लिए बॉक्स देखें। यह पुनर्रचना बूलियन बीजगणित (संरचना)#बूलियन रिंग्स पर आधारित है, और यह तथ्य कि अंकगणितीय मोडुलो दो एक परिमित क्षेत्र बनाते हैं। चूँकि एक XOR b XOR c ट्रू का मूल्यांकन करता है यदि और केवल यदि {a,b,c} के ठीक 1 या 3 सदस्य ट्रू हैं, तो किसी दिए गए सीएनएफ सूत्र के लिए 1-इन-3-सैट समस्या का प्रत्येक समाधान भी एक समाधान है XOR-3-सैट समस्या का, और बदले में XOR-3-सैट का प्रत्येक समाधान 3-सैट, cf का समाधान है। चित्र। परिणामस्वरूप, प्रत्येक सीएनएफ सूत्र के लिए, सूत्र द्वारा परिभाषित XOR-3-सैट समस्या को हल करना संभव है, और परिणाम के आधार पर अनुमान लगाया जाता है कि 3-सैट समस्या हल करने योग्य है या 1-में-3- सैट समस्या हल करने योग्य नहीं है।

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

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

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

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

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


Code	Name	Restrictions	Requirements	Class
3सैट	3-सैटisfiability	Each clause contains 3 literals.	At least one literal must be ट्रू.	NPC
2सैट	2-सैटisfiability	Each clause contains 2 literals.	At least one literal must be ट्रू.	P
1-in-3-सैट	Exactly-1 3-सैट	Each clause contains 3 literals.	Exactly one literal must be ट्रू.	NPC
1-in-3-सैट+	Exactly-1 Positive 3-सैट	Each clause contains 3 positive literals.	Exactly one literal must be ट्रू.	NPC
NAE3सैट	Not-all-equal 3-सैटisfiability	Each clause contains 3 literals.	Either one or two literals must be ट्रू.	NPC
NAE3सैट+	Not-all-equal positive 3-सैट	Each clause contains 3 positive literals.	Either one or two literals must be ट्रू.	NPC
PL-सैट	Planar सैट	The incidence graph (clause-variable graph) is planar.	At least one literal must be ट्रू.	NPC
Lसैट	Linear सैट	Each clause contains 3 literals, intersects at most one other clause, and the intersection is exactly one literal.	At least one literal must be ट्रू.	NPC
HORN-सैट	Horn सैटisfiability	Horn clauses (at most one positive literal).	At least one literal must be ट्रू.	P
XOR-सैट	Xor सैटisfiability	Each clause contains XOR operations rather than OR.	The XOR of all literals must be ट्रू.	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=फॉल्स अन्य। सैट स्वयं (मौन रूप से) केवल ∃ क्वांटिफायर का उपयोग करता है। यदि इसके बजाय केवल ∀ क्वांटिफायर की अनुमति है, तथाकथित 'टॉटोलॉजी (तर्क) समस्या' प्राप्त की जाती है, जो सह-एनपी-पूर्ण है। यदि दोनों परिमाणकों की अनुमति है, तो समस्या को 'मात्राबद्ध बूलियन सूत्र समस्या' ('क्यूबीएफ') कहा जाता है, जिसे पीएसपीएसीई-पूर्ण दिखाया जा सकता है। यह व्यापक रूप से माना जाता है कि एनपी में किसी भी समस्या की तुलना में पीएसपीएसीई-पूर्ण समस्याएं सख्ती से कठिन हैं, हालांकि यह अभी तक सिद्ध नहीं हुआ है। अत्यधिक समानांतर पी प्रणाली का उपयोग करके, QBF-सैट समस्याओं को रैखिक समय में हल किया जा सकता है।^[20] सामान्य सैट पूछता है कि क्या कम से कम एक परिवर्तनीय समनुदेशन है जो सूत्र को सत्य बनाता है। विभिन्न प्रकार के वेरिएंट ऐसे समनुदेशन की संख्या से निपटते हैं:

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

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

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

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

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

एनपी (जटिलता) ⊆ पी/पॉली ⇒ पीएच (जटिलता) = बहुपद पदानुक्रम#परिभाषाएं|Σ₂(कार्प-लिप्टन प्रमेय)

एनपी (जटिलता) ⊆ बीपीपी (जटिलता) ⇒ एनपी (जटिलता) = आरपी (जटिलता)

पी (जटिलता) = एनपी (जटिलता) ⇒ एफपी (जटिलता) = एफएनपी (जटिलता)

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

चूंकि सैट समस्या एनपी-पूर्ण है, केवल घातीय सबसे खराब स्थिति वाले कलनविधि इसके लिए जाने जाते हैं। इसके बावजूद, सैट के लिए कुशल और स्केलेबल कलनविधि 2000 के दशक के दौरान विकसित किए गए थे और हजारों चर और लाखों बाधाओं (यानी खंड) से जुड़े समस्या उदाहरणों को स्वचालित रूप से हल करने की हमारी क्षमता में नाटकीय प्रगति में योगदान दिया है।^[1] इलेक्ट्रॉनिक डिजाइन स्वचालन (EDA) में ऐसी समस्याओं के उदाहरणों में औपचारिक तुल्यता जाँच, मॉडल जाँच, माइक्रोप्रोसेसर का औपचारिक सत्यापन,^[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]

Anonymous

Search

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

Namespaces

More

Page actions

Revision as of 16:53, 17 February 2023

Contents

परिभाषाएँ

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

जटिलता

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

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

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

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

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

रैखिक सैट

2-संतुष्टि

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

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

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

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

यह भी देखें

टिप्पणियाँ

बाहरी संबंध

संदर्भ

अग्रिम पठन

Navigation

Navigation

Wiki tools

Wiki tools

@@ Line 1: / Line 1: @@
-{{Redirect|3SAT|the Central European television network|3sat}}
+{{Redirect|3SAT|मध्य यूरोपीय टेलीविजन नेटवर्क|3sat}}
 {{short description|Problem of determining if a Boolean formula could be made true}}
-[[तर्क]] और [[कंप्यूटर विज्ञान]] में, बूलियन [[संतुष्टि]] समस्या (कभी-कभी प्रस्तावित संतुष्टि समस्या और संक्षिप्त संतुष्टि, एसएटी या बी-एसएटी कहा जाता है) यह निर्धारित करने की समस्या है कि क्या कोई [[व्याख्या (तर्क)]] मौजूद है जो किसी दिए गए [[बूलियन तर्क]] [[सूत्र (गणितीय तर्क)]] की संतुष्टि है। . दूसरे शब्दों में, यह पूछता है कि क्या किसी दिए गए बूलियन सूत्र के चर को लगातार TRUE या FALSE मानों द्वारा इस तरह से प्रतिस्थापित किया जा सकता है कि सूत्र TRUE का मूल्यांकन करता है। यदि यह स्थिति है, तो सूत्र को 'संतोषजनक' कहा जाता है। दूसरी ओर, यदि ऐसा कोई असाइनमेंट मौजूद नहीं है, तो सूत्र द्वारा व्यक्त किया गया कार्य सभी संभावित चर असाइनमेंट के लिए औपचारिक तर्क में विरोधाभास # विरोधाभास है और सूत्र ''असंतोषजनक'' है। उदाहरण के लिए, सूत्र ''a'' और नहीं ''b'' संतुष्ट करने योग्य है क्योंकि कोई ''a'' = TRUE और ''b'' = FALSE मान खोज सकता है, जो (''a'' और नहीं ''बी'') = सच। इसके विपरीत, ''ए'' और नहीं ''ए'' असंतोषजनक है।
+[[तर्क]] और [[Index.php?title= संगणक विज्ञान|संगणक विज्ञान]] में, बूलियन [[संतुष्टि]] समस्या (कभी-कभी प्रस्तावित संतुष्टि समस्या और संक्षिप्त संतुष्टि, सैट या बी-सैट कहा जाता है) यह निर्धारित करने की समस्या है कि क्या कोई [[व्याख्या (तर्क)]] मौजूद है जो किसी दिए गए [[बूलियन तर्क]] [[सूत्र (गणितीय तर्क)]] की संतुष्टि है। . दूसरे शब्दों में, यह पूछता है कि क्या किसी दिए गए बूलियन सूत्र के चर को लगातार ट्रू या फॉल्स मानों द्वारा इस तरह से प्रतिस्थापित किया जा सकता है कि सूत्र ट्रू का मूल्यांकन करता है। यदि यह स्थिति है, तो सूत्र को 'संतोषजनक' कहा जाता है। दूसरी ओर, यदि ऐसा कोई समनुदेशन मौजूद नहीं है, तो सूत्र द्वारा व्यक्त किया गया सभी कार्य संभावित चर समनुदेशन के लिए औपचारिक तर्क में विरोधाभास # विरोधाभास है और सूत्र ''असंतोषजनक'' है। उदाहरण के लिए, सूत्र "''a'' और ना ही ''b"'' संतुष्ट करने योग्य है क्योंकि कोई "''a'' = ट्रू और ''b'' = फॉल्स" मान खोज सकता है, जो (''a'' और ना ही ''बी'') = ट्रू। इसके विपरीत, "''ए'' और ना ही ''ए'' " असंतोषजनक है।
-एसएटी पहली समस्या है जो एनपी-पूर्ण साबित हुई थी; कुक–लेविन प्रमेय देखें। इसका मतलब यह है कि जटिलता वर्ग [[एनपी (जटिलता)]] में सभी समस्याएं, जिसमें प्राकृतिक निर्णय और अनुकूलन समस्याओं की एक विस्तृत श्रृंखला शामिल है, को एसएटी के रूप में हल करना मुश्किल है। ऐसा कोई ज्ञात एल्गोरिथम नहीं है जो प्रत्येक SAT समस्या को कुशलतापूर्वक हल करता हो, और आमतौर पर यह माना जाता है कि ऐसा कोई एल्गोरिथम मौजूद नहीं है; अभी तक यह विश्वास गणितीय रूप से सिद्ध नहीं हुआ है, और इस सवाल को हल करना कि क्या SAT के पास बहुपद-समय एल्गोरिथ्म है, P बनाम NP समस्या के बराबर है, जो कंप्यूटिंग के सिद्धांत में एक प्रसिद्ध खुली समस्या है।
+सैट पहली समस्या है जो एनपी-पूर्ण साबित हुई थी; कुक–लेविन प्रमेय देखें। इसका मतलब यह है कि जटिलता वर्ग [[एनपी (जटिलता)]] में सभी समस्याएं, जिसमें प्राकृतिक निर्णय और अनुकूलन समस्याओं की एक विस्तृत श्रृंखला शामिल है, को सैट के रूप में हल करना मुश्किल है। ऐसा कोई ज्ञात कलनविधि नहीं है जो प्रत्येक सैट समस्या को कुशलतापूर्वक हल करता हो, और आमतौर पर यह माना जाता है कि ऐसा कोई कलनविधि मौजूद नहीं है; अभी तक यह विश्वास गणितीय रूप से सिद्ध नहीं हुआ है, और इस सवाल को हल करना कि क्या सैट के पास बहुपद-समय कलनविधि है, P बनाम NP समस्या के बराबर है, जो कंप्यूटिंग के सिद्धांत में एक प्रसिद्ध खुली समस्या है।
-फिर भी, 2007 तक, ह्यूरिस्टिक एसएटी-एल्गोरिदम समस्या के उदाहरणों को हल करने में सक्षम हैं जिनमें हजारों चर शामिल हैं और <!---"clauses" hasn't been introduced here:--->लाखों प्रतीकों से युक्त सूत्र,<ref name="Codish.Ohrimenko.Stuckey.2007"/>जो कई व्यावहारिक एसएटी समस्याओं के लिए पर्याप्त है, उदाहरण के लिए, [[कृत्रिम होशियारी]], [[सर्किट डिज़ाइन]],<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> और [[स्वचालित प्रमेय साबित करना]]।
 == परिभाषाएँ ==
-एक प्रस्तावपरक तर्क सूत्र, जिसे बूलियन अभिव्यक्ति भी कहा जाता है, वेरिएबल (गणित), ऑपरेटरों AND ([[तार्किक संयोजन]], जिसे ∧ द्वारा भी दर्शाया गया है), OR ([[तार्किक विच्छेदन]], ∨), NOT (निषेध, ¬), और कोष्ठकों से बनाया गया है।
+एक प्रस्तावपरक तर्क सूत्र, जिसे बूलियन अभिव्यक्ति भी कहा जाता है, परिवर्ती (गणित), ऑपरेटरों और ([[तार्किक संयोजन]], जिसे ∧ द्वारा भी दर्शाया गया है), या ([[तार्किक विच्छेदन]], ∨), नहीं (निषेध, ¬), और कोष्ठकों से बनाया गया है।
-एक सूत्र को संतोषजनक कहा जाता है यदि इसके चरों को उपयुक्त तार्किक मान (अर्थात TRUE, FALSE) निर्दिष्ट करके इसे TRUE बनाया जा सकता है।
+एक सूत्र को संतोषजनक कहा जाता है यदि इसके चरों को उपयुक्त तार्किक मान (अर्थात ट्रू, फॉल्स) निर्दिष्ट करके इसे ट्रू बनाया जा सकता हो।
-बूलियन संतुष्टि समस्या (एसएटी) को यह जांचने के लिए एक सूत्र दिया गया है कि यह संतोषजनक है या नहीं।
+बूलियन संतुष्टि समस्या (सैट) को यह जांचने के लिए एक सूत्र दिया गया है कि यह संतोषजनक है या नहीं।
-कंप्यूटर विज्ञान के कई क्षेत्रों में यह [[निर्णय समस्या]] केंद्रीय महत्व की है, जिसमें [[सैद्धांतिक कंप्यूटर विज्ञान]], [[कम्प्यूटेशनल जटिलता सिद्धांत]],<ref>{{cite book | last = Karp | first = Richard M. | author-link = Richard Karp | chapter = Reducibility Among Combinatorial Problems | title = Complexity of Computer Computations | editor = Raymond E. Miller | editor2 = James W. Thatcher | publisher = Plenum | location = New York | pages = 85–103 | year = 1972 | chapter-url = http://www.cs.berkeley.edu/~luca/cs172/karp.pdf | isbn = 0-306-30707-3 | access-date = 2020-05-07 | archive-date = 2011-06-29 | archive-url = https://web.archive.org/web/20110629023717/http://www.cs.berkeley.edu/~luca/cs172/karp.pdf | url-status = dead }} Here: p.86</ref><ref>{{cite book | isbn=0-201-00029-6 |first1=Alfred V. |last1=Aho |first2=John E. |last2=Hopcroft |first3=Jeffrey D. |last3=Ullman | title=The Design and Analysis of Computer Algorithms | publisher=Addison-Wesley | year=1974 |page=403}}</ref> एल्गोरिदम, [[क्रिप्टोग्राफी]]<ref>{{Cite journal|last1=Massacci|first1=Fabio|last2=Marraro|first2=Laura|date=2000-02-01|title=Logical Cryptanalysis as a SAT Problem |journal=Journal of Automated Reasoning |volume=24|issue=1|pages=165–203|doi=10.1023/A:1006326723002|s2cid=3114247 }}</ref><ref>{{Cite journal|last1=Mironov|first1=Ilya|last2=Zhang|first2=Lintao|date=2006|editor-last=Biere|editor-first=Armin|editor2-last=Gomes|editor2-first=Carla P.|title=Applications of SAT Solvers to Cryptanalysis of Hash Functions|url=https://link.springer.com/chapter/10.1007%2F11814948_13|journal=Theory and Applications of Satisfiability Testing — SAT 2006|series=Lecture Notes in Computer Science|volume=4121 |publisher=Springer|pages=102–115|doi=10.1007/11814948_13|isbn=978-3-540-37207-3}}</ref> और कृत्रिम बुद्धि।<ref>{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | pages = 2021–2035 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=Boolean Satisfiability Solvers and Their Applications in Model Checking| s2cid = 10190144 }}</ref>{{additional citations needed|date=May 2020}}
+कंप्यूटर विज्ञान के कई क्षेत्रों में यह [[निर्णय समस्या]] केंद्रीय महत्व की है, जिसमें [[सैद्धांतिक कंप्यूटर विज्ञान]], [[Index.php?title=संगणनात्मक जटिलता सिद्धांत|संगणनात्मक जटिलता सिद्धांत]],<ref>{{cite book | last = Karp | first = Richard M. | author-link = Richard Karp | chapter = Reducibility Among Combinatorial Problems | title = Complexity of Computer Computations | editor = Raymond E. Miller | editor2 = James W. Thatcher | publisher = Plenum | location = New York | pages = 85–103 | year = 1972 | chapter-url = http://www.cs.berkeley.edu/~luca/cs172/karp.pdf | isbn = 0-306-30707-3 | access-date = 2020-05-07 | archive-date = 2011-06-29 | archive-url = https://web.archive.org/web/20110629023717/http://www.cs.berkeley.edu/~luca/cs172/karp.pdf | url-status = dead }} Here: p.86</ref><ref>{{cite book | isbn=0-201-00029-6 |first1=Alfred V. |last1=Aho |first2=John E. |last2=Hopcroft |first3=Jeffrey D. |last3=Ullman | title=The Design and Analysis of Computer Algorithms | publisher=Addison-Wesley | year=1974 |page=403}}</ref> कलनविधि, [[Index.php?title= कूटलेखन|कूटलेखन]]<ref>{{Cite journal|last1=Massacci|first1=Fabio|last2=Marraro|first2=Laura|date=2000-02-01|title=Logical Cryptanalysis as a SAT Problem |journal=Journal of Automated Reasoning |volume=24|issue=1|pages=165–203|doi=10.1023/A:1006326723002|s2cid=3114247 }}</ref><ref>{{Cite journal|last1=Mironov|first1=Ilya|last2=Zhang|first2=Lintao|date=2006|editor-last=Biere|editor-first=Armin|editor2-last=Gomes|editor2-first=Carla P.|title=Applications of SAT Solvers to Cryptanalysis of Hash Functions|url=https://link.springer.com/chapter/10.1007%2F11814948_13|journal=Theory and Applications of Satisfiability Testing — SAT 2006|series=Lecture Notes in Computer Science|volume=4121 |publisher=Springer|pages=102–115|doi=10.1007/11814948_13|isbn=978-3-540-37207-3}}</ref> और कृत्रिम बुद्धि।<ref>{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | pages = 2021–2035 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=Boolean Satisfiability Solvers and Their Applications in Model Checking| s2cid = 10190144 }}</ref>{{additional citations needed|date=May 2020}}
@@ 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>= FALSE, और x<sub>3</sub> मनमाने ढंग से, क्योंकि (FALSE ∨ ¬FALSE) ∧ (¬FALSE ∨ FALSE ∨ x<sub>3</sub>) ∧ ¬FALSE (FALSE ∨ TRUE) ∧ (TRUE ∨ FALSE ∨ x) का मूल्यांकन करता है<sub>3</sub>) ∧ TRUE, और बदले में TRUE ∧ TRUE ∧ TRUE (यानी TRUE के लिए)। इसके विपरीत, CNF सूत्र a ∧ ¬a, जिसमें एक शाब्दिक के दो खंड शामिल हैं, असंतुष्ट है, क्योंकि a=TRUE या a=FALSE के लिए यह TRUE ∧ ¬TRUE (अर्थात, FALSE) या FALSE ∧ ¬FALSE (यानी , फिर से FALSE), क्रमशः।
+उदाहरण के लिए, {{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=फॉल्स के लिए यह ट्रू ∧ ¬ट्रू (अर्थात, फॉल्स) या फॉल्स ∧ ¬फॉल्स (यानी , फिर से फॉल्स), क्रमशः।
-SAT समस्या के कुछ संस्करणों के लिए,<!---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>)}} कुछ [[बूलियन समारोह]] 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) एक सामान्यीकृत खंड है संयुक्त सामान्य रूप। इस सूत्र का उपयोग #Exactly-1 3-satisfiability के साथ किया जाता है, जिसमें R टर्नरी ऑपरेटर होता है जो TRUE होता है जब इसका कोई एक तर्क होता है।
+सैट समस्या के कुछ संस्करणों के लिए,<!---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.--->
 [[बूलियन बीजगणित (संरचना)]] के नियमों का उपयोग करते हुए, प्रत्येक प्रस्तावपरक तर्क सूत्र को समतुल्य संयोजन सामान्य रूप में परिवर्तित किया जा सकता है, जो कि, हालांकि, घातीय रूप से लंबा हो सकता है। उदाहरण के लिए, सूत्र को बदलना
-(एक्स<sub>1</sub>∧y<sub>1</sub>) ∨ (एक्स<sub>2</sub>∧y<sub>2</sub>) ∨ ... ∨ (एक्स<sub>''n''</sub>∧y<sub>''n''</sub>)
+(x<sub>1</sub>∧y<sub>1</sub>) ∨ (x<sub>2</sub>∧y<sub>2</sub>) ∨ ... ∨ (x<sub>''n''</sub>∧y<sub>''n''</sub>)
-संयोजन सामान्य रूप में पैदावार
+संयोजन सामान्य रूप में उत्पन्न
 :{{math|(''x''<sub>1</sub>&nbsp;∨&nbsp;''x''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''<sub>''n''</sub>) ∧}}
 :{{math|(''y''<sub>1</sub>&nbsp;∨&nbsp;''x''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''x''<sub>''n''</sub>) ∧}}
@@ Line 34: / Line 34: @@
 :{{math|(''x''<sub>1</sub>&nbsp;∨&nbsp;''y''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''<sub>''n''</sub>) ∧}}
 :{{math|(''y''<sub>1</sub>&nbsp;∨&nbsp;''y''<sub>2</sub>&nbsp;∨&nbsp;…&nbsp;∨&nbsp;''y''<sub>''n''</sub>)}};
-जबकि पूर्व 2 चर के n संयोजनों का संयोजन है, बाद वाले में 2 होते हैं<sup>n</sup> n चरों के उपवाक्य।
+जबकि पूर्व 2 चर के n संयोजनों का संयोजन है, बाद वाले में 2<sup>n</sup> n चरों के उपवाक्य होते हैं।
-हालांकि, Tseytin परिवर्तन के उपयोग के साथ, हम मूल प्रस्तावपरक तर्क सूत्र के आकार में लंबाई रैखिक के साथ एक समतुल्य संयुग्मन सामान्य रूप सूत्र पा सकते हैं।
+हालांकि,टेसीटिन परिवर्तन के उपयोग के साथ, हम मूल प्रस्तावपरक तर्क सूत्र के आकार में लंबाई रैखिक के साथ एक समतुल्य संयुग्मन सामान्य रूप सूत्र पा सकते हैं।
 == जटिलता ==
-{{Main|Cook–Levin theorem}}
+{{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> उस समय तक, एनपी-पूर्ण समस्या की अवधारणा मौजूद ही नहीं थी।
-सबूत दिखाता है कि कैसे [[जटिलता वर्ग]] एनपी (जटिलता) में हर निर्णय समस्या सीएनएफ के लिए एसएटी समस्या में [[कमी (जटिलता)]] हो सकती है<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> सूत्र, जिन्हें कभी-कभी CNFSAT कहा जाता है।
+उदाहरण दिखाता है कि कैसे [[जटिलता वर्ग]] एनपी (जटिलता) में हर निर्णय समस्या सीएनएफ के लिए सैट समस्या में [[कमी (जटिलता)]] हो सकती है<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-रंग हैं, तो कुक-लेविन कटौती द्वारा निर्मित SAT सूत्र में 17 संतोषजनक कार्य होंगे।
+कुक के रिडक्शन का एक उपयोगी गुण यह है कि यह स्वीकृत उत्तरों की संख्या को सुरक्षित रखता है। उदाहरण के लिए, यह तय करना कि क्या किसी दिए गए आरेख (असतत गणित) में आरेख रंग# शीर्ष् रंग 3-कलरिंग एनपी में एक और समस्या है; यदि किसी आरेख में 17 मान्य 3-रंग हैं, तो कुक-लेविन कटौती द्वारा निर्मित सैट सूत्र में 17 संतोषजनक कार्य होंगे।
-एनपी-पूर्णता केवल सबसे खराब स्थिति के रन-टाइम को संदर्भित करती है। व्यावहारिक अनुप्रयोगों में आने वाले कई उदाहरणों को और अधिक तेज़ी से हल किया जा सकता है। नीचे SAT को हल करने के लिए #Algorithms देखें।
+एनपी-पूर्णता केवल सबसे खराब स्थिति के कार्य अवधि को संदर्भित करती है। व्यावहारिक अनुप्रयोगों में आने वाले कई उदाहरणों को और अधिक तेज़ी से हल किया जा सकता है। नीचे सैट को हल करने के लिए #कलनविधि देखें।
 ===3-संतोषजनकता===
-[[File:Sat reduced to Clique from Sipser.svg|thumb|upright=1.25|3-सैट उदाहरण {{math|(''x'' ∨ ''x'' ∨ ''y'') ∧ (¬''x'' ∨ ¬''y'' ∨ ¬''y'') ∧ (¬''x'' ∨ ''y'' ∨ ''y'')}} एक [[क्लिक समस्या]] में कमी। हरे कोने एक 3-क्लिक बनाते हैं और संतोषजनक असाइनमेंट x=FALSE, y=TRUE के अनुरूप होते हैं।]]मनमाना सूत्रों के लिए संतुष्टि की समस्या की तरह, संयोजन सामान्य रूप में एक सूत्र की संतुष्टि का निर्धारण करना जहां प्रत्येक खंड अधिकतम तीन शाब्दिकों तक सीमित है, एनपी-पूर्ण भी है; इस समस्या को 3-SAT, 3CNFSAT, या 3-संतोषजनक कहा जाता है।
+[[File:Sat reduced to Clique from Sipser.svg|thumb|upright=1.25|3-सैट उदाहरण {{math|(''x'' ∨ ''x'' ∨ ''y'') ∧ (¬''x'' ∨ ¬''y'' ∨ ¬''y'') ∧ (¬''x'' ∨ ''y'' ∨ ''y'')}} एक [[क्लिक समस्या]] में कमी। हरे कोने एक 3-क्लिक बनाते हैं और संतोषजनक समनुदेशन x=फॉल्स, y=ट्रू के अनुरूप होते हैं।]]मनमाने सूत्रों के लिए संतुष्टि की समस्या की तरह, संयोजन सामान्य रूप में एक सूत्र की संतुष्टि का निर्धारण करना जहां प्रत्येक खंड अधिकतम तीन शाब्दिकों तक सीमित है, एनपी-पूर्ण भी है; इस समस्या को 3-सैट, 3सीएनएफ सैट, या 3-संतोषजनकता कहा जाता है।
-अप्रतिबंधित SAT समस्या को 3-SAT तक कम करने के लिए, प्रत्येक खंड को रूपांतरित करें {{math|''l''<sub>1</sub> ∨ ⋯ ∨ ''l''<sub>''n''</sub>}} के संयोजन के लिए {{math|''n'' - 2}} खंड
+अप्रतिबंधित सैट समस्या को 3-सैट तक कम करने के लिए, प्रत्येक खंड को रूपांतरित करें {{math|''l''<sub>1</sub> ∨ ⋯ ∨ ''l''<sub>''n''</sub>}} के संयोजन के लिए {{math|''n'' - 2}} खंड
 :{{math|(''l''<sub>1</sub> ∨ ''l''<sub>2</sub> ∨ ''x''<sub>2</sub>) ∧ }}
 :{{math|(¬''x''<sub>2</sub> ∨ ''l''<sub>3</sub> ∨ ''x''<sub>3</sub>) ∧ }}
@@ Line 55: / Line 55: @@
 :{{math|(¬''x''<sub>''n'' − 3</sub> ∨ ''l''<sub>''n'' − 2</sub> ∨ ''x''<sub>''n'' − 2</sub>) ∧ }}
 :{{math|(¬''x''<sub>''n'' − 2</sub> ∨ ''l''<sub>''n'' − 1</sub> ∨ ''l''<sub>''n''</sub>)}}
-कहाँ {{math|''x''<sub>2</sub>,&thinsp;⋯&thinsp;,&thinsp;''x''<sub>''n'' − 2</sub>}} ताजा चर हैं जो कहीं और नहीं होते हैं।
+जहाँ {{math|''x''<sub>2</sub>,&thinsp;⋯&thinsp;,&thinsp;''x''<sub>''n'' − 2</sub>}} ताजा चर हैं जो कहीं और नहीं होते हैं।
-यद्यपि दो सूत्र तार्किक रूप से समतुल्य नहीं हैं, वे समान हैं। सभी खंडों को बदलने से उत्पन्न होने वाला सूत्र अपने मूल से अधिक से अधिक 3 गुना लंबा है, अर्थात लंबाई वृद्धि बहुपद है।{{sfnp|Aho|Hopcroft|Ullman|1974|loc=Theorem 10.4}}
+यद्यपि दो सूत्र तार्किक रूप से समतुल्य नहीं हैं, वे समान्य: हैं। सभी खंडों को बदलने से उत्पन्न होने वाला सूत्र अपने मूल से अधिक से अधिक 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-एसएटी से दूसरी समस्या में [[बहुपद-समय में कमी]] के द्वारा किया जाता है। एक समस्या का एक उदाहरण जहां इस पद्धति का उपयोग किया गया है, क्लिक समस्या है: एक सीएनएफ फॉर्मूला दिया गया है जिसमें सी खंड शामिल हैं, संबंधित ग्राफ (असतत गणित) में प्रत्येक शाब्दिक के लिए एक शीर्ष होता है, और प्रत्येक दो गैर-विरोधाभासी के बीच एक किनारा होता है<ref group=note>i.e. such that one literal is not the negation of the other</ref> विभिन्न खंडों से शाब्दिक, सीएफ। चित्र। ग्राफ़ में एक सी-क्लिक है अगर और केवल अगर सूत्र संतोषजनक है।{{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-SAT प्रस्ताव में चरों की संख्या है, और 3-SAT को सही ढंग से तय करने की उच्च संभावना के साथ सफल होता है।<ref name="Schoning.1999">{{cite book| last1=Schöning| first1=Uwe| chapter=A Probabilistic Algorithm for ''k''-SAT and Constraint Satisfaction Problems| title=Proc. 40th Ann. Symp. Foundations of Computer Science| pages=410–414| date=Oct 1999| 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>
+शॉनिंग (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''))}} समय (यानी, एन में घातीय से मौलिक रूप से तेज़)।
+[[घातीय समय परिकल्पना]] का दावा है कि कोई भी कलनविधि 3-सैट (या वास्तव में किसी भी के लिए के-सैट) को हल नहीं कर सकता है {{tmath|k > 2}}) में {{math|exp([[Small o notation#Little-o notation|''o'']](''n''))}} समय (यानी, n में घातीय से मौलिक रूप से तेज़)।
-सेलमैन, मिशेल, और लेवेस्क (1996) अपने आकार के मापदंडों के आधार पर बेतरतीब ढंग से उत्पन्न 3-एसएटी सूत्रों की कठिनाई पर अनुभवजन्य डेटा देते हैं।
+सेलमैन, मिशेल, और लेवेस्क (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>
+कठिनाई को [[डीपीएलएल एल्गोरिदम|डीपीएलएल कलनविधि]] द्वारा की गई संख्या पुनरावर्ती संकेत में मापा जाता है। उन्होंने एक चरण संक्रमण क्षेत्र की पहचान लगभग निश्चित रूप से संतोषजनक से लगभग निश्चित रूप से असंतोषजनक सूत्र के खंड-दर-चर अनुपात में लगभग 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>
--संतोषजनकता को के-संतोषजनकता (के-एसएटी, के-सीएनएफ-एसएटी) के लिए सामान्यीकृत किया जा सकता है, जब सीएनएफ में सूत्रों को 'के' अक्षर तक के प्रत्येक खंड के साथ माना जाता है।{{citation needed|date=May 2020}}
+-संतोषजनकता को '''k'''-संतोषजनकता ('''k'''-सैट, '''k'''-सीएनएफ-सैट) के लिए सामान्यीकृत किया जा सकता है, जब सीएनएफ में सूत्रों को ''''k'''<nowiki/>' अक्षर तक के प्रत्येक खंड के साथ माना जाता है।{{citation needed|date=May 2020}}
-हालाँकि, किसी भी k ≥ 3 के लिए, यह समस्या न तो 3-SAT से आसान हो सकती है और न ही SAT से कठिन, और बाद के दो NP-पूर्ण हैं, इसलिए k-SAT होना चाहिए।
+हालाँकि, किसी भी k ≥ 3 के लिए, यह समस्या न तो 3-सैट से आसान हो सकती है और न ही सैट से कठिन, और बाद के दो NP-पूर्ण हैं, इसलिए k-सैट होना चाहिए।
-कुछ लेखक k-SAT को 'बिल्कुल k शाब्दिक' के साथ CNF फ़ार्मुलों तक सीमित रखते हैं।{{citation needed|date=May 2020}} यह प्रत्येक क्लॉज के रूप में एक अलग जटिलता वर्ग की ओर नहीं ले जाता है {{math|''l''<sub>1</sub> ∨ ⋯ ∨ ''l''<sub>''j''</sub>}} with j <k लिटरल को फिक्स्ड डमी वेरिएबल्स के साथ पैडेड किया जा सकता है
+कुछ लेखक k-सैट को 'बिल्कुल k शाब्दिक' के साथ सीएनएफ सूत्र तक सीमित रखते हैं।{{citation needed|date=May 2020}} यह प्रत्येक खंड के रूप में एक अलग जटिलता वर्ग की ओर नहीं ले जाता है {{math|''l''<sub>1</sub> ∨ ⋯ ∨ ''l''<sub>''j''</sub>}} with j <k लिटरल को निर्धारित डमी चर के साथ पैडेड किया जा सकता है
 {{math|''l''<sub>1</sub> ∨ ⋯ ∨ ''l''<sub>''j''</sub> ∨ ''d''<sub>''j''+1</sub> ∨ ⋯ ∨ ''d''<sub>''k''</sub>}}.
-सभी खंडों को भरने के बाद, 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''}}.
+सभी खंडों को भरने के बाद, 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 शाब्दिक प्रति खंड के साथ) को अक्सर SAT सूत्रों के लिए विहित प्रतिनिधित्व माना जाता है। जैसा कि ऊपर दिखाया गया है, सामान्य एसएटी समस्या 3-एसएटी तक कम हो जाती है, इस रूप में सूत्रों के लिए संतुष्टि का निर्धारण करने की समस्या।
+संयोजक सामान्य रूप (विशेष रूप से 3 शाब्दिक प्रति खंड के साथ) को अक्सर सैट सूत्रों के लिए विहित प्रतिनिधित्व माना जाता है। जैसा कि ऊपर दिखाया गया है, सामान्य सैट समस्या 3-सैट तक कम हो जाती है, इस रूप में सूत्रों के लिए संतुष्टि का निर्धारण करने की समस्या।
 === वियोगात्मक सामान्य रूप ===
-एसएटी तुच्छ है यदि सूत्र उन लोगों तक सीमित हैं जो वियोगात्मक सामान्य रूप में हैं, अर्थात, वे शाब्दिक संयोजनों के संयोजन हैं। इस तरह का एक सूत्र वास्तव में संतोषजनक है अगर और केवल अगर इसके संयोजनों में से कम से कम एक संतोषजनक है, और एक संयोजन संतोषजनक है अगर और केवल अगर इसमें कुछ चर '' के लिए '' x '' और नहीं '' x '' दोनों शामिल नहीं हैं। एक्स''। इसे रैखिक समय में चेक किया जा सकता है। इसके अलावा, यदि वे पूर्ण वियोगात्मक सामान्य रूप में होने के लिए प्रतिबंधित हैं, जिसमें प्रत्येक चर प्रत्येक संयुग्मन में ठीक एक बार दिखाई देता है, तो उन्हें निरंतर समय में चेक किया जा सकता है (प्रत्येक संयुग्मन एक संतोषजनक असाइनमेंट का प्रतिनिधित्व करता है)। लेकिन सामान्य एसएटी समस्या को अलग करने वाले सामान्य रूप में परिवर्तित करने में घातीय समय और स्थान लग सकता है; उदाहरण के लिए संयोजन सामान्य रूपों के लिए #परिभाषा एक्सपोनेंशियल ब्लो-अप उदाहरण में ∧ और ∨ का आदान-प्रदान करें।
+सैट नगण्य है यदि सूत्र उन लोगों तक सीमित हैं जो वियोगात्मक सामान्य रूप में हैं, अर्थात, वे शाब्दिक संयोजनों के संयोजन हैं। इस तरह का एक सूत्र वास्तव में संतोषजनक है अगर और केवल अगर इसके संयोजनों में से कम से कम एक संतोषजनक है, और एक संयोजन संतोषजनक है अगर और केवल अगर इसमें कुछ चर '' के लिए '' x '' और ना ही '' x '' दोनों शामिल नहीं हैं। x'' इसे रैखिक समय में चेक किया जा सकता है। इसके अलावा, यदि वे पूर्ण वियोगात्मक सामान्य रूप में होने के लिए प्रतिबंधित हैं, जिसमें प्रत्येक चर प्रत्येक संयुग्मन में ठीक एक बार दिखाई देता है, तो उन्हें निरंतर समय में चेक किया जा सकता है (प्रत्येक संयुग्मन एक संतोषजनक समनुदेशन का प्रतिनिधित्व करता है)। लेकिन सामान्य सैट समस्या को अलग करने वाले सामान्य रूप में परिवर्तित करने में घातीय समय और स्थान लग सकता है; उदाहरण के लिए संयोजन सामान्य रूपों के लिए #परिभाषा घातीय झटका उदाहरण में ∧ और ∨ का आदान-प्रदान करें।
 ===बिल्कुल-1 3-संतोषजनकता===
-[[File:Schaefer's 3-SAT to 1-in-3-SAT reduction.gif|thumb|x100px|बायाँ: शेफ़र द्वारा 3-SAT क्लॉज़ ''x'' ∨ ''y'' ∨ ''z'' की कमी। 'र' का परिणाम है {{fontcolor|#00a000|TRUE (1)}} यदि इसका एक तर्क सही है, और {{fontcolor|#a00000|FALSE (0)}} अन्यथा। x,y,z के मानों के सभी 8 संयोजनों की जांच की जाती है, प्रति पंक्ति एक। ताजा चर a,...,f सभी खंडों को संतुष्ट करने के लिए चुना जा सकता है (बिल्कुल एक {{fontcolor|#00a000|green}} प्रत्येक R के लिए तर्क) पहली पंक्ति को छोड़कर सभी पंक्तियों में, जहाँ x ∨ y ∨ z FALSE है। 'दाहिना:' समान गुणों वाला एक सरल अपचयन।]]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|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-सैट के रूप में भी जाना जाता है)।
-तीन शाब्दिक प्रति खंड के साथ एक सामान्य सामान्य रूप को देखते हुए, समस्या यह निर्धारित करने के लिए है कि क्या चर के लिए एक सत्य असाइनमेंट मौजूद है, ताकि प्रत्येक खंड में '' बिल्कुल '' एक TRUE शाब्दिक (और इस प्रकार बिल्कुल दो FALSE शाब्दिक) हो। इसके विपरीत, साधारण 3-SAT के लिए आवश्यक है कि प्रत्येक खंड में ''कम से कम'' एक TRUE शाब्दिक हो।
+तीन शाब्दिक प्रति खंड के साथ एक सामान्य रूप को देखते हुए, समस्या यह निर्धारित करने के लिए है कि क्या चर के लिए एक सत्य समनुदेशन मौजूद है, ताकि प्रत्येक खंड में ''बिल्कुल '' एक ट्रू शाब्दिक (और इस प्रकार बिल्कुल दो फॉल्स शाब्दिक) हो। इसके विपरीत, साधारण 3-सैट के लिए आवश्यक है कि प्रत्येक खंड में ''कम से कम''  एक ट्रू शाब्दिक हो।
-औपचारिक रूप से, एक-में-तीन 3-एसएटी समस्या को एक सामान्यीकृत संयोजक सामान्य रूप के रूप में दिया जाता है जिसमें सभी सामान्यीकृत खंडों के साथ एक टर्नरी ऑपरेटर 'आर' का उपयोग किया जाता है जो सही है, अगर इसका कोई तर्क है। जब एक-इन-थ्री 3-सैट सूत्र के सभी शाब्दिक धनात्मक होते हैं, तो संतुष्टि समस्या को एक-इन-थ्री सकारात्मक 3-सैट कहा जाता है।
+औपचारिक रूप से, एक-में-तीन 3-सैट समस्या को एक सामान्यीकृत संयोजक सामान्य रूप के रूप में दिया जाता है जिसमें सभी सामान्यीकृत खंडों के साथ एक  त्रिआधारी ऑपरेटर 'आर' का उपयोग किया जाता है जो सही है, अगर इसका कोई तर्क है। जब एक-इन-थ्री 3-सैट सूत्र के सभी शाब्दिक धनात्मक होते हैं, तो संतुष्टि समस्या को एक-इन-थ्री सकारात्मक 3-सैट कहा जाता है।
-एक-इन-थ्री 3-एसएटी, इसके सकारात्मक मामले के साथ, मानक संदर्भ में एनपी-पूर्ण समस्या LO4 के रूप में सूचीबद्ध है, ''कंप्यूटर और इंट्रेक्टेबिलिटी: ए गाइड टू द थ्योरी ऑफ एनपी-पूर्णता''
+एक-इन-थ्री 3-सैट, इसके सकारात्मक मामले के साथ, मानक संदर्भ में एनपी-पूर्ण समस्या "LO4" के रूप में सूचीबद्ध है, ''संगणक और अव्यावहारिकता: ए गाइड टू द थ्योरी ऑफ एनपी-पूर्णता''
-माइकल आर. गैरी और डेविड एस. जॉनसन द्वारा। एक-में-तीन 3-सैट को [[थॉमस जेरोम शेफर]] द्वारा शेफर के द्विबीज प्रमेय के एक विशेष मामले के रूप में एनपी-पूर्ण साबित किया गया था, जो दावा करता है कि बूलियन संतुष्टि को एक निश्चित तरीके से सामान्यीकृत करने वाली कोई भी समस्या या तो कक्षा पी में है या एनपी- है। पूरा।<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) 3CNF सूत्र में एक खंड है। इस खंड का अनुकरण करने के लिए उपयोग किए जाने वाले छह नए बूलियन चर a, b, c, d, e, और f जोड़ें और कोई अन्य नहीं।
+शेफ़र 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,FALSE) द्वारा संतोषजनक है ताज़ा चरों की कुछ सेटिंग यदि और केवल यदि x, y, या z में से कम से कम एक सत्य है, चित्र देखें (बाएं)। इस प्रकार एम खंड और एन चर के साथ किसी भी 3-एसएटी उदाहरण को 5 एम खंड और एन + 6 एम चर के साथ तीन 3-एसएटी उदाहरण में एक समतुल्य में परिवर्तित किया जा सकता है।{{sfnp|Schaefer|1978|p=222, Lemma 3.5}}
+तब सूत्र 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), चित्र देखें (दाएं)।
 ===नहीं-सब-बराबर 3-संतोषजनक===
-{{main|Not-all-equal 3-satisfiability}}
+{{main|नहीं-सब-बराबर 3-संतोषजनक}}
-एक अन्य संस्करण नॉट-ऑल-इक्वल 3-संतोषजनक समस्या है (जिसे NAE3SAT भी कहा जाता है)।
-तीन शाब्दिक प्रति खंड के साथ एक संयोजन सामान्य रूप दिया गया है, समस्या यह निर्धारित करने के लिए है कि क्या चर के लिए एक असाइनमेंट मौजूद है जैसे कि किसी भी खंड में सभी तीन शाब्दिक समान सत्य मूल्य नहीं हैं। यह समस्या एनपी-पूर्ण है, भले ही शेफर के द्विबीजपत्री प्रमेय द्वारा कोई निषेध प्रतीक स्वीकार न किया गया हो।<ref name="schaefer"/>
+एक अन्य संस्करण नहीं-सब-बराबर 3-संतोषजनक समस्या है (जिसे एनएई 3सैट भी कहा जाता है)।
+तीन शाब्दिक प्रति खंड के साथ एक संयोजन सामान्य रूप दिया गया है, समस्या यह निर्धारित करने के लिए है कि क्या चर के लिए एक समनुदेशन मौजूद है जैसे कि किसी भी खंड में सभी तीन शाब्दिक समान सत्य मूल्य नहीं हैं। यह समस्या एनपी-पूर्ण है, भले ही शेफर के द्विबीजपत्री प्रमेय द्वारा कोई निषेध प्रतीक स्वीकार न किया गया हो।<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>
 ===2-संतुष्टि ===
-{{Main|2-satisfiability}}
+{{Main|2-संतुष्टि}}
-एसएटी आसान है अगर एक खंड में अक्षर की संख्या अधिकतम 2 तक सीमित है, इस मामले में समस्या को 2-एसएटी कहा जाता है। इस समस्या को बहुपद समय में हल किया जा सकता है, और वास्तव में जटिलता वर्ग एन[[एल (जटिलता)]] के लिए [[एनएल-पूर्ण]] है। यदि अतिरिक्त रूप से शाब्दिक रूप से सभी या संचालन को अनन्य या संचालन में बदल दिया जाता है, तो परिणाम को अनन्य-या 2-संतोषजनकता कहा जाता है, जो कि जटिलता वर्ग SL (जटिलता) = L (जटिलता) के लिए पूर्ण समस्या है।
+सैट आसान है अगर एक खंड में अक्षर की संख्या अधिकतम 2 तक सीमित है, इस मामले में समस्या को 2-सैट कहा जाता है। इस समस्या को बहुपद समय में हल किया जा सकता है, और वास्तव में जटिलता वर्ग एन[[एल (जटिलता)]] के लिए [[एनएल-पूर्ण]] है। यदि अतिरिक्त रूप से शाब्दिक रूप से सभी या संचालन को अनन्य या संचालन में बदल दिया जाता है, तो परिणाम को अनन्य-या 2-संतोषजनकता कहा जाता है, जो कि जटिलता वर्ग एसएल (जटिलता) = एल (जटिलता) के लिए पूर्ण समस्या है।
 === हॉर्न-संतुष्टि ===
-{{Main|Horn-satisfiability}}
+{{Main|हॉर्न-संतुष्टि}}
-हॉर्न क्लॉज के दिए गए संयोजन की संतुष्टि की समस्या को हॉर्न-संतोषजनकता या हॉर्न-सैट कहा जाता है।
-इसे बहुपद समय में यूनिट प्रसार एल्गोरिथ्म के एक चरण द्वारा हल किया जा सकता है, जो हॉर्न क्लॉज के सेट के एकल न्यूनतम मॉडल का उत्पादन करता है (w.r.t. TRUE को निर्दिष्ट शाब्दिक सेट)।
+हॉर्न खंड के दिए गए संयोजन की संतुष्टि की समस्या को हॉर्न-संतोषजनकता या हॉर्न-सैट कहा जाता है।
-हॉर्न-संतोषजनकता [[पी-पूर्ण]] है। इसे पी (जटिलता) के रूप में देखा जा सकता है। बूलियन संतुष्टि समस्या के पी संस्करण।
+इसे बहुपद समय में यूनिट प्रसार कलनविधि के एक चरण द्वारा हल किया जा सकता है, जो हॉर्न खंड के सेट के एकल न्यूनतम मॉडल का उत्पादन करता है डब्ल्यू.आर.टी. ट्रू को निर्दिष्ट शाब्दिक सेट)।
-इसके अलावा, बहुपद समय में परिमाणित हॉर्न फ़ार्मुलों की सच्चाई का निर्धारण किया जा सकता है।
+हॉर्न-संतोषजनकता [[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> ∧ ... ∧ एक्स<sub>''n''</sub> → वाई, यानी, अगर एक्स<sub>1</sub>,...,एक्स<sub>''n''</sub> सभी TRUE हैं, तो y को भी TRUE होना चाहिए।
+हॉर्न खण्ड़ दिलचस्प हैं क्योंकि वे अन्य चरों के एक सेट से एक चर की प्रविष्टि को व्यक्त करने में सक्षम हैं। दरअसल, ऐसा ही एक खंड ¬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 को भी ट्रू होना चाहिए।
-हॉर्न फ़ार्मुलों की श्रेणी का एक सामान्यीकरण नाम बदलने योग्य-हॉर्न फ़ार्मुलों का है, जो कि उन फ़ार्मुलों का सेट है जिन्हें कुछ चरों को उनके संबंधित नकार के साथ बदलकर हॉर्न रूप में रखा जा सकता है।
+हॉर्न सूत्र की श्रेणी का एक सामान्यीकरण नाम बदलने योग्य-हॉर्न सूत्र का है, जो कि उन सूत्र का सेट है जिन्हें कुछ चरों को उनके संबंधित नकार के साथ बदलकर हॉर्न रूप में रखा जा सकता है।
-उदाहरण के लिए, (एक्स<sub>1</sub> ∨ ¬x<sub>2</sub>) ∧ (¬x<sub>1</sub> ∨ एक्स<sub>2</sub> ∨ एक्स<sub>3</sub>) ∧ ¬x<sub>1</sub> हॉर्न फॉर्मूला नहीं है, लेकिन इसका नाम बदलकर हॉर्न फॉर्मूला (x<sub>1</sub> ∨ ¬x<sub>2</sub>) ∧ (¬x<sub>1</sub> ∨ एक्स<sub>2</sub> ∨ ¬y<sub>3</sub>) ∧ ¬x<sub>1</sub> वाई पेश करके<sub>3</sub> एक्स की अस्वीकृति के रूप में<sub>3</sub>.
+उदाहरण के लिए, (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> ∨ ¬x<sub>2</sub>) ∧ (¬x<sub>1</sub> ∨ x<sub>2</sub> ∨ ¬y<sub>3</sub>) ∧ ¬x<sub>1</sub> y पेश करके<sub>3</sub> x की अस्वीकृति के रूप में<sub>3</sub>.
-इसके विपरीत, (x<sub>1</sub> ∨ ¬x<sub>2</sub> ∨ ¬x<sub>3</sub>) ∧ (¬x<sub>1</sub> ∨ एक्स<sub>2</sub> ∨ एक्स<sub>3</sub>) ∧ ¬x<sub>1</sub> एक हॉर्न सूत्र की ओर जाता है।
+इसके विपरीत, (x<sub>1</sub> ∨ ¬x<sub>2</sub> ∨ ¬x<sub>3</sub>) ∧ (¬x<sub>1</sub> ∨ x<sub>2</sub> ∨ x<sub>3</sub>) ∧ ¬x<sub>1</sub> एक हॉर्न सूत्र की ओर जाता है।
 ऐसे प्रतिस्थापन के अस्तित्व की जाँच रैखिक समय में की जा सकती है; इसलिए, ऐसे सूत्रों की संतुष्टि P में है क्योंकि पहले इस प्रतिस्थापन को करके और फिर परिणामी हॉर्न सूत्र की संतुष्टि की जाँच करके इसे हल किया जा सकता है।
 {| style="float:right"
-| [[File:Boolean satisfiability vs true literal counts.png|thumb|x200px|A formula with 2 clauses may be unsatisfied (red), 3-satisfied (green), xor-3-satisfied (blue), or/and 1-in-3-satisfied (yellow), depending on the TRUE-literal count in the 1st (hor) and 2nd (vert) clause.]]
+|
 |}
-===XOR-संतुष्टि ===
+===एक्सओआर-संतुष्टि ===
 {| align="right" class="wikitable collapsible collapsed" style="text-align:left; margin: 1em"
 |-
-! Solving an XOR-SAT example<BR>by [[Gaussian elimination]]
+! Solving an XOR-सैट example<BR>by [[Gaussian elimination]]
 |-
 |
@@ Line 145: / Line 148: @@
 ! colspan="9" | Equation system
 |-
-| colspan="9" | ("1" means TRUE, "0" means FALSE)
+| colspan="9" | ("1" means ट्रू, "0" means फॉल्स)
 |-
 | colspan="9" | Each clause leads to one equation.
@@ Line 332: / Line 335: @@
 | If the {{color|#ff8080|red clause}} is present: || Unsolvable
 |-
-| Else: || ''a'' = 0 = FALSE
+| Else: || ''a'' = 0 = फॉल्स
 |-
-| || ''b'' = 1 = TRUE
+| || ''b'' = 1 = ट्रू
 |-
-| || ''c'' = 0 = FALSE
+| || ''c'' = 0 = फॉल्स
 |-
-| || ''d'' = 1 = TRUE
+| || ''d'' = 1 = ट्रू
 |-
 | colspan="2" | '''As a consequence:'''
@@ Line 344: / Line 347: @@
 | colspan="2" | ''R''(''a'',''c'',''d'') ∧ ''R''(''b'',¬''c'',''d'') ∧ ''R''(''a'',''b'',¬''d'') ∧ ''R''(''a'',¬''b'',¬''c'') {{color|#ff8080|∧ ''R''(¬''a'',''b'',''c'')}}
 |-
-| colspan="2" | is not 1-in-3-satisfiable,
+| colspan="2" | is not 1-in-3-सैटisfiable,
 |-
 | colspan="2" | while (''a'' ∨ ''c'' ∨ ''d'') ∧ (''b'' ∨ ¬''c'' ∨ ''d'') ∧ (''a'' ∨ ''b'' ∨ ¬''d'') ∧ (''a'' ∨ ¬''b'' ∨ ¬''c'')
 |-
-| colspan="2" |  is 3-satisfiable with ''a''=''c''=FALSE and ''b''=''d''=TRUE.
+| colspan="2" |  is 3-सैटisfiable with ''a''=''c''=फॉल्स and ''b''=''d''=ट्रू.
 |}
 |}
 एक और विशेष मामला समस्याओं का वर्ग है जहां प्रत्येक खंड में (सादे) या ऑपरेटरों के बजाय एक्सओआर (यानी अनन्य या) होता है।<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>
-यह [[पी (जटिलता वर्ग)]] में है, चूंकि एक्सओआर-एसएटी सूत्र को रैखिक समीकरण मॉड 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> उदाहरण के लिए बॉक्स देखें। यह पुनर्रचना बूलियन बीजगणित (संरचना)#बूलियन रिंग्स पर आधारित है, और यह तथ्य कि अंकगणितीय मोडुलो दो एक [[परिमित क्षेत्र]] बनाते हैं। चूँकि एक XOR b XOR c TRUE का मूल्यांकन करता है यदि और केवल यदि {a,b,c} के ठीक 1 या 3 सदस्य TRUE हैं, तो किसी दिए गए CNF सूत्र के लिए 1-इन-3-SAT समस्या का प्रत्येक समाधान भी एक समाधान है XOR-3-SAT समस्या का, और बदले में XOR-3-SAT का प्रत्येक समाधान 3-SAT, cf का समाधान है। चित्र। परिणामस्वरूप, प्रत्येक CNF सूत्र के लिए, सूत्र द्वारा परिभाषित XOR-3-SAT समस्या को हल करना संभव है, और परिणाम के आधार पर अनुमान लगाया जाता है कि 3-SAT समस्या हल करने योग्य है या 1-में-3- एसएटी समस्या हल करने योग्य नहीं है।
+यह [[पी (जटिलता वर्ग)]] में है, चूंकि एक्सओआर-सैट सूत्र को रैखिक समीकरण मॉड 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> उदाहरण के लिए बॉक्स देखें। यह पुनर्रचना बूलियन बीजगणित (संरचना)#बूलियन रिंग्स पर आधारित है, और यह तथ्य कि अंकगणितीय मोडुलो दो एक [[परिमित क्षेत्र]] बनाते हैं। चूँकि एक XOR b XOR c ट्रू का मूल्यांकन करता है यदि और केवल यदि {a,b,c} के ठीक 1 या 3 सदस्य ट्रू हैं, तो किसी दिए गए सीएनएफ सूत्र के लिए 1-इन-3-सैट समस्या का प्रत्येक समाधान भी एक समाधान है XOR-3-सैट समस्या का, और बदले में XOR-3-सैट का प्रत्येक समाधान 3-सैट, cf का समाधान है। चित्र। परिणामस्वरूप, प्रत्येक सीएनएफ सूत्र के लिए, सूत्र द्वारा परिभाषित XOR-3-सैट समस्या को हल करना संभव है, और परिणाम के आधार पर अनुमान लगाया जाता है कि 3-सैट समस्या हल करने योग्य है या 1-में-3- सैट समस्या हल करने योग्य नहीं है।
 बशर्ते कि पी = एनपी समस्या, न तो 2-, न ही हॉर्न-, न ही एक्सओआर-संतुष्टि, सैट के विपरीत एनपी-पूर्ण है।
@@ Line 359: / Line 362: @@
 === शेफर का द्विभाजन प्रमेय ===
 {{Main|Schaefer's dichotomy theorem}}
-उपरोक्त प्रतिबंध (सीएनएफ, 2सीएनएफ, 3सीएनएफ, हॉर्न, एक्सओआर-एसएटी) विचार किए गए सूत्रों को सबफॉर्मुला के संयोजन के रूप में बाध्य करते हैं; प्रत्येक प्रतिबंध सभी उपसूत्रों के लिए एक विशिष्ट रूप बताता है: उदाहरण के लिए, केवल द्विआधारी खंड 2CNF में उपसूत्र हो सकते हैं।
+उपरोक्त प्रतिबंध (सीएनएफ, 2सीएनएफ, 3सीएनएफ, हॉर्न, एक्सओआर-सैट) विचार किए गए सूत्रों को सबफॉर्मुला के संयोजन के रूप में बाध्य करते हैं; प्रत्येक प्रतिबंध सभी उपसूत्रों के लिए एक विशिष्ट रूप बताता है: उदाहरण के लिए, केवल द्विआधारी खंड 2सीएनएफ में उपसूत्र हो सकते हैं।
-शेफर के द्विभाजन प्रमेय में कहा गया है कि, बूलियन कार्यों के लिए किसी भी प्रतिबंध के लिए जिसका उपयोग इन उपसूत्रों को बनाने के लिए किया जा सकता है, संबंधित संतुष्टि समस्या पी या एनपी-पूर्ण में है। 2CNF, हॉर्न, और XOR-SAT सूत्रों की संतुष्टि की P में सदस्यता इस प्रमेय के विशेष मामले हैं।<ref name="schaefer"/>
+शेफर के द्विभाजन प्रमेय में कहा गया है कि, बूलियन कार्यों के लिए किसी भी प्रतिबंध के लिए जिसका उपयोग इन उपसूत्रों को बनाने के लिए किया जा सकता है, संबंधित संतुष्टि समस्या पी या एनपी-पूर्ण में है। 2सीएनएफ, हॉर्न, और XOR-सैट सूत्रों की संतुष्टि की P में सदस्यता इस प्रमेय के विशेष मामले हैं।<ref name="schaefer"/>
-निम्न तालिका एसएटी के कुछ सामान्य रूपों का सारांश देती है।
+निम्न तालिका सैट के कुछ सामान्य रूपों का सारांश देती है।
 {| class="wikitable sortable"
 |+
@@ Line 372: / Line 375: @@
 !Class
 |-
-|3SAT
+|3सैट
-|3-satisfiability
+|3-सैटisfiability
 |Each clause contains 3 literals.
-|At least one literal must be true.
+|At least one literal must be ट्रू.
 |NPC
 |-
-|2SAT
+|2सैट
-|2-satisfiability
+|2-सैटisfiability
 |Each clause contains 2 literals.
-|At least one literal must be true.
+|At least one literal must be ट्रू.
 |P
 |-
-|1-in-3-SAT
+|1-in-3-सैट
-|Exactly-1 3-SAT
+|Exactly-1 3-सैट
 |Each clause contains 3 literals.
-|Exactly one literal must be true.
+|Exactly one literal must be ट्रू.
 |NPC
 |-
-|1-in-3-SAT+
+|1-in-3-सैट+
-|Exactly-1 Positive 3-SAT
+|Exactly-1 Positive 3-सैट
 |Each clause contains 3 positive literals.
-|Exactly one literal must be true.
+|Exactly one literal must be ट्रू.
 |NPC
 |-
-|NAE3SAT
+|NAE3सैट
-|Not-all-equal 3-satisfiability
+|Not-all-equal 3-सैटisfiability
 |Each clause contains 3 literals.
-|Either one or two literals must be true.
+|Either one or two literals must be ट्रू.
 |NPC
 |-
-|NAE3SAT+
+|NAE3सैट+
-|Not-all-equal positive 3-SAT
+|Not-all-equal positive 3-सैट
 |Each clause contains 3 positive literals.
-|Either one or two literals must be true.
+|Either one or two literals must be ट्रू.
 |NPC
 |-
-|PL-SAT
+|PL-सैट
-|[[Planar SAT]]
+|[[Planar SAT|Planar सैट]]
 |The incidence graph (clause-variable graph) is [[Planar graph|planar]].
-|At least one literal must be true.
+|At least one literal must be ट्रू.
 |NPC
 |-
-|LSAT
+|Lसैट
-|Linear SAT
+|Linear सैट
 |Each clause contains 3 literals, intersects at most one other clause, and the intersection is exactly one literal.
-|At least one literal must be true.
+|At least one literal must be ट्रू.
 |NPC
 |-
-|HORN-SAT
+|HORN-सैट
-|Horn satisfiability
+|Horn सैटisfiability
 |Horn clauses (at most one positive literal).
-|At least one literal must be true.
+|At least one literal must be ट्रू.
 |P
 |-
-|XOR-SAT
+|XOR-सैट
-|Xor satisfiability
+|Xor सैटisfiability
 |Each clause contains XOR operations rather than OR.
-|The XOR of all literals must be true.
+|The XOR of all literals must be ट्रू.
 |P
 |}
-== एसएटी == के एक्सटेंशन
+== सैट == के एक्सटेंशन
 एक एक्सटेंशन जिसने 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=TRUE यदि x और y दोनों FALSE हैं, और z=FALSE अन्य।
+ऐसी अभिव्यक्ति का एक उदाहरण होगा {{math|size=100%|∀''x'' ∀''y'' ∃''z'' (''x'' ∨ ''y'' ∨ ''z'') ∧ (¬''x'' ∨ ¬''y'' ∨ ¬''z'')}}; यह मान्य है, क्योंकि x और y के सभी मानों के लिए, z का एक उपयुक्त मान पाया जा सकता है, अर्थात। z=ट्रू यदि x और y दोनों फॉल्स हैं, और z=फॉल्स अन्य।
-SAT स्वयं (मौन रूप से) केवल ∃ क्वांटिफायर का उपयोग करता है।
+सैट स्वयं (मौन रूप से) केवल ∃ क्वांटिफायर का उपयोग करता है।
 यदि इसके बजाय केवल ∀ क्वांटिफायर की अनुमति है, तथाकथित '[[टॉटोलॉजी (तर्क)]] समस्या' प्राप्त की जाती है, जो [[सह-एनपी-पूर्ण]] है।
-यदि दोनों परिमाणकों की अनुमति है, तो समस्या को 'मात्राबद्ध बूलियन सूत्र समस्या' ('क्यूबीएफ') कहा जाता है, जिसे पीएसपीएसीई-पूर्ण दिखाया जा सकता है। यह व्यापक रूप से माना जाता है कि एनपी में किसी भी समस्या की तुलना में पीएसपीएसीई-पूर्ण समस्याएं सख्ती से कठिन हैं, हालांकि यह अभी तक सिद्ध नहीं हुआ है। अत्यधिक समानांतर [[पी प्रणाली]] का उपयोग करके, QBF-SAT समस्याओं को रैखिक समय में हल किया जा सकता है।<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>
+यदि दोनों परिमाणकों की अनुमति है, तो समस्या को 'मात्राबद्ध बूलियन सूत्र समस्या' ('क्यूबीएफ') कहा जाता है, जिसे पीएसपीएसीई-पूर्ण दिखाया जा सकता है। यह व्यापक रूप से माना जाता है कि एनपी में किसी भी समस्या की तुलना में पीएसपीएसीई-पूर्ण समस्याएं सख्ती से कठिन हैं, हालांकि यह अभी तक सिद्ध नहीं हुआ है। अत्यधिक समानांतर [[पी प्रणाली]] का उपयोग करके, QBF-सैट समस्याओं को रैखिक समय में हल किया जा सकता है।<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>
-सामान्य एसएटी पूछता है कि क्या कम से कम एक परिवर्तनीय असाइनमेंट है जो सूत्र को सत्य बनाता है। विभिन्न प्रकार के वेरिएंट ऐसे असाइनमेंट की संख्या से निपटते हैं:
+सामान्य सैट पूछता है कि क्या कम से कम एक परिवर्तनीय समनुदेशन है जो सूत्र को सत्य बनाता है। विभिन्न प्रकार के वेरिएंट ऐसे समनुदेशन की संख्या से निपटते हैं:
-* MAJ-SAT पूछता है कि क्या सभी असाइनमेंट्स में से अधिकांश सूत्र को TRUE बनाते हैं। यह [[पीपी (जटिलता)]] के लिए पूर्ण माना जाता है, एक संभाव्य वर्ग।
+* MAJ-सैट पूछता है कि क्या सभी समनुदेशन्स में से अधिकांश सूत्र को ट्रू बनाते हैं। यह [[पीपी (जटिलता)]] के लिए पूर्ण माना जाता है, एक संभाव्य वर्ग।
-* Sharp-SAT|#SAT, गिनती की समस्या कि कितने चर असाइनमेंट एक सूत्र को संतुष्ट करते हैं, एक गिनती की समस्या है, निर्णय की समस्या नहीं है, और Sharp-P-पूर्ण|#P-पूर्ण है।
+* Sharp-सैट|#सैट, गिनती की समस्या कि कितने चर समनुदेशन एक सूत्र को संतुष्ट करते हैं, एक गिनती की समस्या है, निर्णय की समस्या नहीं है, और Sharp-P-पूर्ण|#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> एक गैर-नियतात्मक बहुपद समय [[ट्यूरिंग मशीन]] द्वारा हल की जा सकने वाली समस्याओं का वर्णन करने वाली जटिलता वर्ग, जो तब स्वीकार करती है जब वास्तव में एक गैर-नियतात्मक स्वीकार्य पथ होता है और अन्यथा अस्वीकार करता है।
-*UNAMBIGUOUS-SAT वह नाम है जो संतुष्टि समस्या को दिया जाता है जब इनपुट अधिकतम एक संतोषजनक असाइनमेंट वाले फ़ार्मुलों के लिए प्रॉमिस प्रॉब्लम होता है। समस्या को यूएसएटी भी कहा जाता है।<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> UNAMBIGUOUS-SAT के लिए एक सॉल्विंग एल्गोरिदम को कई संतोषजनक असाइनमेंट वाले फॉर्मूले पर अंतहीन लूपिंग सहित किसी भी व्यवहार को प्रदर्शित करने की अनुमति है। हालाँकि यह समस्या आसान लगती है, वैलेंट और वज़ीरानी के पास वैलेंट-वज़ीरानी प्रमेय है<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> कि अगर इसे हल करने के लिए एक व्यावहारिक (यानी [[परिबद्ध-त्रुटि संभाव्य बहुपद]] | रैंडमाइज्ड पॉलीनोमियल-टाइम) एल्गोरिदम है, तो [[एनपी (जटिलता वर्ग)]] में सभी समस्याओं को आसानी से हल किया जा सकता है।
+*UNAMBIGUOUS-सैट वह नाम है जो संतुष्टि समस्या को दिया जाता है जब इनपुट अधिकतम एक संतोषजनक समनुदेशन वाले सूत्र के लिए प्रॉमिस प्रॉब्लम होता है। समस्या को यूसैट भी कहा जाता है।<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> UNAMBIGUOUS-सैट के लिए एक सॉल्विंग कलनविधि को कई संतोषजनक समनुदेशन वाले फॉर्मूले पर अंतहीन लूपिंग सहित किसी भी व्यवहार को प्रदर्शित करने की अनुमति है। हालाँकि यह समस्या आसान लगती है, वैलेंट और वज़ीरानी के पास वैलेंट-वज़ीरानी प्रमेय है<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> कि अगर इसे हल करने के लिए एक व्यावहारिक (यानी [[परिबद्ध-त्रुटि संभाव्य बहुपद]] | रैंडमाइज्ड पॉलीनोमियल-टाइम) कलनविधि है, तो [[एनपी (जटिलता वर्ग)]] में सभी समस्याओं को आसानी से हल किया जा सकता है।
-* MAX-SAT, [[अधिकतम संतुष्टि की समस्या]], SAT का FNP (जटिलता) सामान्यीकरण है। यह अधिकतम संख्या में खंडों के लिए पूछता है जो किसी भी असाइनमेंट से संतुष्ट हो सकते हैं। इसमें कुशल सन्निकटन एल्गोरिदम हैं, लेकिन एनपी-कठिन को ठीक से हल करना है। इससे भी बदतर, यह [[एपीएक्स]]-पूर्ण है, जिसका अर्थ है कि इस समस्या के लिए कोई [[बहुपद-समय सन्निकटन योजना]] (पीटीएएस) नहीं है जब तक कि पी = एनपी न हो।
+* MAX-सैट, [[अधिकतम संतुष्टि की समस्या]], सैट का FNP (जटिलता) सामान्यीकरण है। यह अधिकतम संख्या में खंडों के लिए पूछता है जो किसी भी समनुदेशन से संतुष्ट हो सकते हैं। इसमें कुशल सन्निकटन कलनविधि हैं, लेकिन एनपी-कठिन को ठीक से हल करना है। इससे भी बदतर, यह [[एपीएक्स]]-पूर्ण है, जिसका अर्थ है कि इस समस्या के लिए कोई [[बहुपद-समय सन्निकटन योजना]] (पीटीएएस) नहीं है जब तक कि पी = एनपी न हो।
-*WMSAT न्यूनतम वजन का एक असाइनमेंट खोजने की समस्या है जो एक मोनोटोन बूलियन फॉर्मूला (यानी बिना किसी निषेध के एक फॉर्मूला) को संतुष्ट करता है। समस्या के इनपुट में प्रस्तावात्मक चर के भार दिए गए हैं। असाइनमेंट का वजन सही चर के वजन का योग है। वह समस्या एनपी-पूर्ण है (थ देखें। 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>).
+*WMसैट न्यूनतम वजन का एक समनुदेशन खोजने की समस्या है जो एक मोनोटोन बूलियन सूत्र (यानी बिना किसी निषेध के एक सूत्र) को संतुष्ट करता है। समस्या के इनपुट में प्रस्तावात्मक चर के भार दिए गए हैं। समनुदेशन का वजन सही चर के वजन का योग है। वह समस्या एनपी-पूर्ण है (थ देखें। 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 पूर्णांक प्रोग्रामिंग]] के लिए संतुष्टि शामिल है।
-== एक संतोषजनक असाइनमेंट ढूँढना ==
+== एक संतोषजनक समनुदेशन ढूँढना ==
-जबकि SAT एक निर्णय समस्या है, संतोषजनक असाइनमेंट खोजने की [[खोज समस्या]] SAT तक कम हो जाती है। अर्थात्, प्रत्येक एल्गोरिथम जो सही ढंग से उत्तर देता है कि क्या एसएटी का एक उदाहरण हल करने योग्य है, एक संतोषजनक असाइनमेंट खोजने के लिए इस्तेमाल किया जा सकता है। सबसे पहले दिए गए सूत्र Φ पर प्रश्न पूछा जाता है। यदि उत्तर नहीं है, तो सूत्र संतोषजनक नहीं है। अन्यथा, प्रश्न आंशिक रूप से तत्काल सूत्र Φप्रतिस्थापन (तर्क) पर पूछा जाता है|{x<sub>1</sub>=TRUE}, यानी Φ पहले चर x के साथ<sub>1</sub> TRUE द्वारा प्रतिस्थापित किया गया, और तदनुसार सरलीकृत किया गया। यदि उत्तर हाँ है, तो x<sub>1</sub>= TRUE, अन्यथा 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 461: / Line 465: @@
 : पी (जटिलता) = एनपी (जटिलता) ⇒ [[एफपी (जटिलता)]] = एफएनपी (जटिलता)
-== एसएटी == को हल करने के लिए एल्गोरिदम
+== सैट == को हल करने के लिए कलनविधि
 {{main|SAT solver}}
-चूंकि एसएटी समस्या एनपी-पूर्ण है, केवल घातीय सबसे खराब स्थिति वाले एल्गोरिदम इसके लिए जाने जाते हैं। इसके बावजूद, एसएटी के लिए कुशल और स्केलेबल एल्गोरिदम 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> [[इलेक्ट्रॉनिक डिजाइन स्वचालन]] (EDA) में ऐसी समस्याओं के उदाहरणों में [[औपचारिक तुल्यता जाँच]], मॉडल जाँच, [[माइक्रोप्रोसेसर]] का [[औपचारिक सत्यापन]],<ref name="Bryant.German.Velev.1999"/>स्वत: परीक्षण पैटर्न पीढ़ी, [[एफपीजीए]] की [[रूटिंग (इलेक्ट्रॉनिक डिजाइन स्वचालन)]],<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> [[स्वचालित योजना और शेड्यूलिंग]], और [[शेड्यूलिंग एल्गोरिदम]], और इसी तरह। इलेक्ट्रॉनिक डिज़ाइन ऑटोमेशन टूलबॉक्स में एक SAT-सॉल्विंग इंजन को भी एक आवश्यक घटक माना जाता है।
+चूंकि सैट समस्या एनपी-पूर्ण है, केवल घातीय सबसे खराब स्थिति वाले कलनविधि इसके लिए जाने जाते हैं। इसके बावजूद, सैट के लिए कुशल और स्केलेबल कलनविधि 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> [[इलेक्ट्रॉनिक डिजाइन स्वचालन]] (EDA) में ऐसी समस्याओं के उदाहरणों में [[औपचारिक तुल्यता जाँच]], मॉडल जाँच, [[माइक्रोप्रोसेसर]] का [[औपचारिक सत्यापन]],<ref name="Bryant.German.Velev.1999"/>स्वत: परीक्षण पैटर्न पीढ़ी, [[एफपीजीए]] की [[रूटिंग (इलेक्ट्रॉनिक डिजाइन स्वचालन)]],<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> [[स्वचालित योजना और शेड्यूलिंग]], और [[शेड्यूलिंग एल्गोरिदम|शेड्यूलिंग कलनविधि]], और इसी तरह। इलेक्ट्रॉनिक डिज़ाइन ऑटोमेशन टूलबॉक्स में एक सैट-सॉल्विंग इंजन को भी एक आवश्यक घटक माना जाता है।
-आधुनिक एसएटी सॉल्वरों द्वारा उपयोग की जाने वाली प्रमुख तकनीकों में डेविस-पुटनम-लॉगमैन-लवलैंड एल्गोरिथम (या डीपीएलएल), [[संघर्ष-संचालित क्लॉज लर्निंग]] (सीडीसीएल), और [[वॉकसैट]] जैसे [[स्टोकेस्टिक]] लोकल सर्च (कंस्ट्रेंट संतुष्टि) एल्गोरिदम शामिल हैं। लगभग सभी एसएटी सॉल्वरों में टाइम-आउट शामिल है, इसलिए वे उचित समय में समाप्त हो जाएंगे, भले ही उन्हें समाधान नहीं मिल रहा हो।
+आधुनिक सैट सॉल्वरों द्वारा उपयोग की जाने वाली प्रमुख तकनीकों में डेविस-पुटनम-लॉगमैन-लवलैंड कलनविधि (या डीपीएलएल), [[संघर्ष-संचालित क्लॉज लर्निंग|संघर्ष-संचालित खंड लर्निंग]] (सीडीसीएल), और [[वॉकसैट]] जैसे [[स्टोकेस्टिक]] लोकल सर्च (कंस्ट्रेंट संतुष्टि) कलनविधि शामिल हैं। लगभग सभी सैट सॉल्वरों में टाइम-आउट शामिल है, इसलिए वे उचित समय में समाप्त हो जाएंगे, भले ही उन्हें समाधान नहीं मिल रहा हो।
-अलग-अलग एसएटी सॉल्वर अलग-अलग उदाहरणों को आसान या कठिन पाएंगे, और कुछ असंतोष साबित करने में उत्कृष्ट होंगे, और अन्य समाधान खोजने में। गहन शिक्षण तकनीकों का उपयोग करके एक उदाहरण की संतुष्टि को जानने के लिए हाल ही में प्रयास किए गए हैं।<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>
-SAT सॉल्वर विकसित किए जाते हैं और SAT-सॉल्विंग प्रतियोगिताओं में उनकी तुलना की जाती है।<ref>{{cite web|url=http://www.satcompetition.org/ |title=The international SAT Competitions web page|access-date=2007-11-15}}</ref> आधुनिक SAT सॉल्वर का सॉफ्टवेयर सत्यापन, आर्टिफिशियल इंटेलिजेंस में बाधाओं को हल करने, और संचालन अनुसंधान सहित अन्य क्षेत्रों पर भी महत्वपूर्ण प्रभाव पड़ रहा है।
+सैट सॉल्वर विकसित किए जाते हैं और सैट-सॉल्विंग प्रतियोगिताओं में उनकी तुलना की जाती है।<ref>{{cite web|url=http://www.satcompetition.org/ |title=The international SAT Competitions web page|access-date=2007-11-15}}</ref> आधुनिक सैट सॉल्वर का सॉफ्टवेयर सत्यापन, आर्टिफिशियल इंटेलिजेंस में बाधाओं को हल करने, और संचालन अनुसंधान सहित अन्य क्षेत्रों पर भी महत्वपूर्ण प्रभाव पड़ रहा है।
 == यह भी देखें ==
@@ Line 474: / Line 478: @@
 *तीव्र-सत
 * [[प्लानर सैट]]
-* कार्लोफ-ज़्विक एल्गोरिथम
+* कार्लोफ-ज़्विक कलनविधि
 * [[सर्किट संतुष्टि]]
@@ Line 484: / Line 488: @@
 {{commons category}}
-* [http://www.cril.univ-artois.fr/~roussel/satgame/satgame.php?lang=eng SAT Game]: try solving a Boolean satisfiability problem yourself
+* [http://www.cril.univ-artois.fr/~roussel/satgame/satgame.php?lang=eng सैट Game]: try solving a Boolean सैटisfiability problem yourself
-* [http://www.satcompetition.org/ The international SAT competition website]
+* [http://www.satcompetition.org/ The international सैट competition website]
-* [http://www.satisfiability.org/ International Conference on Theory and Applications of Satisfiability Testing]
+* [http://www.satisfiability.org/ International Conference on Theory and Applications of सैटisfiability Testing]
-* [https://web.archive.org/web/20060219180520/http://jsat.ewi.tudelft.nl/ Journal on Satisfiability, Boolean Modeling and Computation]
+* [https://web.archive.org/web/20060219180520/http://jsat.ewi.tudelft.nl/ Journal on सैटisfiability, Boolean Modeling and Computation]
-* [http://www.satlive.org SAT Live, an aggregate website for research on the satisfiability problem]
+* [http://www.satlive.org सैट Live, an aggregate website for research on the सैटisfiability problem]
-* [http://www.maxsat.udl.cat/ Yearly evaluation of MaxSAT solvers]
+* [http://www.maxsat.udl.cat/ Yearly evaluation of Maxसैट solvers]

Anonymous

Search

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

Revision as of 16:53, 17 February 2023

परिभाषाएँ

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

जटिलता

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

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

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

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

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

रैखिक सैट

2-संतुष्टि

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

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

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

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

यह भी देखें

टिप्पणियाँ

बाहरी संबंध

संदर्भ

अग्रिम पठन

Navigation

Wiki tools

Page tools

Other projects

Categories