💻 computer science

A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals

यह शोध पत्र तर्क $\mathcal{L}_{[\,]}$ के लिए एक निर्णय प्रक्रिया प्रस्तुत करता है, जो अनबाउंडेड (unbounded) चरों की अनुमति देने वाले परिमित पूर्णांक अंतरालों के साथ परिमित सेट थ्योरी का विस्तार करता है, और एक एलीवेटर एल्गोरिदम के लिए इनवेरिएंस लेम्मा (invariance lemmas) को स्वचालित रूप से सत्यापित करने के लिए $\{log\}$ टूल के माध्यम से इसकी व्यावहारिक उपयोगिता को प्रदर्शित करता है।

मूल लेखक: Maximiliano Cristiá, Gianfranco Rossi

प्रकाशित 2026-05-05

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

CC BY 4.0

मूल लेखक: Maximiliano Cristiá, Gianfranco Rossi

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

कल्पना कीजिए कि आप एक बहुत ही विशिष्ट प्रकार के गोदाम का प्रबंधन करने वाले एक कुशल प्रबंधक (master organizer) हैं। इस गोदाम में, आपके पास दो प्रकार की वस्तुएं हैं: बक्से (जो अन्य बक्सों या वस्तुओं को रख सकते हैं) और संख्यांकित शेल्फ (जो पूर्णांकों की एक निरंतर श्रेणी रखते हैं, जैसे शेल्फ 1 से 10 तक)।

लंबे समय तक, कंप्यूटर उपकरण इन बक्सों को पूरी तरह से व्यवस्थित करने में आपकी मदद कर सकते थे। वे बता सकते थे कि क्या दो बक्से एक ही हैं, क्या एक बॉक्स दूसरे के अंदर है, या एक बॉक्स में कितनी वस्तुएं हैं। हालाँकि, जब आपने संख्यांकित शेल्फ के बारे में बात करने की कोशिश की, तो इन उपकरणों के सामने एक दीवार आ गई। वे यह समझने में सक्षम नहीं थे कि एक शेल्फ जो "फ्लोर 3" से "फ्लोर 10" तक फैला हुआ है, उसे एक साथ देखते हुए यह कैसे जांचा जाए कि क्या वस्तुओं का एक विशिष्ट बॉक्स उस शेल्फ पर रखा गया है।

यह शोध पत्र एक नया "सुपर-ऑर्गनाइज़र" टूल (जिसे {log} या "setlog" कहा जाता है) पेश करता है जो बक्सों और संख्यांकित शेल्फ दोनों को एक साथ संभाल सकता है। लेखकों ने इसे कैसे हासिल किया, इसका विवरण सरल उपमाओं के माध्यम से यहाँ दिया गया है।

1. समस्या: "शेल्फ" का अंतर (The "Shelf" Gap)

पहले, टूल निम्नलिखित को संभाल सकता था:

बक्से: "क्या बॉक्स A, बॉक्स B के समान है?" या "बॉक्स C में कितने सेब हैं?"
संख्याएँ: "क्या संख्या 5, संख्या 10 से कम है?"

लेकिन यह मिश्रण को नहीं संभाल सका: "क्या शेल्फ [3, 10] (जिसका अर्थ है शेल्फ 3, 4, 5, 6, 7, 8, 9, और 10) पर मौजूद वस्तुओं का संग्रह बिल्कुल बॉक्स A के समान है?"

लेखक एक ऐसा सिस्टम बनाना चाहते थे जो स्वचालित रूप से यह सिद्ध कर सके कि: "यदि मैं शेल्फ [3, 10] की वस्तुओं को दो समूहों में विभाजित करता हूँ, और दोनों समूहों में वस्तुओं की संख्या समान है, तो शेल्फ में स्लॉट्स की संख्या सम (even) होनी चाहिए।"

2. जादू का तरीका: "पहचान पत्र" (The "Identity Card")

इसे हल करने के लिए, लेखकों ने एक चतुर गणितीय "पहचान पत्र" (एक विशिष्ट नियम) की खोज की जो एक अनुवादक के रूप में कार्य करता है।

एक संख्यांकित शेल्फ (जैसे [3, 10] का अंतराल) को एक बहुत ही कठोर, पहले से पैक किए गए बॉक्स के रूप में सोचें। आप केवल शुरूआती और अंतिम संख्याओं को देखकर जानते हैं कि इसके अंदर क्या है।

