संतोषप्रदता

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

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

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

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

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

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

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

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

Main article: Propositional satisfiability

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

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

प्रथम-क्रम तर्क (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)

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

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

Constraints over:	rationals	integers	natural numbers
Linear equations	PTIME	PTIME	NP-complete
Linear inequalities	PTIME	NP-complete	NP-complete

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

यह भी देखें

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