बूलियन संतुष्टि समस्या

"3SAT" redirects here. For मध्य यूरोपीय टेलीविजन नेटवर्क, see 3sat.

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

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

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

परिभाषाएँ

एक प्रस्तावपरक तर्क सूत्र, जिसे बूलियन अभिव्यक्ति भी कहा जाता है, परिवर्ती (गणित), ऑपरेटरों और (तार्किक संयोजन, जिसे ∧ द्वारा भी दर्शाया गया है), या (तार्किक विच्छेदन, ∨), नहीं (निषेध, ¬), और कोष्ठकों से बनाया गया है। एक सूत्र को संतोषजनक कहा जाता है यदि इसके चरों को उपयुक्त तार्किक मान (अर्थात ट्रू, फॉल्स) निर्दिष्ट करके इसे ट्रू बनाया जा सकता हो। बूलियन संतुष्टि समस्या (सैट) को यह जांचने के लिए एक सूत्र दिया गया है कि यह संतोषजनक है या नहीं। कंप्यूटर विज्ञान के कई क्षेत्रों में यह निर्णय समस्या केंद्रीय महत्व की है, जिसमें सैद्धांतिक कंप्यूटर विज्ञान, संगणनात्मक जटिलता सिद्धांत, कलनविधि, कूटलेखन और कृत्रिम बुद्धि।

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

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

सैट समस्या के कुछ संस्करणों के लिए, यह एक सामान्यीकृत संयोजक सामान्य रूप सूत्र, अर्थात की धारणा को परिभाषित करने के लिए उपयोगी है। मनमाने ढंग से कई सामान्यीकृत खंडों के संयोजन के रूप में, बाद वाला फॉर्म का है R(l₁,...,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₁ ∨ x₂ ∨ … ∨ x_n) ∧

(y₁ ∨ x₂ ∨ … ∨ x_n) ∧

(x₁ ∨ y₂ ∨ … ∨ x_n) ∧

(y₁ ∨ y₂ ∨ … ∨ x_n) ∧ ... ∧

(x₁ ∨ x₂ ∨ … ∨ y_n) ∧

(y₁ ∨ x₂ ∨ … ∨ y_n) ∧

(x₁ ∨ y₂ ∨ … ∨ y_n) ∧

(y₁ ∨ y₂ ∨ … ∨ y_n);

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

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

जटिलता

Main article: कुक-लेविन प्रमेय

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

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

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

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

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

अप्रतिबंधित सैट समस्या को 3-सैट तक कम करने के लिए, प्रत्येक खंड को रूपांतरित करें l₁ ∨ ⋯ ∨ l_n के संयोजन के लिए n - 2 खंड

(l₁ ∨ l₂ ∨ x₂) ∧

(¬x₂ ∨ l₃ ∨ x₃) ∧

(¬x₃ ∨ l₄ ∨ x₄) ∧ ⋯ ∧

(¬x_{n − 3} ∨ l_{n − 2} ∨ x_{n − 2}) ∧

(¬x_{n − 2} ∨ l_{n − 1} ∨ l_n)

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

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

कुछ लेखक k-सैट को 'बिल्कुल k शाब्दिक' के साथ सीएनएफ सूत्र तक सीमित रखते हैं। यह प्रत्येक खंड के रूप में एक अलग जटिलता वर्ग की ओर नहीं ले जाता है l₁ ∨ ⋯ ∨ l_j with j <k लिटरल को निर्धारित डमी चर के साथ पैडेड किया जा सकता है l₁ ∨ ⋯ ∨ l_j ∨ d_j+1 ∨ ⋯ ∨ d_k. सभी खंडों को भरने के बाद, 2^k-1 अतिरिक्त खंड केवल यह सुनिश्चित करने के लिए संलग्न किया जाता है d₁ = ⋯ = d_k=FALSE संतोषजनक कार्य मिल सकता है। चूँकि k सूत्र की लंबाई पर निर्भर नहीं करता है, इसलिए अतिरिक्त खंड लंबाई में निरंतर वृद्धि करते हैं। उसी कारण से, इससे कोई फर्क नहीं पड़ता कि ' समरूप शाब्दिक' को खंडों में अनुमति दी जाती है, जैसा कि ¬x ∨ ¬y ∨ ¬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 में है या एनपी- है। पूरा। शेफ़र 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-सैट उदाहरण में एक समतुल्य में परिवर्तित किया जा सकता है। एक और कटौती में केवल चार नए चर और तीन खंड शामिल हैं: R(¬x,a,b) ∧ R(b,y,c) ∧ R(c,d,¬z), चित्र देखें (दाएं)।

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

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

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