नियम: यदि आपके पास एक बॉक्स है, और आप दो चीजें जानते हैं:
1. बॉक्स में मौजूद सब कुछ शेल्फ [3, 10] के भीतर आता है।
2. बॉक्स में वस्तुओं की संख्या बिल्कुल उतनी ही है जितनी उस शेल्फ को भरने के लिए आवश्यक है (इस मामले में 8 वस्तुएं)।
- तो: वह बॉक्स ही वह शेल्फ है। वह शेल्फ [3, 10] के समान है।

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

3. "न्यूनतम समाधान" जासूस (The "Minimum Solution" Detective)

एक बार जब टूल शेल्फ को बॉक्स में अनुवादित कर देता है, तो उसके सामने एक नई चुनौती आती है: हम ब्रह्मांड की हर एक संभावना की जाँच किए बिना यह कैसे जान सकते हैं कि एक समाधान संभव है?

कल्पना कीजिए कि आप एक नियम को संतुष्ट करने वाले लोगों के सबसे छोटे समूह को खोजने की कोशिश कर रहे हैं।

टूल पहले सबसे छोटा संभव समूह ( "न्यूनतम समाधान") खोजता है जो नियमों में फिट बैठता है।
तर्क: यदि सबसे छोटा समूह नियम को पूरा करने में विफल रहता है, तो कोई भी बड़ा समूह भी विफल हो जाएगा। यह एक छोटी कार में एक विशाल हाथी को फिट करने की कोशिश करने जैसा है; यदि कार हाथी के लिए बहुत छोटी है, तो अधिक हाथी जोड़ने से कोई मदद नहीं मिलेगी।
इसके विपरीत, यदि सबसे छोटा समूह काम करता है, तो नियम संतुष्ट होता है।

केवल इन "न्यूनतम" परिदृश्यों की जाँच करके, टूल अनंत संभावनाओं की जाँच करने के अंतहीन लूप में फंसने से बच जाता है। यह सिद्ध करता है कि यदि सरल मामला काम करता है (या विफल होता है), तो पूरी समस्या हल हो जाती है।

4. एलीवेटर टेस्ट (केस स्टडी)

अपने नए टूल के वास्तविक दुनिया में काम करने को सिद्ध करने के लिए, लेखकों ने एक क्लासिक समस्या पर इसका परीक्षण किया: द एलीवेटर एल्गोरिदम।

एक एलीवेटर की कल्पना करें जो मंजिलों के बीच ऊपर-नीचे जा रहा है। इसमें अनुरोध (ऊपर या नीचे जाने के लिए लोग) होते हैं। टूल को एलीवेटर के तर्क को सुरक्षित और सही साबित करना था।

चुनौती: एलीवेटर को यह जानने की आवश्यकता होती है जैसे कि, "यदि मैं फ्लोर 3 पर हूँ और ऊपर जा रहा हूँ, और फ्लोर 5 और 8 पर अनुरोध हैं, तो मैं अगली कौन सी मंजिल पर जाऊँगा?" इसमें मंजिलों के एक रेंज (अंतराल) और अनुरोधों के सेट (बक्सों) के बारे में तर्क देना शामिल है।
परिणाम: टूल ने स्वचालित रूप से एलीवेटर सिस्टम के सभी नियमों (invariants) की जाँच की। इसने सिद्ध किया कि एलीवेटर कभी फंसेगा नहीं, हमेशा सही दिशा में चलेगा, और अनुरोधों को सही ढंग से संभालेगा। इसने यह सब बिना किसी इंसान द्वारा हर एक कदम को मैन्युअल रूप से जांचे किया, जिससे यह सिद्ध हुआ कि प्रणाली तार्किक रूप से सुदृढ़ है।

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

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

यह शोध पत्र एक निर्णय प्रक्रिया (decision procedure) प्रदान करता है। सरल शब्दों में, इसका अर्थ है कि यह टूल एक "हाँ/ना" मशीन है जो निश्चित रूप से उत्तर दे सकती है: "क्या सेट और संख्या श्रेणियों के बारे में यह कथन सत्य है या असत्य?" यह गारंटी देता है कि एक सीमित समय में उत्तर मिलेगा।

सारांश

लेखकों ने दो दुनियाओं के बीच एक पुल बनाया: सेट्स (चीजों के समूह) और इंटर्वल्स (संख्याओं की सीमा)। उन्होंने इसे इस प्रकार किया:

एक ऐसा नियम बनाकर जो "संख्याओं की सीमा" को "वस्तुओं के समूह" में बदल देता है यदि आकार मेल खाता हो।
अनंत संभावनाओं में खो जाने से बचने के लिए "सबसे छोटे मामले" की रणनीति का उपयोग करके।
एक एलीवेटर सिस्टम के लिए सुरक्षा जाँच को स्वचालित करके इसे सफल सिद्ध करके।

