💻 computer science

Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols

यह शोधपत्र सार्वभौमिक परिमाणकों (universal quantifiers) और अनइंटरप्रिटेड फंक्शन सिम्बल्स (uninterpreted function symbols) को संयोजित करने वाले सूत्रों के लिए एक इंडक्टिव सैटिस्फिएबिलिटी सर्टिफिकेशन पद्धति प्रस्तुत करता है, जो उन मामलों में सैटिस्फिएबिलिटी को सफलतापूर्वक सिद्ध करता है जहाँ वर्तमान SMT सॉल्वर स्पष्ट मॉडल बनाने में असमर्थता के कारण विफल हो जाते हैं।

मूल लेखक: Stefan Ratschan, Anggha Nugraha, Mikoláš Janota, Marek Dančo

प्रकाशित 2026-02-19

📖 5 मिनट में पढ़ें🧠 गहराई से पढ़ें

CC BY 4.0

मूल लेखक: Stefan Ratschan, Anggha Nugraha, Mikoláš Janota, Marek Dančo

मूल पेपर CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) के तहत लाइसेंस किया गया है। ✨ नीचे दिए गए पेपर की यह व्याख्या AI से तैयार की गई है। इसे लेखकों ने न तो लिखा है, न इसका समर्थन किया है। तकनीकी सटीकता के लिए मूल पेपर देखें। पूरा डिस्क्लेमर पढ़ें

कल्पना कीजिए कि आप एक जासूस हैं जो एक रहस्य सुलझाने की कोशिश कर रहे हैं: क्या नियमों का एक विशिष्ट समूह वास्तव में किसी समाधान को अस्तित्व में आने की अनुमति देता है?

कंप्यूटर विज्ञान की दुनिया में, इसे "सैटिस्फिएबिलिटी" (Satisfiability) समस्या कहा जाता है। आपके पास एक तार्किक पहेली (एक फॉर्मूला) है जिसमें वेरिएबल्स, गणित और कुछ रहस्यमय "ब्लैक बॉक्स" फंक्शन (जैसे कि एक मशीन जो एक नंबर लेती है और दूसरा नंबर बाहर निकालती है, लेकिन आप नहीं जानते कि वह अंदर से कैसे काम करती है) शामिल हैं। आप यह जानना चाहते हैं: क्या कोई ऐसा तरीका है जिससे संख्याओं को इस तरह सेट किया जाए कि सभी नियम एक ही समय में खुश रहें?

समस्या: द "इनफिनिट" ट्रैप (अनंत का जाल)

वर्तमान कंप्यूटर जासूस (जिन्हें SMT Solvers कहा जाता है) यह सिद्ध करने में अविश्वसनीय रूप से कुशल हैं कि कोई पहेली असंभव (unsatisfiable) है। वे जल्दी से एक विरोधाभास ढूंढ सकते हैं, जैसे कि "यह नियम कहता है कि X, 5 है, लेकिन वह नियम कहता है कि X, 6 है।"

हालांकि, वे तब संघर्ष करते हैं जब उत्तर हाँ (satisfiable) हो, खासकर यदि समाधान के लिए अनंत चरणों या एक ऐसे पैटर्न की आवश्यकता हो जो अनंत काल तक चलता रहे।

पुराना तरीका: एक समाधान मौजूद है, यह सिद्ध करने के लिए, ये सॉल्वर उत्तर का एक भौतिक मॉडल बनाने की कोशिश करते हैं। वे हर एक संख्या के लिए मान (value) लिखने की कोशिश करते हैं।
विफलता: यदि समाधान के लिए एक अनंत पैटर्न की आवश्यकता है (जैसे कि एक फंक्शन जो ऋणात्मक अनंत से धनात्मक अनंत तक प्रत्येक पूर्णांक के लिए काम करता है), तो कंप्यूटर की मेमोरी खत्म हो जाती है। यह समुद्र तट पर मौजूद रेत के हर एक कण को लिखने की कोशिश करने जैसा है ताकि यह साबित किया जा सके कि समुद्र तट मौजूद है। यदि समुद्र तट अनंत है, तो आप कभी भी लिखना समाप्त नहीं कर पाएंगे।

