Revisiting Incremental Linearization for Nonlinear Integer Arithmetic

कल्पना कीजिए कि आप एक जासूस हैं जो एक रहस्य को सुलझाने की कोशिश कर रहे हैं, लेकिन आपको जो सुराग दिए गए हैं वे एक ऐसी भाषा में लिखे गए हैं जिसका अर्थ इस बात पर निर्भर करता है कि आप उन्हें कैसे देखते हैं। यह सैटिस्फिएबिलिटी मोडुलो थ्योरीज (SMT) की दुनिया है, जो कंप्यूटर विज्ञान की एक शाखा है जहाँ सॉफ़्टवेयर यह पता लगाने की कोशिश करता है कि क्या तर्क के नियमों का एक समूह कभी एक साथ सत्य हो सकता है। इसे एक सुपर-स्मार्ट पहेली सुलझाने वाले के रूप में समझें जो यह जाँचता है कि क्या कोई प्रोग्राम क्रैश हो जाएगा, या क्या कोई गुप्त कोड तोड़ा जा सकता है, या क्या किसी रोबोट का रास्ता सुरक्षित है।

ज्यादातर समय, ये पहेलियाँ आसान होती हैं क्योंकि इनमें केवल सीधी रेखाएँ और सरल जोड़ शामिल होते हैं (जैसे $x + y = 5$)। कंप्यूटर इसमें अद्भुत हैं। लेकिन जीवन बहुत उलझ जाता है जब आप इसमें नॉनलीनियर अरिथमेटिक (nonlinear arithmetic) पेश करते हैं—ऐसे नियम जहाँ चीजों को आपस में गुणा किया जाता है या उनकी घात (powers) ली जाती है (जैसे $x \times y$ या $x^3$)। अचानक, नियम मुड़ने लगते हैं और टेढ़े-मेढ़े हो जाते हैं, और गणित अविश्वसनीय रूप से कठिन हो जाता है। वास्तव में, पूर्ण संख्याओं (whole numbers) के लिए, इन सभी पहेलियों को हल करने के लिए एक आदर्श, 100% पूर्ण विधि बनाना गणितीय रूप से असंभव है। इसी कारण से, कंप्यूटर वैज्ञानिक "काफी अच्छे" जासूस बनाते हैं जो तेजी से उत्तर खोजने के लिए चतुर शॉर्टकट का उपयोग करते हैं, भले ही वे हर असंभव मामले को हल करने का वादा नहीं कर सकते।

आप जो शोध पत्र पढ़ने जा रहे हैं, वह एक नए जासूस, जिसका नाम qfn2l है, का परिचय देता है, जो पहले के जासूसों की तुलना में इन पेचीदा, घुमावदार पहेलियों को सुलझाने में बेहतर है। लेखकों ने, जो प्राग के चेक टेक्निकल यूनिवर्सिटी के शोधकर्ता हैं, महसूस किया कि पुराने शॉर्टकट एक विशिष्ट प्रकार की कठिन पहेली के साथ संघर्ष कर रहे थे: वे पहेलियाँ जिनमें घात (powers) (जैसे $x^3$) और मिक्स्ड प्रोडक्ट्स (mixed products) (जैसे $x^2y$) शामिल थे। उन्होंने जासूस के टूलकिट को नए नियमों के एक ताज़ा सेट के साथ अपग्रेड करने का निर्णय लिया जो एक तंग जाल की तरह काम करते हैं, जिससे उन गलत अनुमानों को पकड़ा जा सके जो पहले फिसल जाते थे।

पुराना तरीका: अनइंटरप्रिटेड फंक्शन्स के साथ अनुमान लगाना