रैखिक सैट

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

2-संतुष्टि

Main article: 2-संतुष्टि

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

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

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

हॉर्न खंड के दिए गए संयोजन की संतुष्टि की समस्या को हॉर्न-संतोषजनकता या हॉर्न-सैट कहा जाता है। इसे बहुपद समय में यूनिट प्रसार कलनविधि के एक चरण द्वारा हल किया जा सकता है, जो हॉर्न खंड के सेट के एकल न्यूनतम मॉडल का उत्पादन करता है डब्ल्यू.आर.टी. ट्रू को निर्दिष्ट शाब्दिक सेट)। हॉर्न-संतोषजनकता P पूर्ण है। इसे P (जटिलता) के रूप में देखा जा सकता है। बूलियन संतुष्टि समस्या के P संस्करण। इसके अलावा, बहुपद समय में परिमाणित हॉर्न सूत्र की सच्चाई का निर्धारण किया जा सकता है। हॉर्न खण्ड़ दिलचस्प हैं क्योंकि वे अन्य चरों के एक सेट से एक चर की प्रविष्टि को व्यक्त करने में सक्षम हैं। दरअसल, ऐसा ही एक खंड ¬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=ट्रू.

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

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

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

Main article: Schaefer's dichotomy theorem

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

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

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

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

संतुष्टि की समस्या और अधिक कठिन हो जाती है यदि सभी के लिए (∀) और वहाँ (∃) परिमाणक (तर्क)तर्क) दोनों के लिए बूलियन चर को बाँधने की अनुमति है। ऐसी अभिव्यक्ति का एक उदाहरण होगा ∀x ∀y ∃z (x ∨ y ∨ z) ∧ (¬x ∨ ¬y ∨ ¬z); यह मान्य है, क्योंकि x और y के सभी मानों के लिए, z का एक उपयुक्त मान पाया जा सकता है, अर्थात। z=ट्रू यदि x और y दोनों फॉल्स हैं, और z=फॉल्स अन्य। सैट स्वयं (मौन रूप से) केवल ∃ क्वांटिफायर का उपयोग करता है। यदि इसके बजाय केवल ∀ क्वांटिफायर की अनुमति है, तथाकथित 'टॉटोलॉजी (तर्क) समस्या' प्राप्त की जाती है, जो सह-एनपी-पूर्ण है। यदि दोनों परिमाणकों की अनुमति है, तो समस्या को 'मात्राबद्ध बूलियन सूत्र समस्या' ('क्यूबीएफ') कहा जाता है, जिसे पीएसपीएसीई-पूर्ण दिखाया जा सकता है। यह व्यापक रूप से माना जाता है कि एनपी में किसी भी समस्या की तुलना में पीएसपीएसीई-पूर्ण समस्याएं सख्ती से कठिन हैं, हालांकि यह अभी तक सिद्ध नहीं हुआ है। अत्यधिक समानांतर पी प्रणाली का उपयोग करके, QBF-सैट समस्याओं को रैखिक समय में हल किया जा सकता है। सामान्य सैट पूछता है कि क्या कम से कम एक परिवर्तनीय समनुदेशन है जो सूत्र को सत्य बनाता है। विभिन्न प्रकार के वेरिएंट ऐसे समनुदेशन की संख्या से निपटते हैं:

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

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

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

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

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

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

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

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

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

Main article: SAT solver

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

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

यह भी देखें

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

बाहरी संबंध

• सैट 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

अग्रिम पठन

(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