नया विचार: द "इंडक्टिव सर्टिफिकेट" (आगमनात्मक प्रमाण पत्र)

इस शोध पत्र के लेखक एक स्मार्ट तरीका प्रस्तावित करते हैं। पूरे समुद्र तट को लिखने के बजाय, वे एक मैप या एक रेसिपी लिखना चाहते हैं जो यह सिद्ध करे कि समुद्र तट मौजूद है।

वे इसे "सैटिस्फिएबिलिटी सर्टिफिकेट" (Satisfiability Certificate) कहते हैं।

इसे एक डोमिनो प्रभाव की तरह समझें:

बेस केस (आधार मामला): आप संख्याओं के एक छोटे, परिमित समूह (जैसे, 0, 1 और 2) के लिए नियमों को सिद्ध करते हैं।
इंडक्टिव स्टेप (आगमनात्मक चरण): आप एक नियम सिद्ध करते हैं कि, "यदि नियम संख्या $N$ के लिए काम करते हैं, तो वे स्वचालित रूप से संख्या $N+1$ के लिए भी काम करेंगे।"

यदि आपके पास दोनों हैं, तो आपको हर संख्या की जांच करने की आवश्यकता नहीं है। आपको बस शुरुआती बिंदु और आगे बढ़ने के नियम की जांच करनी है। यह गणितीय आगमन (Mathematical Induction) है।

यह कैसे काम करता है (रूपक)

कल्पना कीजिए कि आप एक नदी के पार एक पुल बना रहे हैं जो अनंत रूप से चौड़ी है।

पुराने सॉल्वर: वे शुरुआत से अंत तक हर एक ईंट बिछाने की कोशिश करते हैं। वे थक जाते हैं और हार मान लेते हैं क्योंकि नदी बहुत लंबी है।
यह नया तरीका:
1. वे पहले कुछ मीटरों के लिए एक ठोस नींव रखते हैं (प्री-सैटिस्फिएबिलिटी सर्टिफिकेट)।
2. वे एक मशीन (प्रोपगेटर/Propagator) डिजाइन करते हैं जो पुल के किसी भी मौजूदा हिस्से को ले सकती है और उसे स्वचालित रूप से एक मीटर आगे बढ़ा सकती है, यह सुनिश्चित करते हुए कि नया हिस्सा पुराने हिस्से के साथ पूरी तरह फिट बैठता है।
3. वे यह सिद्ध करते हैं कि यह मशीन किसी भी दिशा (आगे या पीछे) के लिए काम करती है।

यदि वे दिखा सकते हैं कि नींव ठोस है और मशीन काम करती है, तो उनके पास एक सर्टिफिकेट है कि पुल मौजूद है, भले ही उन्होंने पूरा पुल कभी बनाया न हो।

"ReqPivot" की स्थिति

यहाँ एक पेच है। यह "मशीन" (इंडक्टिव स्टेप) केवल तभी काम करती है जब पहेली के नियम "व्यवस्थित" (well-behaved) हों।
शोध पत्र में ReqPivot नामक एक स्थिति पेश की गई है।

उपमा: कल्पना कीजिए कि आप एक पैटर्न को बढ़ाने की कोशिश कर रहे हैं। यदि पैटर्न अराजक है (जैसे, "यदि आप चरण 1 पर हैं, तो 100 पर जाएं; यदि आप चरण 2 पर हैं, तो 3 पर जाएं"), तो आप अगले चरण की आसानी से भविष्यवाणी नहीं कर सकते।
ReqPivot की स्थिति यह सुनिश्चित करती है कि पैटर्न इतना "स्मूथ" (सुचारू) है कि मशीन अगली कार्रवाई की विश्वसनीय रूप से भविष्यवाणी कर सके। यह जाँचता है कि क्या पैटर्न के "चरम" (उच्चतम और निम्नतम संख्याएं) को लगातार संभाला जा सकता है।

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