इस अपग्रेड को समझने के लिए, आइए देखें कि पिछले जासूस कैसे काम करते थे। कल्पना कीजिए कि आपके पास एक रहस्यमय बॉक्स है जिस पर $f(x, y)$ लिखा है। आप नहीं जानते कि इसके अंदर क्या है, लेकिन आप जानते हैं कि यदि आप इसमें समान संख्याएँ डालेंगे, तो आपको समान संख्या प्राप्त होगी। पुराने तरीके ने हर गुणन (multiplication), जैसे $x \times y$, को इसी रहस्यमय बॉक्स के रूप में माना। कंप्यूटर इस बॉक्स के लिए एक मान (value) का अनुमान लगाता था, यह जाँचता था कि क्या यह तर्कसंगत है, और यदि नहीं, तो वह सुधार के लिए एक नियम जोड़ देता था।

यह सरल मामलों में ठीक काम करता था, लेकिन यह एक तरबूज का वजन केवल यह जानकर अनुमान लगाने जैसा था कि वह "भारी" है। यह बहुत अस्पष्ट था। जब पहेली में उच्च घात, जैसे $x^3$, शामिल होती थी, तो पुराने नियम बहुत ढीले थे। जासूस एक मान का अनुमान लगाता था, कंप्यूटर कहता, "नहीं, यह फिट नहीं बैठता," और फिर सुधार के लिए एक बहुत ही कमजोर नियम जोड़ देता था। जासूस को बार-बार अनुमान लगाना पड़ता, विफल होना पड़ता और फिर से अनुमान लगाना पड़ता, और अक्सर उत्तर खोजने से पहले ही उसका समय समाप्त हो जाता।

नया तरीका: सेकेंट्स (Secants) के साथ जाल को कसना

लेखकों ने तय किया कि वे इन घातों को रहस्यमय बॉक्स के रूप में मानना बंद करेंगे और इसके बजाय उन्हें ताज़ा स्थिरांकों (fresh constants)—यानी केवल साधारण संख्याएँ जो घात के परिणाम का प्रतिनिधित्व करती हैं—के रूप में मानेंगे। लेकिन असली जादू उन नियमों में है जो उन्होंने इन संख्याओं की जाँच करने के लिए जोड़े हैं।

उन्होंने खोजा कि किसी भी पूर्ण संख्या, मान लीजिए $v$, के लिए, फलन $x^k$ (जैसे $x^3$) $v$ और $v+1$ के बीच एक बहुत ही अनुमानित तरीके से व्यवहार करता है। उन्होंने सेकेंट लाइन्स (secant lines) पर आधारित नियमों का एक नया सेट बनाया। कल्पना कीजिए कि ग्राफ पर एक वक्र (curve) है। एक सेकेंट लाइन वह सीधी रेखा है जो उस वक्र पर दो बिंदुओं को जोड़ती है। लेखकों ने महसूस किया कि यदि आप बिंदु $(v, v^k)$ और अगले पूर्णांक बिंदु के बीच एक सीधी रेखा खींचते हैं, तो वह रेखा उत्तर के वक्र के चारों ओर एक बहुत ही तंग "बाड़" (fence) बनाती है।

यहाँ समानता दी गई है:

• पुराना तरीका: जासूस संभावित उत्तरों के चारों ओर एक बड़ा, ढीला घेरा बनाता था। इसे बनाना आसान था, लेकिन इसने कई गलत अनुमानों को अंदर आने दिया।
• नया तरीका: जासूस उत्तर के वक्र को बहुत करीब से छूने वाली कई तंग, सीधी बाड़ें (secant lines) बनाता है। यदि कोई अनुमान इन तंग बाड़ों के बाहर गिरता है, तो जासूस तुरंत जान जाता है कि वह गलत है और अनुमान को वापस अंदर धकेलने के लिए एक नियम जोड़ देता है।

क्योंकि ये बाड़ें इतनी तंग हैं, इसलिए जासूस को उतनी बार अनुमान नहीं लगाना पड़ता। यह उत्तर के सही मान की ओर बहुत तेजी से बढ़ता है, विशेष रूप से क्यूब्स और मिक्स्ड प्रोडक्ट्स वाली पहेलियों के लिए।

