संतोषप्रदता

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

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

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

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

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

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

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

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

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

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

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

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

मॉडल सिद्धांत में संतुष्टि

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

ए ⊧ φ [ए]

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

ए ⊧ φ

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

ए ⊧ टी

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

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

परिमित संतुष्टि एवं संतुष्टि को सामान्य रूप से मेल नहीं खाना चाहिए। उदाहरण के लिए, निम्नलिखित वाक्यों के तार्किक संयोजन के रूप में प्राप्त प्रथम-क्रम तर्क सूत्र पर विचार करें, जहाँ $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: Satisfiability modulo theories and Constraint satisfaction problem

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

Constraints	over reals	over integers
Linear	PTIME (see linear programming)	NP-complete (see integer programming)
Polynomial	decidable through e.g. Cylindrical algebraic decomposition	undecidable (Hilbert's tenth problem)

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

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