लेखकों ने अपने तरीके का परीक्षण उन समस्याओं पर किया जिन्होंने दुनिया के सर्वश्रेष्ठ वर्तमान सॉल्वर्स (जैसे Z3 और CVC5) को उलझा दिया था।

परिणाम: उनके तरीके ने उन समस्याओं को हल किया जिनमें अनंत मॉडल या बहुत बड़े, जटिल पैटर्न की आवश्यकता थी।
गति: जबकि पुराने सॉल्वर्स का समय समाप्त हो गया या वे भ्रमित हो गए, इस नए तरीके ने "ब्रूट फोर्स" (पूरा मॉडल बनाने) के बजाय "रेसिपी" (इंडक्शन) का उपयोग करके उत्तर लगभग तुरंत खोज लिया।

सारांश

यह शोध पत्र कंप्यूटर तर्क के लिए एक नया उपकरण पेश करता है। किसी पहेली के संपूर्ण अनंत समाधान को बनाने की कोशिश करने के (जो कि असंभव है) के बजाय, यह एक प्रूफ सर्टिफिकेट बनाता है। यह सर्टिफिकेट एक छोटे, सत्यापित शुरुआती बिंदु और एक नियम का संयोजन है जो यह सिद्ध करता है कि समाधान को अनंत काल तक बढ़ाया जा सकता है। यह ब्रह्मांड के हर तारे को गिनने की कोशिश करने बनाम यह सिद्ध करने के बीच का अंतर है कि तारे एक ऐसे पैटर्न का पालन करते हैं जो उनके अस्तित्व की गारंटी देता है।

यह कंप्यूटरों को आत्मविश्वास से यह कहने की अनुमति देता है, "हाँ, एक समाधान मौजूद है," भले ही वह समाधान इतना बड़ा हो कि उसे कभी लिखा न जा सके।

यहाँ Ratschan et al. के शोध पत्र "Inductive Satisfiability Certification for Universal Quantifiers and Uninterpreted Function Symbols" का विस्तृत तकनीकी सारांश दिया गया है।

1. समस्या विवरण (Problem Statement)

यह शोध पत्र वर्तमान सैटिस्फिएबिलिटी मोड्यूलो थ्योरीज (SMT) सॉल्वर्स की एक महत्वपूर्ण सीमा को संबोधित करता है: यूनिवर्सल क्वांटिफायर (Universal Quantifiers) और अनइंटरप्रिटेड फंक्शन सिम्बल्स (Uninterpreted Function Symbols - UFS) वाले फॉर्मूलों के लिए सैटिस्फिएबिलिटी (Satisfiability) को कुशलतापूर्वक सिद्ध करने में असमर्थता, विशेष रूप से जब इन्हें लीनियर इंटीजर अरिथमेटिक (Linear Integer Arithmetic - LIA) के साथ जोड़ा जाता है।

संदर्भ: यह संयोजन SMTLIB लॉजिक UFLIA (Uninterpreted Functions with Linear Integer Arithmetic) के अनुरूप है, जो आम तौर पर अनडिसाइडेबल (undecidable) है।
वर्तमान सीमाएँ:
- SMT सॉल्वर्स 'अनसैटिस्फिएबिलिटी' (unsatisfiability/refutation) सिद्ध करने के लिए अत्यधिक अनुकूलित हैं।
- सैटिस्फिएबिलिटी सिद्ध करने के लिए, सॉल्वर्स आमतौर पर स्पष्ट मॉडल निर्माण (explicit model construction) (एक परिमित मॉडल खोजना) पर निर्भर करते हैं।
- यह दृष्टिकोण उन फॉर्मूलों के लिए विफल हो जाता है जहाँ सबसे छोटा मॉडल अनंत (infinite) होता है (जैसे, $f(0)=0 \land \forall x. f(x+1) = f(x)+1$ ) या जहाँ सबसे छोटा परिमित (finite) मॉडल अत्यधिक बड़ा होता है।
- मौजूदा ह्यूरिस्टिक्स अक्सर ऐरे रीजनिंग (array reasoning) और ऑफसेट-आधारित बाधाओं (जैसे, $a[i+c]$ ) के साथ संघर्ष करते हैं।

