💻 computer science

A Modern View on MCSat

यह शोध पत्र मूल ढांचे को परिष्कृत करने और विभिन्न SMT सिद्धांतों में वर्तमान अत्याधुनिक तर्क को कैप्चर करने के लिए Yices2 सॉल्वर के भीतर कार्यान्वयन को औपचारिक रूप देकर, मॉडल कंस्ट्रक्टिंग सैटिस्फिएबिलिटी (MCSat) के लिए एक आधुनिक, सिद्धांत-अज्ञेय (theory-agnostic) प्रमाण प्रणाली प्रस्तुत करता है।

मूल लेखक: Thomas Hader, Theo Jauschneg, Daniela Kaufmann, Laura Kovacs

प्रकाशित 2026-07-08

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

CC BY 4.0

मूल लेखक: Thomas Hader, Theo Jauschneg, Daniela Kaufmann, Laura Kovacs

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

कल्पना कीजिए कि आप एक विशाल, बहु-स्तरीय तर्क पहेली (logic puzzle) को हल करने की कोशिश कर रहे हैं। आपके पास अलग-अलग प्रकार के टुकड़ों का एक बॉक्स है: कुछ सरल "सत्य/असत्य" (True/False) स्विच हैं (जैसे लाइट स्विच), कुछ संख्याएँ हैं जिन्हें जोड़ा या गुणा किया जा सकता है (जैसे एक कैलकुलेटर), और कुछ रहस्यमय काले बक्से (black boxes) हैं जिनमें आप नहीं जानते कि क्या है, केवल यह कि यदि आप एक ही चीज़ अंदर डालेंगे, तो आपको वही चीज़ बाहर मिलेगी।

यह शोध पत्र इस तरह की पहेलियों को हल करने के एक नए, आधुनिक तरीके के बारे में है, जिसे MCSat (मॉडल कंस्ट्रक्टिंग सैटिस्फिएबिलिटी) कहा जाता है। लेखक, जो TU Wien की एक टीम है, मूल रूप से यह कह रहे हैं: "इस पहेली को सुलझाने के तरीके के मूल निर्देश कुछ समय पहले लिखे गए थे। उसके बाद से, जो लोग वास्तव में पहेली सुलझाने वाले सॉफ़्टवेयर (जैसे Yices2 सॉफ़्टवेयर) बना रहे हैं, उन्होंने चीज़ों को थोड़ा अलग तरीके से करना शुरू कर दिया ताकि वे तेज़ हो सकें। हम आधिकारिक नियम पुस्तिका को अपडेट करना चाहते हैं ताकि वह वर्तमान में प्रो खिलाड़ी गेम कैसे खेलते हैं, उससे मेल खा सके।"

यहाँ उनके दृष्टिकोण का सरल उपमाओं (analogies) का उपयोग करके विवरण दिया गया है:

1. पुराना तरीका बनाम नया तरीका

पुराना तरीका (DPLL(T)): एक जासूस की कल्पना करें जो पहले पहेली के "सत्य/असत्य" वाले हिस्से (लाइट स्विच) को हल करता है। एक बार जब वे सेट हो जाते हैं, तो वे शेष संख्या पहेलियों को एक अलग गणित विशेषज्ञ को सौंप देते हैं। यदि गणित विशेषज्ञ कहता है, "अरे, ये संख्याएँ तुम्हारे द्वारा चुने गए स्विचों के साथ काम नहीं करतीं," तो जासूस को वापस जाना पड़ता है, एक स्विच बदलना पड़ता है और फिर से शुरू करना पड़ता है। वे अलग-अलग कमरों में काम करते हैं।

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

2. मुख्य तंत्र: एक "ट्रेल" (Trail) बनाना

लेखक इस प्रक्रिया को एक ट्रेल बनाने के रूप में वर्णित करते हैं। इस ट्रेल को एक पदचिह्न (footprints) के पथ के रूप में सोचें जो आप जंगल (पहेली) में चलते समय छोड़ते हैं।

