संतोषप्रदता

गणितीय तर्क में, उचित रूप से निर्मित सूत्र संतोषप्रदता है यदि यह इसके चर (गणित) के मूल्यों के कुछ असाइनमेंट के अनुसार सत्य है। उदाहरण के लिए, सूत्र $x+3=y$ संतोषप्रदता है क्योंकि जब $x=3$ एवं $y=6$, एवं सूत्र $x+1=x$ पूर्णांकों पर संतुष्ट नहीं है। संतुष्टि के लिए दोहरी अवधारणा वैधता है; सूत्र मान्य है यदि इसके चर के मानों का प्रत्येक असाइनमेंट सूत्र को सत्य बनाता है। उदाहरण के लिए, $x+3=3+x$ पूर्णांक मान्य है, किन्तु $x+3=y$ क्या पूर्णांक मान्य नहीं है।

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

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

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

वैधता की संतुष्टि में कमी

नकारात्मकता के साथ क्लासिकल तर्क शास्त्र के लिए, सामान्यतः सूत्र की वैधता के प्रश्न को व्यक्त करना संभव है, क्योंकि विपक्ष के उपरोक्त वर्ग में व्यक्त अवधारणाओं के मध्य संबंधों के कारण संतुष्टि सम्मिलित है। विशेष रूप से φ मान्य है एवं यदि ¬φ असंतुष्ट है, जिसका अर्थ त्रुटिपूर्ण ¬φ संतोषप्रदता है। एवं यदि ¬φ अमान्य है।

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

क्लासिकल लॉजिक के लिए प्रस्तावित संतुष्टि

Main article: प्रस्तावित संतुष्टि

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

प्रथम क्रम के तर्क में संतुष्टि

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

प्रतिमान सिद्धांत में संतुष्टि

प्रतिमान सिद्धांत में, परमाणु सूत्र संतोषप्रदता होता है यदि संरचना (तर्क) के तत्वों का संग्रह होता है जो सूत्र को सत्य बनाता है। यदि A संरचना है, φ सूत्र है, एवं a तत्वों का संग्रह है, जो संरचना से लिया गया है, जो φ को संतुष्ट करता है, तो सामान्यतः यह लिखा जाता है कि

A ⊧ φ [a]

यदि φ का कोई मुक्त चर नहीं है, अर्थात, यदि φ परमाणु वाक्य है, एवं यह A से संतुष्ट है, तो इस प्रकार लिखा जाता है,

A ⊧ φ

इस विषय में, यह भी कहा जाता है कि A, φ के लिए प्रतिमान में φ A में सत्य है। यदि T, A द्वारा संतुष्ट परमाणु वाक्यों का संग्रह है, तो इस प्रकार लिखा जाता है,

A ⊧ T

परिमित संतुष्टि

संतुष्टि से संबंधित समस्या परिमित संतुष्टि है, जो यह निर्धारित करने का प्रश्न है कि क्या कोई सूत्र परिमित प्रतिमान को स्वीकार करता है जो इसे सत्य बनाता है। तर्क के लिए जिसमें परिमित प्रतिमान संपत्ति है, संतुष्टि एवं परिमित संतुष्टि की समस्याएं होती हैं, क्योंकि उस तर्क के सूत्र के पास प्रतिमान है यदि केवल उसके पास परिमित प्रतिमान है, तो परिमित प्रतिमान सिद्धांत के गणितीय क्षेत्र में यह प्रश्न महत्वपूर्ण है।

परिमित संतुष्टि को सामान्य रूप से युग्मित नहीं होना चाहिए। उदाहरण के लिए, निम्नलिखित वाक्यों के तार्किक संयोजन के रूप में प्राप्त प्रथम-क्रम तर्क सूत्र पर विचार करें, जहाँ $a_{0}$ एवं $a_{1}$ तार्किक स्थिरांक हैं।

• $R(a_{0},a_{1})$
• $\forall xy(R(x,y)\rightarrow \exists zR(y,z))$
• $\forall xyz(R(y,x)\wedge R(z,x)\rightarrow y=z))$
• $\forall x\neg R(x,a_{0})$