2. कार्यप्रणाली (Methodology)

लेखक एक वैकल्पिक दृष्टिकोण प्रस्तावित करते हैं: इंडक्टिव सैटिस्फिएबिलिटी सर्टिफिकेशन (Inductive Satisfiability Certification)। एक पूर्ण मॉडल का निर्माण करने के बजाय, एल्गोरिदम एक सर्टिफिकेट (certificate) उत्पन्न करता है जो इंडक्शन तर्कों (induction arguments) के माध्यम से सैटिस्फिएबिलिटी को सिद्ध करता है।

मुख्य अवधारणाएँ (Core Concepts)

सैटिस्फिएबिलिटी सर्टिफिकेट (Satisfiability Certificate): एक वस्तु जिसमें शामिल है:
1. प्री-सैटिस्फिएबिलिटी सर्टिफिकेट ( $I$ ): एक आंशिक व्याख्या (सेल इंटरप्रिटेशन) जो क्वांटिफायर-फ्री भाग ( $F$ ) और क्वांटिफाइड भाग ( $Q$ ) के तर्कों के लिए विशिष्ट ग्राउंड टर्म्स और अनइंटरप्रेटेड फंक्शन्स को मान (values) आवंटित करती है।
2. वेल-ऑर्डर ( $\preceq$ ): क्वांटिफाइड वेरिएबल्स के डोमेन पर इंडक्शन की दिशा को परिभाषित करता है।
3. प्रोपैगेटेड सेल्स ( $X_z$ ): क्वांटिफाइड वेरिएबल के प्रत्येक इंस्टेंशिएशन $z$ के लिए, प्रोपैगेटेड सेल्स का एक सेट जिनके मान एक सैटिस्फिएबिलिटी प्रोपोगेटर (Satisfiability Propagator) द्वारा निर्धारित होते हैं।
4. सैटिस्फिएबिलिटी प्रोपोगेटर: एक तंत्र जो यह सिद्ध करता है कि किसी भी इंस्टेंशिएशन $z$ के लिए, प्रोपैगेटेड सेल्स को इस प्रकार मान दिए जा सकते हैं कि क्वांटिफाइड फॉर्मूला $Q$ सत्य हो जाए, बिना पहले से आवंटित मानों के साथ संघर्ष किए।

एल्गोरिदम (UFLIA फ्रैगमेंट)

शोध पत्र UFLIA के एक विशिष्ट फ्रैगमेंट पर ध्यान केंद्रित करता है जिसमें निम्नलिखित प्रतिबंध हैं:

अनइंटरप्रेटेड फंक्शन्स की अरिटी (arity) 1 है।
केवल एक क्वांटिफाइड वेरिएबल ( $x$ ) है।
फंक्शन आर्गुमेंट्स में क्वांटिफाइड वेरिएबल के लिए यूनिफॉर्म कोएफिशिएंट्स (uniform coefficients) हैं (जैसे, $f(2x+3)$ अनुमत है, लेकिन $f(2x+3) = f(x+1)$ नहीं है)।

एल्गोरिदम (Algorithm 1):