परिणामस्वरूप, यह एक ऐसा टूल है जो वस्तुओं के संग्रह और निरंतर संख्या श्रेणियों दोनों से जुड़े जटिल तार्किक नियमों को स्वचालित रूप से सत्यापित कर सकता है, जो पहले स्वचालित रूप से करना बहुत कठिन था।

तकनीकी सारांश: परिमित पूर्णांक अंतरालों (Finite Integer Intervals) के साथ एक परिमित सेट सिद्धांत के लिए एक निर्णय प्रक्रिया (Decision Procedure)

समस्या विवरण

औपचारिक सत्यापन (Formal Verification) और विश्लेषण के संदर्भ में, स्वचालित तर्क उपकरण (Automated Reasoning Tools) सत्यापन स्थितियों (Verification Conditions) को हल करने के लिए आवश्यक हैं। जबकि सेट थ्योरी पर आधारित मौजूदा उपकरण (जैसे, B, ProB) प्रभावी हैं, वे अक्सर पूर्णांक अंतरालों (Integer Intervals) के साथ परिमित सेटों के विशिष्ट खंडों (Fragments) के लिए निर्णय प्रक्रियाओं (Decision Procedures) की कमी रखते हैं। कार्डिनैलिटी बाधाओं (Cardinality Constraints) के साथ विस्तारित परिमित सेटों का बूलियन बीजगणित (Boolean Algebra), जिसे $L|\cdot|$ द्वारा दर्शाया गया है, निर्णयात्मक (Decidable) है, लेकिन यह स्वाभाविक रूप से उन परिमित पूर्णांक अंतरालों (Ranges) को व्यक्त या तर्क नहीं कर सकता जहाँ सीमाएँ (Limits) अनबाउंड वेरिएबल्स (Unbounded Variables) हो सकती हैं। यह सीमा उन गुणों के स्वचालित सत्यापन में बाधा डालती है जिनमें सेट ऑपरेशन्स जैसे कि सेट का न्यूनतम या अधिकतम खोजना, पूर्णांक थ्रेशोल्ड के आधार पर सेट का विभाजन करना, या अंतराल-आधारित ऐरे डोमेन (Array Domains) के बारे में तर्क करना शामिल है। मुख्य समस्या जो संबोधित की गई है, वह एक क्वांटिफायर-फ्री लॉजिक (Quantifier-free Logic) के भीतर परिमित सेटों, कार्डिनैलिटी बाधाओं और परिमित पूर्णांक अंतरालों (जिसे $L[\ ]$ द्वारा दर्शाया गया है) को एकीकृत करने वाले सिद्धांत की निर्णयात्मकता (Decidability) है।

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

लेखक एक निर्णय प्रक्रिया, SAT $[\ ]$ , प्रस्तावित करते हैं, जो पूर्णांक अंतरालों को संभालने के लिए मौजूदा सॉल्वर SAT $|\cdot|$ (जो $L|\cdot|$ के लिए है) का विस्तार करती है। कार्यप्रणाली एक बेस थ्योरी पर निर्भर करती है जो हेरिटेरीली फाइनाइट सेट्स (Hereditarily Finite Sets) पर आधारित है और इसे कंस्ट्रेंट लॉजिक प्रोग्रामिंग (CLP) भाषा CLP($SET$) और टूल {log} में लागू किया गया है।

प्रमुख तकनीकी घटक:

भाषा विस्तार ( $L[\ ]$ ):
- भाषा को $[k, m]$ के रूप में सेट टर्म्स को शामिल करने के लिए विस्तारित किया गया है, जो सेट $\{p \in \mathbb{Z} \mid k \le p \le m\}$ को दर्शाता है।
- अंतराल सीमाएँ ( $k, m$ ) पूर्णांक रैखिक पद (Integer Linear Terms) हो सकती हैं, जिनमें वेरिएबल्स भी शामिल हैं।
- लॉजिक क्वांटिफायर-फ्री रहता है, जो सेट सदस्यता (Membership), यूनियन, विच्छेद (Disjointness), कार्डिनैलिटी और अंतराल सदस्यता के संबंध में बाधाओं के कंजंक्शन्स और डिसजंक्शन्स का उपयोग करता है।
मुख्य पहचान और रिडक्शन रणनीति (Core Identity and Reduction Strategy):
- केंद्रीय सैद्धांतिक अंतर्दृष्टि यह पहचान है: $k \le m \implies (A = [k, m] \iff A \subseteq [k, m] \land |A| = m - k + 1)$ ।
- यह पहचान प्रक्रिया को उन बाधाओं को रूपांतरित करने की अनुमति देती है जो अंतराल के साथ समानता (Equality) से जुड़ी होती हैं, उन्हें सबसेट संबंधों और कार्डिनैलिटी बाधाओं में बदल देती है।
- सॉल्वर सूत्रों को एक मानक $L|\cdot|$ फॉर्मूला ( $\Phi_{|\cdot|}$ ) और अंतरालों के साथ सबसेट बाधाओं के एक सेट ( $\Phi_{\subseteq[\ ]}$ ) के कंजंक्शन में पुनर्गठित (Rewrite) करता है, जो आमतौर पर $X \subseteq [p, q]$ के रूप में होते हैं जहाँ $X$ एक वेरिएबल है।
SAT $[\ ]$ एल्गोरिदम:
- रीराइट नियम (Rewrite Rules): सॉल्वर सिंटैक्टिक जटिलता को कम करने के लिए रीराइट नियमों (STEPS $[\ ]$ ) का उपयोग करता है। ये नियम अंतरालों वाले समानता, सदस्यता, यूनियन, विच्छेद और कार्डिनैलिटी बाधाओं को संभालते हैं।
- पूर्णांक अंकगणित में रिडक्शन (Reduction to Integer Arithmetic): कई नियम अंतरालों वाले सेट बाधाओं को सीधे लीनियर इंटीजर अरिथमेटिक (LIA) बाधाओं में बदल देते हैं।
- न्यूनतम समाधान जाँच (Minimum Solution Check): जब अपरिवर्तनीय (Irreducible) बाधाएं $X \subseteq [p, q]$ $X \subseteq [p, q]$ के रूप में शेष रहती हैं, तो प्रक्रिया केवल विफल नहीं होती है। इसके बजाय, यह इस गुण का लाभ उठाती है कि यदि कोई फॉर्मूला संतोषजनक (Satisfiable) है, तो उसका एक "न्यूनतम समाधान" (एक ऐसा समाधान जहाँ सेटों की कार्डिनैलिटी न्यूनतम संभव हो) होना चाहिए।
  - सॉल्वर $L|\cdot|$ भाग ( $\Phi_{|\cdot|}$ ) के लिए न्यूनतम समाधान की गणना करता है।
  - फिर यह जाँचता है कि क्या यह न्यूनतम समाधान अंतराल बाधाओं ( $\Phi_{\subseteq[\ ]}$ ) को संतुष्ट करता है।
  - लेखक सिद्ध करते हैं कि यदि कोई न्यूनतम समाधान पूर्ण सूत्र को संतुष्ट नहीं करता है, तो कोई बड़ा समाधान भी उसे संतुष्ट नहीं करेगा, जिससे सूत्र असंतोषजनक (Unsatisfiable) हो जाता है।
{log} में कार्यान्वयन:
- प्रक्रिया को {log} (setlog) में लागू किया गया है, जो एक प्रोलॉग-आधारित टूल है।
- कार्यान्वयन में अंतरालों के लिए वेरिएबल प्रतिस्थापन (Variable Substitutions) को ट्रैक करने के लिए एक मेमोइजिंग स्कीमा (Memoizing Schema) शामिल है, जो अनावश्यक रीराइटिंग को रोकता है और दक्षता में सुधार करता है।
- व्युत्पन्न बाधाओं (जैसे, इंटरसेक्शन, डिफरेंस) को निरंतरता बनाए रखने के लिए प्रिमिटिव बाधाओं के रूप में परिभाषित किया गया है।

प्रमुख योगदान