निर्णय (Decisions): कभी-कभी आपको अनुमान लगाना पड़ता है। आप देखते हैं कि रास्ते में एक मोड़ है और आप कहते हैं, "मैं बाईं ओर जाऊँगा।" शोध पत्र में, इसे Decision कहा जाता है। आप किसी चर (variable) के लिए एक मान चुनते हैं (जैसे $x = 5$ सेट करना) सिर्फ यह देखने के लिए कि यह कहाँ ले जाता है।
प्रसार (Propagations): अन्य समय में, पथ आपको एक निश्चित दिशा में जाने के लिए मजबूर करता है। यदि आप $x = 5$ सेट करते हैं और नियम कहते हैं कि " $x + y = 10$ ," तो $y$ को 5 होना ही होगा। आपने इसे नहीं चुना; गणित ने इसे मजबूर किया। इसे Propagation कहा जाता है।
"एक्सप्लेन" (Explain) फ़ंक्शन (जादुई अनुवादक): यह सबसे महत्वपूर्ण हिस्सा है। यदि आप एक दीवार से टकराते हैं (एक संघर्ष), तो सिस्टम को यह समझाने की आवश्यकता होती है कि क्यों।
- उपमा: कल्पना करें कि आप अपने एक दोस्त के साथ खेल रहे हैं जो एक अलग भाषा बोलता है। आप एक चाल चलते हैं, और वह कहता है, "नहीं, यह अवैध है!" आपको एक अनुवादक की आवश्यकता है। Explain फ़ंक्शन वही अनुवादक है। यह जटिल गणितीय कारण को कि आपकी चाल खराब क्यों थी, एक सरल "नियम" (एक क्लॉज) में अनुवादित करता है जिसे पूरा सिस्टम समझ सके।
- उदाहरण: यदि आपने $x=1$ और $y=1$ सेट करने की कोशिश की लेकिन नियम था " $x \times y \le 0$ ," तो अनुवादक कहता है, "आप दोनों को सकारात्मक नहीं रख सकते।" यह गणितीय संघर्ष को एक तार्किक नियम में बदल देता है: "यदि $x$ सकारात्मक है, तो $y$ सकारात्मक नहीं हो सकता।"

3. "प्लगइन्स" (विशेषज्ञ)

शोध पत्र इस बात पर जोर देता है कि MCSat "थ्योरी-एग्नोस्टिक" (theory-agnostic) है। इसका मतलब है कि मुख्य इंजन को अपने आप में कैलकुलस या तर्क करने की आवश्यकता नहीं है।

उपमा: MCSat इंजन को एक प्रोजेक्ट मैनेजर के रूप में सोचें। प्रोजेक्ट मैनेजर को यह नहीं पता कि लीक होता पाइप कैसे ठीक किया जाए या कोड कैसे लिखा जाए। इसके बजाय, वे प्लगइन्स (विशेषज्ञ ठेकेदार) को काम पर रखते हैं।
- एक प्लगइन प्रपोजिशनल लॉजिक (सत्य/असत्य स्विच) जानता है।
- एक प्लगइन रियल अरिथमेटिक (गणित) जानता है।
- एक प्लगइन अनइंटरप्रिटेड फंक्शन्स (काले बक्से) जानता है।
जब प्रोजेक्ट मैनेजर को कोई चाल चलने की आवश्यकता होती है, तो वे संबंधित प्लगइन से पूछते हैं: "क्या यह चाल संभव है?" यदि प्लगइन कहता है "नहीं," तो वह स्पष्टीकरण (कारण) प्रदान करता है। प्रोजेक्ट मैनेजर फिर उस कारण का उपयोग अपनी योजना को समायोजित करने के लिए करता है।

4. उन्होंने वास्तव में क्या बदला?

यह शोध पत्र एक नई पहेली सुलझाने का तरीका आविष्कार नहीं कर रहा है; यह वास्तविकता के अनुरूप नियम पुस्तिका को अपडेट कर रहा है।