इनिशियलाइजेशन (Initialization): एक बेस इंटरवल $B = [0, 0]$ के साथ शुरू करें।
बेस चेक (Check Base): सत्यापित करें कि क्या सभी इंस्टेंशिएशन $x \in B$ के लिए फॉर्मूला सैटिस्फिएबल है।
प्रोपैगेशन चेक (Check Propagation - ReqPivot Condition):
- एल्गोरिदम जाँचता है कि क्या फॉर्मूला ReqPivot कंडीशन को संतुष्ट करता है। इसमें टर्म्स के ऐसे उपसमुच्चय ( $S$ ) खोजना शामिल है जो "एक्सट्रीमल" (extremal) हैं (जैसे, सबसे छोटे या सबसे बड़े आर्गुमेंट्स), ताकि मानों को इंटरवल $B$ से अनंत की ओर पॉजिटिव ( $+$ ) और नेगेटिव ($-$) दोनों दिशाओं में प्रसारित (propagate) किया जा सके।
- यह प्रोपैगेबिलिटी (Propagability) को सत्यापित करता है: क्या गैर-एक्सट्रीमल टर्म्स के मानों की परवाह किए बिना $Q$ को संतुष्ट करने के लिए एक्सट्रीमल टर्म्स को मान दिए जा सकते हैं?
- यह क्लैश कंडीशंस (Clash Conditions) को सत्यापित करता है: सुनिश्चित करें कि प्रोपैगेटेड सेल्स, क्वांटिफायर-फ्री भाग $F$ में परिभाषित ग्राउंड टर्म्स के साथ टकराते (collide) नहीं हैं।
इटरेशन (Iteration): यदि बेस इंटरवल और प्रोपैगेशन स्थितियाँ संतुष्ट हैं, तो Sat लौटाएं। यदि नहीं, तो इंटरवल $B$ को सममित रूप से (symmetrically) विस्तारित करें और दोहराएं।
समाप्ति (Termination): यदि इनपुट फॉर्मूला सैटिस्फिएबल है और ReqPivot कंडीशन को पूरा करता है, तो एल्गोरिदम गारंटी के साथ समाप्त होगा और Sat लौटाएगा।

प्रोपोजीशनल एनकोडिंग (Propositional Encoding)

सभी संभावित उपसमुच्चयों $S$ की स्पष्ट रूप से जाँच करने के कारण होने वाले एक्सपोनेंशियल ब्लोअप (exponential blowup) से बचने के लिए, लेखक एक कॉम्पैक्ट CNF एनकोडिंग (Compact CNF Encoding) पेश करते हैं। वे एक्सट्रीमल सेट्स में सदस्यता का प्रतिनिधित्व करने के लिए सहायक बूलियन वेरिएबल्स का उपयोग करते हैं, जिससे शर्तों को मानक SAT/SMT सॉल्वर्स द्वारा कुशलतापूर्वक जांचा जा सकता है।

3. प्रमुख योगदान (Key Contributions)

इंडक्टिव सर्टिफिकेशन फ्रेमवर्क: एक "सैटिस्फिएबिलिटी सर्टिफिकेट" की औपचारिक परिभाषा पेश की जो स्पष्ट मॉडल निर्माण के स्थान पर इंडक्टिव प्रमाणों का उपयोग करती है। यह अनंत मॉडलों वाले फॉर्मूलों के लिए सैटिस्फिएबिलिटी सिद्ध करना सक्षम बनाता है।
ReqPivot कंडीशन: एक ऐसी सिमेंटिक स्थिति को परिभाषित किया जो UFLIA फॉर्मूलों के लिए एक वैध इंडक्टिव प्रोपगेशन रणनीति के अस्तित्व की गारंटी देती है।
UFLIA के लिए एल्गोरिदम: एक ठोस एल्गोरिदम विकसित किया जो एक वैध इंटरवल और प्रोपगेशन रणनीति की खोज करता है, जो साउंडनेस (soundness) और रिलेटिव कम्प्लीटनेस (relative completeness - ReqPivot धारणा के तहत पूर्णता) सिद्ध करता है।
कुशल एनकोडिंग: प्रोपैगेशन के लिए उपसमुच्चय चयन को कम्प्यूटेशनल रूप से व्यवहार्य बनाने के लिए एक CNF एनकोडिंग प्रदान की।
मॉडल एक्सट्रैक्शन: एक रिकर्सिव इवैल्यूएशन फंक्शन का उपयोग करके सर्टिफिकेट से मॉडल (फंक्शन सिम्बल्स के मान) को कम्प्यूटेशनल रूप से निकालने का तरीका प्रदर्शित किया।