निर्णयता प्रमाण (Decidability Proof): यह शोध पत्र पहला प्रमाण प्रदान करता है कि कार्डिनैलिटी बाधाओं और परिमित पूर्णांक अंतरालों के साथ विस्तारित परिमित सेटों का बूलियन बीजगणगर ( $L[\ ]$ ) निर्णयात्मक है।
निर्णय प्रक्रिया (Decision Procedure - SAT $[\ ]$ ): एक पूर्ण एल्गोरिदम प्रस्तुत किया गया है जो $L[\ ]$ सूत्रों की संतुष्टि (Satisfiability) को निर्धारित करता है। प्रक्रिया को साउंड (Sound), पूर्ण (Complete) और टर्मिनेटिंग (Terminating) सिद्ध किया गया है।
अंतरालों और सेटों का एकीकरण: उन दृष्टिकोणों के विपरीत जो अंतरालों को एक अलग डोमेन के रूप में मानते हैं या स्थिर सीमाओं की आवश्यकता रखते हैं, यह कार्य वेरिएबल-बाउंडेड पूर्णांक अंतरालों को सेट थ्योरी में सहजता से एकीकृत करता है, जिससे क्वांटिफायर-फ्री लॉजिक में गैर-तुच्छ ऑपरेटरों (जैसे, $i$ -वाँ सबसे छोटा तत्व, थ्रेशोल्ड द्वारा विभाजन) को व्यक्त करना संभव होता है।
कार्यान्वयन और टूलिंग: निर्णय प्रक्रिया को {log} के विस्तार के रूप में लागू किया गया है, जो कंस्ट्रेंट लॉजिक प्रोग्रामिंग भाषा और एक संतुष्टि सॉल्वर (Satisfiability Solver) दोनों के रूप में दोहरी क्षमता प्रदान करता है।

परिणाम और मूल्यांकन

पेपर व्यावहारिक उपयोगिता प्रदर्शित करने के लिए अनुभवजन्य साक्ष्य और एक केस स्टडी प्रस्तुत करता है:

बेंचमार्क मूल्यांकन: 60 $L[\ ]$ सूत्रों का एक सेट, जो पेपर में परिभाषित ऑपरेटरों (जैसे, न्यूनतम, अधिकतम, $i$ -वाँ तत्व) के गुणों का प्रतिनिधित्व करता है, को हल किया गया। {log} ने सभी समस्याओं को औसतन 0.51 सेकंड प्रति समस्या के औसत समय में हल किया, केवल एक समस्या को 5 सेकंड से अधिक समय लगा।
केस स्टडी (एलिवेटर एल्गोरिदम): लेखकों ने एक एलिवेटर कंट्रोल सिस्टम को मॉडल किया जहाँ एलिवेटर को एक विशिष्ट दिशा में अनुरोधों को पूरा करना होता है। मॉडल ने फ्लोर और अनुरोधों को परिभाषित करने के लिए पूर्णांक अंतरालों का उपयोग किया।
- इसमें 7 ऑपरेशन शामिल थे (जैसे, अनुरोध जोड़ना, अगला अनुरोध पूरा करना)।
- {log} का उपयोग 49 इनवेरिएंस लेम्मा (Invariance Lemmas) को स्वतः डिस्चार्ज करने के लिए किया गया (यह सिद्ध करने के लिए कि स्टेट ऑपरेशन्स 7 स्टेट इनवेरिएंट्स को सुरक्षित रखते हैं) और 7 प्रारंभिक अवस्था जाँचों के लिए किया गया।
- सभी प्रमाण एक मानक लैपटॉप पर लगभग 0.5 सेकंड में पूरे हो गए।
- टूल ने सफलतापूर्वक काउंटर-एग्जांपल (Counterexamples) उत्पन्न किए जब इनवेरिएंट्स को जानबूझकर कमजोर किया गया, जिससे इसकी डिबगिंग क्षमताओं का प्रदर्शन हुआ।

महत्व और दावे

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

पेपर इस बात पर जोर देता है कि यह दृष्टिकोण सेट थ्योरी में निहित है, जो इसे अन्य अंतराल तर्क उपकरणों (जैसे, एलन के इंटरवल अलजेब्रा या स्टैटिक एनालिसिस लैटिस पर आधारित उपकरण) से अलग करता है जो अक्सर सामान्य सेट ऑपरेशन्स के साथ अंतरालों को संयोजित करने में असमर्थ होते हैं। {log} फ्रेमवर्क में अंतराल तर्क का एकीकरण उपयोगकर्ताओं को अपने प्रोग्राम और उनके गुणों को सिद्ध करने के लिए एक ही कोड और टूल का उपयोग करने की अनुमति देता है, जो फॉर्मूला और प्रोग्राम की द्वैतता (Duality) का लाभ उठाता है। लेखक विनम्रतापूर्वक नोट करते हैं कि हालांकि यह दृष्टिकोण सामान्य और सुसंगत है, यह विशिष्ट अंतराल-केवल समस्याओं के लिए विशेष सॉल्वरों की तुलना में दक्षता लागत (Efficiency Costs) उठा सकता है, लेकिन यह जटिल हाइब्रिड सेट-इंटरवल संरचनाओं के बारे में तर्क करने की क्षमता के लिए एक ट्रेड-ऑफ है।