"तीन क्यूब्स का योग" चुनौती

अपने नए जासूस को काम करते हुए सिद्ध करने के लिए, लेखों ने "तीन क्यूब्स के योग" (sum of three cubes) नामक प्रसिद्ध पहेलियों के एक वर्ग पर इसका परीक्षण किया। ये वे समस्याएँ हैं जो पूछती हैं: "क्या आप तीन पूर्ण संख्याएँ पा सकते हैं जिन्हें क्यूब करने और जोड़ने पर एक विशिष्ट संख्या प्राप्त होती है?"

उदाहरण के लिए, पहेली ऐसी हो सकती है: $x^3 + y^3 + z^3 = 79$।

यह मानक सॉल्वर के लिए एक दुःस्वप्न है। संख्याएँ बहुत बड़ी हो सकती हैं, और संबंध जटिल होते हैं। लेखकों ने अपने नए सॉल्वर, qfn2l, का परीक्षण सबसे अच्छे मौजूदा सॉल्वर्स (जैसे Z3, cvc5, और MathSAT) के विरुद्ध किया।

• अन्य सॉल्वर्स ने $x^3 + y^3 + z^3 = 79$ पहेली को हल करने की कोशिश की लेकिन 3 मिनट के बाद हार मान ली (उन्होंने "टाइम आउट" दिया)।
• नए सॉल्वर, qfn2l ने केवल 20 सेकंड में उत्तर ढूंढ लिया—$x = -19, y = 35, z = -33$।

परिणाम: एक प्रतिस्पर्धी नया दावेदार

शोधकर्ताओं ने अपने सॉल्वर को SMT-LIB नामक एक मानक लाइब्रेरी से 25,444 पहेलियों के विशाल संग्रह पर चलाया। यहाँ उन्होंने क्या पाया:

1. कुल प्रदर्शन: नया सॉल्वर बाहर के बेहतरीन उपकरणों के साथ प्रतिस्पर्धी है। इसने कुल मिलाकर लगभग 14,000 पहेलियाँ हल कीं, जो शीर्ष प्रदर्शन करने वालों के करीब है, हालांकि यह हर एक प्रकार की पहेली पर सबसे अच्छे (जैसे Z3) को नहीं हरा सका।
2. खास क्षेत्र (Sweet Spot): नया सॉल्वर उन पहेलियों पर पूरी तरह चमकता है जो घातों और मिक्स्ड प्रोडक्ट्स द्वारा संचालित होती हैं। "MathProblems" परिवार पर, इसने लगभग 53% मामलों को हल किया (1,100 में से 585 से 587)। अन्य सॉल्वर्स इन विशिष्ट प्रकार की समस्याओं के साथ काफी संघर्ष करते रहे।
3. समझौता (Trade-off): लेखकों ने अपने सॉल्वर के एक संस्करण का परीक्षण किया जो यह जाँचने के लिए अतिरिक्त सावधानी बरतता है कि क्या पहेली के विभिन्न भाग सुसंगत हैं (जिसे "कंग्रुएंस एक्सिओम्स" कहा जाता है)। उन्होंने पाया कि यह अतिरिक्त जाँच वास्तव में सामान्य पहेलियों पर सॉल्वर को धीमा कर देती है, जिससे कुल मिलाकर लगभग 1,600 कम मामले हल हुए। यह सुझाव देता है कि अधिकांश समस्याओं के लिए, तंग बाड़ (secant bounds) पर्याप्त हैं, और आपको हर एक निरंतरता नियम की जाँच करने के लिए अतिरिक्त भारी काम करने की आवश्यकता नहीं है।

यह क्यों महत्वपूर्ण है

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

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

संक्षेप में, लेखकों ने एक बिखरी हुई, घुमावदार समस्या ली और उसके चारों ओर तंग रेखाएँ खींचीं, जिससे कंप्यूटर पहले की तुलना में बहुत तेज़ी से सत्य तक पहुँच सका।