परिणामी सूत्र में अनंत प्रतिमान $R(a_{0},a_{1}),R(a_{1},a_{2}),\ldots$ है , किन्तु यह दिखाया जा सकता है कि इसका कोई परिमित प्रतिमान नहीं है (तथ्य से प्रारम्भ $R(a_{0},a_{1})$ एवं $R$ की श्रंखला का पालन कर रहा है, परमाणु सूत्र जो दूसरे स्वयंसिद्ध द्वारा उपस्थित होना चाहिए, प्रतिमान की परिमितता के लिए लूप के अस्तित्व की आवश्यकता होगी, जो तीसरे एवं चौथे स्वयं सिद्धों का उल्लंघन करेगा, चाहे वह वापस लूप हो $a_{0}$ या भिन्न तत्व को हो।

किसी दिए गए तर्क में इनपुट सूत्र के लिए संतुष्टि का निर्णय लेने का कम्प्यूटेशनल जटिलता सिद्धांत परिमित संतुष्टि का निर्णय लेने से भिन्न हो सकता है; वास्तव में, कुछ तर्क के लिए, उनमें से केवल निर्धारणीय (तर्क) है।

क्लासिकल प्रथम-क्रम तर्क के लिए, परिमित संतुष्टि गणनात्मक रूप से गणना योग्य है (कक्षा आरई (जटिलता) में) एवं ट्रैखटेनब्रॉट के प्रमेय द्वारा अनिर्णीत समस्या सूत्र की अस्वीकृति पर प्रारम्भ होती है।

संख्यात्मक बाधाएँ

Further information: संतुष्टि मॉड्यूल सिद्धांत and बाधा संतुष्टि समस्या

प्रायः गणितीय अनुकूलन के क्षेत्र में दिखाई देते हैं, जहां कोई सामान्यतः कुछ बाधाओं के अधीन उद्देश्य फंक्शन को अधिकतम करना चाहता है। चूंकि, वस्तुनिष्ठ फ़ंक्शन को त्यागकर, केवल यह निर्धारित करने का मूल विषय कि क्या बाधाएं संतोषप्रदता हैं, कुछ समायोजन में अनिर्णीत हो सकती हैं। निम्न तालिका मुख्य विषयो को सारांशित करती है।

प्रतिबंध	वास्तविक से अधिक	पूर्णांकों पर
रेखीय	पी.टाइम (रैखिक प्रोग्रामिंग देखें))	एनपी-पूर्ण (पूर्णांक प्रोग्रामिंग देखें)
बहुपद	उदा के माध्यम से निर्णय लेने योग्य बेलनाकार बीजगणितीय अपघटन	अनिर्णीत (हिल्बर्ट की दसवीं समस्या))

तालिका स्रोत: बॉकमायर एवं वीस्पफेनिंग।

रैखिक बाधाओं के लिए, निम्न तालिका द्वारा पूर्ण चित्र प्रदान किया गया है।

प्रतिबंध समाप्त	परिमेय	पूर्णांक	प्राकृतिक संख्या
रेखीय समीकरण	पी.टाइम	पीटाइम	एन पी-सम्पूर्ण
रैखिक असमानताएँ	पी.टाइम	एन पी-सम्पूर्ण	एन पी-सम्पूर्ण

तालिका स्रोत: बॉकमायर एवं वीस्पफेनिंग।

यह भी देखें

• 2-संतुष्टि
• बूलियन संतुष्टि समस्या
• सर्किट संतुष्टि
• कार्प की 21 एनपी-पूर्ण समस्याएँ
• वैधता (तर्क)
• संयमित संतोष

संदर्भ

• Boolos, George; Burgess, John; Jeffrey, Richard (2007). Computability and Logic (5th ed.). Cambridge University Press.

अग्रिम पठन

• Daniel Kroening; Ofer Strichman (2008). Decision Procedures: An Algorithmic Point of View. Springer Science & Business Media. ISBN 978-3-540-74104-6.
• A. Biere; M. Heule; H. van Maaren; T. Walsh, eds. (2009). Handbook of Satisfiability. IOS Press. ISBN 978-1-60750-376-7.