एकीकृत नियम (Unified Rules): पुराने नियम पुस्तिका में, "लॉजिक मूव्स" और "मैथ मूव्स" के लिए अलग-अलग नियम थे। लेखकों ने महसूस किया कि प्रो लोग उन्हें लगभग एक जैसा ही मानते हैं, इसलिए उन्होंने नियमों को एक ही सेट में मिला दिया। यह ऐसा है जैसे यह महसूस करना कि चाहे आप शतरंज का मोहरा चला रहे हों या चेकर्स का, नियम बस यह है कि "इसे खाली स्थान पर ले जाएँ।"
लेजी जस्टिफिकेशन (Lazy Justifications): कभी-कभी, यह गणना करना कि कोई चाल क्यों मजबूर की गई है, बहुत महंगा (जैसे एक जटिल गणना करना) होता है। नया दृष्टिकोण सिस्टम को यह कहने की अनुमति देता है, "हमें पता है कि यह मजबूर है, हम विस्तृत कारण बाद में लिखेंगे यदि हमें वास्तव में इसकी आवश्यकता हुई।" यह समय बचाता है।
"ब्लैक बॉक्स" को संभालना: उन्होंने "अनइंटरप्रेटेड फंक्शन्स" (काले बक्सों) को संभालने के तरीके को परिष्कृत किया। उन्होंने स्पष्ट किया कि इन्हें चरों (variables) की तरह ही माना जाता है, यह सुनिश्चित करते हुए कि यदि आप एक ही इनपुट डालते हैं, तो आपको समान आउटपुट मिलेगा, चाहे कोई भी प्लगइन देख रहा हो।

5. परिणाम

लेखकों ने इस अपडेट की गई नियम पुस्तिका का परीक्षण करने के लिए Yices2 सॉल्वर (एक वास्तविक दुनिया का पहेली सुलझाने वाला सॉफ़्टवेयर जिसका उपयोग पेशेवरों द्वारा किया जाता है) को देखा। उन्होंने दिखाया कि उनके नए, सरल नियमों का सेट पूरी तरह से बताता है कि Yices2 कैसे काम करता है।

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

वे यह दावा नहीं करते हैं कि इससे बीमारियाँ ठीक होंगी या शेयर बाजार की भविष्यवाणी की जा सकेगी। वे केवल यह दावा करते हैं कि सैद्धांतिक विवरण को वर्तमान सॉफ़्टवेयर कार्यान्वयन से मिलाने के लिए अपडेट करके, अब हमारे पास इन शक्तिशाली तर्क मशीनों के काम करने के तरीके की अधिक स्पष्ट और सटीक समझ है।

तकनीकी सारांश: MCSat पर एक आधुनिक दृष्टिकोण

समस्या विवरण

मॉडल कंस्ट्रक्टिंग सैटिस्फिएबिलिटी (MCSat) कैलकुलस, सैटिस्फिएबिलिटी मोड्यूलो थ्योरीज (SMT) समस्याओं को हल करने के लिए एक अत्याधुनिक दृष्टिकोण के रूप में उभरा है, विशेष रूप से जटिल बीजगणितीय सिद्धांतों जैसे कि नॉन-लीनियर रियल अरिथमेटिक (NRA) में। हालांकि इसे मूल रूप से NLSAT के रूप में विकसित किया गया था और बाद में MCSat के रूप में औपचारिक रूप दिया गया था, वर्तमान उच्च-प्रदर्शन कार्यान्वयन (विशेष रूप से Yices2 सॉल्वर में) मूल साहित्य में पाए जाने वाले मौलिक औपचारिक प्रस्तुतीकरणों से काफी अलग हो गए हैं। यह विचलन उन शोधकर्ताओं और अभ्यासकर्ताओं के लिए एक बाधा उत्पन्न करता है जो वर्तमान अत्याधुनिक प्रक्रियाओं को समझने का प्रयास कर रहे हैं। यह शोध पत्र एक एकीकृत, आधुनिक प्रमाण प्रणाली (proof system) की आवश्यकता को संबोधित करता है जो इन कार्यान्वयन वास्तविकताओं को सटीक रूप से दर्शाती है और साथ ही एक कठोर सैद्धांतिक आधार बनाए रखती है।

कार्यप्रणाली

लेखक एक संशोधित, थ्योरी-एग्नोस्टिक (सिद्धांत-निरपेक्ष) MCSat फ्रेमवर्क प्रस्तावित करते हैं जो एक प्रमाण प्रणाली के रूप में कार्य करता है। कार्यप्रणाली में शामिल है:

कार्यान्वयन का औपचारिकीकरण: फ्रेमवर्क को Yices2 SMT सॉल्वर के भीतर डिजाइन निर्णयों को बारीकी से औपचारिक रूप देकर व्युत्पन्न किया गया है। यह मूल सैद्धांतिक शोध पत्रों और व्यावहारिक, उच्च-प्रदर्शन सॉल्वरों के बीच के अंतर को पाटता है।
एकीकृत खोज स्कीमा (Unified Search Schema): पारंपरिक DPLL(T) दृष्टिकोणों के विपरीत, जो प्रपोजिशनल रीजनिंग को थ्योरी रीजनिंग से अलग करते हैं, या प्रारंभिक MCSat स्वरूपों के विपरीत, जो प्रपोजिशनल लिटरल और थ्योरी वेरिएबल्स के बीच अंतर करते हैं, यह कार्य स्वैच्छिक टर्म असाइनमेंट (arbitrary term assignments) पर एक खोज स्कीमा को परिभाषित करता है। यह Boolean और थ्योरी-विशिष्ट तर्क दोनों को संभालने के लिए नियमों के एक एकल सेट की अनुमति देता है।
थ्योरी प्लगइन्स और स्पष्टीकरण (Explanations): सिस्टम थ्योरी प्लगइन्स पर निर्भर करता है जो एक सामान्य MCSat कोर के साथ इंटरैक्ट करते हैं। ये प्लगइन्स निम्नलिखित के लिए जिम्मेदार हैं:
- व्याख्याित टर्म्स के लिए मूल्यांकन फंक्शन (eval) प्रदान करना।
- अनइंटरप्रिटेड फंक्शन्स के लिए कॉंग्रुएंस (congruence) सुनिश्चित करना।
- संघर्ष (conflicts) उत्पन्न होने या मानों के प्रसार (propagation) के दौरान स्पष्टीकरण (लेम्मा क्लॉज) उत्पन्न करना।
- स्पष्टीकरण फंक्शन को सार्वभौमिक वैधता के बजाय केवल खोज समस्या के संबंध में वैधता ( $\phi \models E$ ) की आवश्यकता के साथ शिथिल किया गया है, जिससे अधिक लचीला और कार्यान्वयन-अनुकूल संघर्ष विश्लेषण संभव होता है।
नियम-आधारित कैलकुलस: खोज को एक "ट्रेल" (टर्म असाइनमेंट का एक अनुक्रम) और एक क्लॉज डेटाबेस पर संचालित होने वाले ट्रांजिशन सिस्टम के रूप में परिभाषित किया गया है। सिस्टम मानक SAT-जैसे ऑपरेशन्स (Decide, Propagate, Conflict, Resolve, Learn) का उपयोग करता है, जिन्हें स्वैच्छिक सॉर्ट्स (arbitrary sorts) और थ्योरी बाधाओं को संभालने के लिए विस्तारित किया गया है।

मुख्य योगदान

शोध पत्र MCSat औपचारिकता में कई विशिष्ट सुधार और योगदान प्रस्तुत करता है:

सामान्य नियम योजना (General Rule Scheme): एक संक्षिप्त, थ्योरी-एग्नोस्टिक नियम सेट प्रस्तुत किया गया है जो Boolean और थ्योरी रीजनिंग को एकीकृत करता है। यह प्रपोजिशनल और थ्योरी वेरिएबल्स के लिए अलग-अलग नियम सेटों की आवश्यकता को समाप्त करता है, जिससे कैलकुलस सरल हो जाता है।
परिष्कृत परिभाषाएं:
- टर्म असाइनमेंट: फ्रेमवर्क "थ्योरी वेरिएबल्स" को मान असाइन करने के बजाय स्वैच्छिक टर्म्स को मान असाइन करने की ओर स्थानांतरित होता है, जो SMT-LIB परिभाषाओं के अनुरूप है और अनइंटरप्रेटेड फंक्शन्स को अधिक स्वाभाविक रूप से समर्थन देता है।
- स्पष्टीकरण फंक्शन: स्पष्टीकरण की आवश्यकता को सार्वभौमिक रूप से वैध लेम्मा होने के बजाय विशिष्ट खोज समस्या के संदर्भ में वैध होने के रूप में कमजोर किया गया है। यह असंतोषजनकता (unsatisfiability) के मामलों में खाली क्लॉज (empty clauses) की अनुमति देता है और Boolean संघर्षों को बेहतर ढंग से समायोजित करता है।
- प्रसार और औचित्य (Propagation and Justification): पेपर थ्योरी वैल्यूज (न केवल Boolean लिटरल) के प्रसार को औपचारिक रूप देता है और Learn-Justification नियम पेश करता है। यह सिस्टम को मांग पर (on demand/lazily) प्रसार के औचित्य सीखने की अनुमति देता है, जो उन सिद्धांतों के लिए महत्वपूर्ण है जहाँ औचित्य उत्पन्न करना गणनात्मक रूप से महंगा होता है।
ठोस इंस्टांशिएशन (Concrete Instantiations): लेखक कई सिद्धांतों के लिए सामान्य कैलकुलस को इंस्टांशिएट करते हैं, जिनमें शामिल हैं:
- प्रपोजिशनल लॉजिक: इसे Boolean बाधाओं को संभालने वाले एक नेटिव प्लगइन के रूप में माना जाता है।
- नॉन-लीनर रियल अरिथमेटिक: साइलिंड्रिकल अलब्रािक डिकंपोजिशन (CAD) पर आधारित, जो स्पष्टीकरणों के लिए एक परिमित आधार (finite basis) सुनिश्चित करने के लिए साइन-इनवेरिएंट क्षेत्रों का उपयोग करता है।
- अनइंटरप्रेटेड फंक्शन्स (UF): संघर्षों और प्रसार का पता लगाने के लिए इक्वैलिटी ग्राफ्स (e-graphs) के माध्यम से कार्यान्वित।
- अन्य सिद्धांत: फ्रेमवर्क को लीनियर/नॉन-लीनियर इंटीजर्स, फिक्स्ड-साइज़ बिट-वेक्टर्स और फाइनाइट फील्ड्स का समर्थन करने के लिए नोट किया गया है।