4. प्रयोगात्मक परिणाम (Experimental Results)

लेखकों ने अपने एल्गोरिदम को Z3 API का उपयोग करके Python में लागू किया और इसकी तुलना अत्याधुनिक सॉल्वर्स Z3 और CVC5 (CVC5 के SyGuS मोड सहित) के विरुद्ध की।

टेस्ट सुइट: UFS और LIA वाले 28 हस्तनिर्मित (handcrafted) सैटिस्फिएबल समस्याओं का परीक्षण किया गया, जिनमें मॉडल के आकार को एक पैरामीटर $c$ द्वारा नियंत्रित किया गया।
प्रदर्शन:
- प्रस्तावित एल्गोरिदम: सभी 28 समस्याओं को नगण्य समय में हल किया, चाहे मॉडल आकार पैरामीटर $c$ कुछ भी हो। इसका रनटाइम स्थिर था क्योंकि इंडक्शन लॉजिक डोमेन के आकार को एब्सट्रैक्ट (abstract) कर देता है।
- Z3: काफी संघर्ष करता है। बड़े $c$ के लिए, यह अक्सर "Unknown" लौटाता है या टाइमआउट हो जाता है। इसने केवल 4 अनबाउंडेड (unbounded) समस्याओं को हल किया।
- CVC5 (Standard): जैसे-जैसे $c$ बढ़ता है, यह टाइमआउट हो जाता है या विफल हो जाता है।
- CVC5 (SyGuS): 15 समस्याओं को तेज़ी से हल करता है लेकिन उन फॉर्मूलों पर विफल हो जाता है जिन्हें इसके डिफ़ॉल्ट व्याकरण (grammar) से बाहर के फंक्शन की आवश्यकता होती है (जैसे, $f(x+1) = 2f(x)$ )।
मुख्य निष्कर्ष: इंडक्टिव दृष्टिकोण उन फॉर्मूलों के लिए श्रेष्ठ है जहाँ मॉडल अनंत है या स्पष्ट निर्माण के लिए बहुत बड़ा है, एक ऐसी स्थिति जहाँ वर्तमान SMT सॉल्वर्स विफल हो जाते हैं।

5. महत्व और भविष्य का कार्य (Significance and Future Work)

अंतराल को भरना (Bridging the Gap): यह कार्य एक विश्वसनीय विधि प्रदान करके ऑटोमेटेड रीजनिंग में एक बड़ा अंतर भरता है, जो उन अनडिसाइडेबल समस्याओं के लिए सैटिस्फिएबिलिटी सिद्ध करने के काम आता है जो प्रोग्राम वेरिफिकेशन (जैसे, ऐरे प्रॉपर्टीज) में सामान्य हैं।
परिमित मॉडलों से परे: यह उन सिस्टम के सत्यापन को सक्षम बनाता है जहाँ स्टेट स्पेस अनंत होता है, जो कि मानक SMT सॉल्वर्स के लिए पहले असंभव कार्य था।
भविष्य की दिशाएँ: लेखकों का लक्ष्य सिंथेटिक प्रतिबंधों को कम करना (जैसे, नॉन-यूनिफॉर्म कोएफिशिएंट्स के साथ कई क्वांटिफाइड वेरिएबल्स को संभालना) और सिमेंटिक ReqPivot कंडीशन को व्यापक बनाना है, संभवतः मजबूत इंडक्शन रूपों या सामान्यीकृत थ्योरी सपोर्ट का उपयोग करके।

संक्षेप में, यह शोध पत्र "मॉडल खोजने" से "इंडक्शन के माध्यम से मॉडल के अस्तित्व को प्रमाणित करने" की ओर एक प्रतिमान परिवर्तन (paradigm shift) प्रस्तुत करता है, जो उन समस्याओं के वर्ग के लिए एक मजबूत समाधान प्रदान करता है जो वर्तमान सर्वश्रेष्ठ SMT सॉल्वर्स को विफल कर देते हैं।