हां, nonlinear पूर्णांक अंकगणित के लिए निर्णय समस्या अपरिहार्य है। हम nonlinear पूर्णांक अंकगणित में ट्यूरिंग मशीनों के लिए हलिंग समस्या को एन्कोड कर सकते हैं। मैं इस समस्या में रूचि रखने वाले किसी भी व्यक्ति के लिए सुंदर पुस्तक Hilbert's tenth problem की दृढ़ता से अनुशंसा करता हूं।
ध्यान दें कि, यदि किसी सूत्र के पास समाधान है, तो हम इसे हमेशा ब्रूट फोर्स द्वारा पा सकते हैं। यही है, हम सभी संभावित असाइनमेंट की गणना करते रहते हैं, और परीक्षण करते हैं कि वे सूत्र को संतुष्ट करते हैं या नहीं। यह केवल प्रोग्राम चलाने और यह निर्धारित करने के बाद कि क्या यह किसी दिए गए चरणों के बाद समाप्त हो जाता है, यह हल करके समस्या को हल करने की कोशिश करने से अलग नहीं है।
Z3 एक निष्पक्ष गणना नहीं करता है। k की संख्या को देखते हुए, यह k बिट्स का उपयोग करके प्रत्येक पूर्णांक चर को एन्कोड करता है और सब कुछ प्रस्तावित तर्क में कम कर देता है। फिर, एक समाधान खोजने के लिए एक एसएटी सॉल्वर का उपयोग किया जाता है। यदि कोई समाधान मिलता है, तो यह इसे मूल सूत्र के लिए एक पूर्णांक समाधान में परिवर्तित कर देता है। यदि प्रस्ताव औपचारिक औपचारिकता के लिए कोई समाधान नहीं है, तो यह k को बढ़ाने की कोशिश करता है, या एक अलग रणनीति पर स्विच करता है। प्रस्तावित तर्क में यह कमी अनिवार्य रूप से एक मॉडल/समाधान खोजने की प्रक्रिया है। यह नहीं दिखा सकता कि किसी समस्या में कोई समाधान नहीं है। असल में, उन समस्याओं के लिए जहां प्रत्येक पूर्णांक चर के निचले और ऊपरी बाउंड होते हैं, यह ऐसा कर सकता है। इसलिए, Z3 को कोई समाधान मौजूद नहीं होने के लिए अन्य रणनीतियों का उपयोग करना है।
इसके अलावा, प्रस्तावित तर्क में कमी केवल तभी काम करती है जब बहुत छोटा समाधान होता है (एक समाधान जिसके लिए बिट्स को एन्कोड किया जाना चाहिए)। मैं के बारे में बात करें कि निम्न पोस्ट में:
जेड 3 nonlinear पूर्णांक गणित के लिए अच्छा समर्थन नहीं है। ऊपर वर्णित दृष्टिकोण बहुत सरल है।
http://reference.wolfram.com/legacy/v5_2/functions/AdvancedDocumentationDiophantinePolynomialSystems
अंत में, nonlinear असली अंकगणित (NLSat) solver nonlinear पूर्णांक समस्याओं के लिए डिफ़ॉल्ट रूप से नहीं किया जाता है: मेरी राय में, मेथेमेटिका तकनीक का सबसे व्यापक पोर्टफोलियो है लगता है। यह आमतौर पर पूर्णांक समस्याओं पर बहुत अप्रभावी है। फिर भी, हम पूर्णांक समस्याओं के लिए भी ZL को NLSat का उपयोग करने के लिए मजबूर कर सकते हैं।
(check-sat)
साथ
(check-sat-using qfnra-nlsat)
जब इस आदेश प्रयोग किया जाता है, जेड 3 एक वास्तविक समस्या के रूप में समस्या का समाधान होगा: हम सिर्फ बदलने के लिए। यदि कोई वास्तविक समाधान नहीं मिला है, तो हम जानते हैं कि कोई पूर्णांक समाधान नहीं है। यदि कोई समाधान पाया जाता है, तो Z3 जांच करेगा कि समाधान वास्तव में पूर्णांक चरों को पूर्णांक मान निर्दिष्ट कर रहा है या नहीं। यदि ऐसा नहीं है, तो यह समस्या को हल करने में विफल होने के संकेत देने के लिए unknown वापस कर देगा।
यह एक वैध सवाल है। कृपया इसे वोट न दें, या इसे बंद करने के लिए वोट दें। धन्यवाद। –