परिणाम और उदाहरण

पेपर कैलकुलस को क्रियान्वित दिखाने के लिए प्रपोजिशनल लॉजिक और रियल अरिथमेटिक के मिश्रण वाला एक विस्तृत "रनिंग एक्जाम्पल" प्रदान करता है। उदाहरण निम्नलिखित को प्रदर्शित करता है:

निर्णय लेना (Decision Making): अनअसाइंड टर्म्स के लिए मान चुनना (जैसे, $x \mapsto 2$ तय करना)।
प्रसार (Propagation): यूनिट क्लॉज और थ्योरी बाधाओं के आधार पर मजबूर मान प्राप्त करना (जैसे, अरिथमेटिक बाधाओं के आधार पर $y \mapsto -1$ को प्रसारित करना)।
संघर्ष विश्लेषण (Conflict Analysis): विसंगतियों का पता लगाना (जैसे, $x \approx 7y$ और $x \approx -7$ के बीच एक संघर्ष), रेजोल्यूशन के माध्यम से संघर्ष क्लॉज उत्पन्न करना, और पिछले निर्णय स्तरों पर बैकजंपिंग करना।
सीखना (Learning): एक ही संघर्ष को दोबारा आने से रोकने के लिए डेटाबेस में रिजोलवेंट क्लॉज जोड़ना।

पेपर दावा करता है कि कैलकुलस सत्य और पूर्ण (sound and complete) है, जिसका अर्थ है कि यदि कोई मॉडल मौजूद है तो यह sat अवस्था में समाप्त होगा, या यदि फॉर्मूला विरोधाभासी है तो unsat में, बशर्ते कि स्पष्टीकरण फंक्शन 'फाइनाइट बेसिस' की आवश्यकता को पूरा करता हो (एक शर्त जिसे प्रदर्शन के लिए Yices2 जैसे व्यावहारिक कार्यान्वयन में शिथिल किया गया है)।

महत्व और दावे

लेखक का दावा है कि यह कार्य एक आधुनिक परिप्रेक्ष्य प्रदान करता है जो मूल MCSat स्वरूप को परिष्कृत करता है। इसका महत्व यहाँ है:

सिद्धांत और व्यवहार को जोड़ना: यह Yices2 से उन डिजाइन निर्णयों को शामिल करके MCSat-आधारित SMT रीजनिंग के वर्तमान अत्याधुनिक स्तर को कैप्चर करता है जो पहले के औपचारिक स्वरूपों में अनुपस्थित थे।
सुलभता: एक संक्षिप्त, उदाहरण-संचालित प्रस्तुति प्रदान करके, पेपर का लक्ष्य जटिल आधुनिक MCSat मशीनरी को नए पाठकों के लिए सुलभ बनाना है जबकि विशेषज्ञों के लिए परिचित बनाए रखना है।
एकीकरण: यह Boolean और थ्योरी रीजनिंग के बीच के संबंध को स्पष्ट करता है, यह दिखाते हुए कि उन्हें अलग-अलग तंत्रों के बजाय एक एकल, सुसंगत सेट के नियमों द्वारा संभाला जा सकता है।

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