संतुष्टि मॉड्यूलो सिद्धांत

From Vigyanwiki
Revision as of 22:16, 7 August 2023 by alpha>Adityak

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

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

मूल शब्दावली

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

अधिकांश एसएमटी सॉल्वर अपने तर्कों के केवल क्वांटिफायर-मुक्त अंशों का समर्थन करते हैं।

अभिव्यंजक घात

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

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

कन्सट्रैन्ट लॉजिक प्रोग्रामिंग रैखिक अंकगणितीय बाधाओं के लिए समर्थन प्रदान करती है, लेकिन एक पूरी तरह से अलग सैद्धांतिक ढांचे के भीतर। उच्च-क्रम तर्क में सूत्रों को हल करने के लिए एसएमटी सॉल्वरों को भी बढ़ाया गया है।[1]

सॉल्वर दृष्टिकोण

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

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

अनिर्णीत सिद्धांतों के लिए एसएमटी

अधिकांश सामान्य एसएमटी दृष्टिकोण निर्णायक सिद्धांतों का समर्थन करते हैं। हालाँकि, कई वास्तविक दुनिया प्रणालियाँ, जैसे कि एक विमान और उसका व्यवहार, केवल पारमार्थिक फंक्शन से जुड़े वास्तविक संख्याओं पर गैर-रैखिक अंकगणित के माध्यम से मॉडलिंग की जा सकती हैं। यह तथ्य एसएमटी समस्या के गैर-रेखीय सिद्धांतों तक विस्तार को प्रेरित करता है, जैसे यह निर्धारित करना कि क्या निम्नलिखित समीकरण संतोषजनक है:

जहाँ

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

वास्तविकताओं पर अनिर्णीत अंकगणितीय सिद्धांतों से सिद्धांत परमाणुओं के बूलियन संयोजनों को संबोधित करने वाले एसएमटी सॉल्वर के उदाहरण एबीएसॉल्वर हैं,[3] जो एक गैर-रेखीय अनुकूलन पैकेट के साथ एक शास्त्रीय डीपीएलएल (टी) आर्किटेक्चर को (आवश्यक रूप से अपूर्ण) अधीनस्थ सिद्धांत सॉल्वर और आईएसएटी के रूप में नियोजित करता है। , डीपीएलएल एसएटी-समाधान और अंतराल बाधा प्रसार के एकीकरण पर निर्माण, जिसे आईएसएटी एल्गोरिदम कहा जाता है।[4]

सॉल्वर

नीचे दी गई तालिका कई उपलब्ध एसएमटी सॉल्वरों की कुछ विशेषताओं का सारांश प्रस्तुत करती है। कॉलम "एसएमटी-LIB" एसएमटी-LIB भाषा के साथ अनुकूलता दर्शाता है; 'हाँ' चिह्नित कई प्रणालियाँ केवल एसएमटी-LIB के पुराने संस्करणों का समर्थन कर सकती हैं, या भाषा के लिए केवल आंशिक समर्थन प्रदान कर सकती हैं। कॉलम "सीवीसी" सीवीसी भाषा के लिए समर्थन दर्शाता है। कॉलम "DIMACS" DIMACS प्रारूप के लिए समर्थन दर्शाता है।

परियोजनाएं न केवल सुविधाओं और प्रदर्शन में भिन्न होती हैं, बल्कि आसपास के समुदाय की व्यवहार्यता, परियोजना में इसकी चल रही रुचि और दस्तावेज़ीकरण, सुधार, परीक्षण और संवर्द्धन में योगदान करने की क्षमता में भी भिन्न होती हैं।


परियोजनाएं न केवल सुविधाओं और प्रदर्शन में भिन्न होती हैं, बल्कि आसपास के समुदाय की व्यवहार्यता, परियोजना में इसकी चल रही रुचि और दस्तावेज़ीकरण, सुधार, परीक्षण और संवर्द्धन में योगदान करने की क्षमता में भी भिन्न होती हैं।

प्लैटफ़ॉर्म विशेषताएँ टिप्पणियाँ
नाम ओएस लाइसेंस श्रीमती-एलआईबी सीवीसी DIMACS अंतर्निहित सिद्धांत एपीआई श्रीमती-COMP [1]
एबी सॉल्वर लिनक्स सीपीएल v1.2 नहीं हाँ रैखिक अंकगणित, अरेखीय अंकगणित सी++ नहीं डीपीएलएल-आधारित
ऑल्ट-एर्गो लिनक्स , मैक ओएस , विंडोज़ CeCILL-C (लगभग एलजीपीएल के बराबर ) आंशिक v1.2 और v2.0 नहीं नहीं खाली सिद्धांत , रैखिक पूर्णांक और तर्कसंगत अंकगणित, गैर-रेखीय अंकगणित, बहुरूपी सरणियाँ , प्रगणित डेटा प्रकार , एसी प्रतीक , बिटवेक्टर , रिकॉर्ड डेटा प्रकार , क्वांटिफायर ओकैमल 2008 पॉलिमॉर्फिक प्रथम-क्रम इनपुट भाषा आ ला एमएल, एसएटी-सॉल्वर आधारित, मॉड्यूलो सिद्धांतों के तर्क के लिए शोस्ताक-जैसे और नेल्सन-ओपेन जैसे दृष्टिकोणों को जोड़ती है।
Barcelogic लिनक्स संपदा v1.2 खोखला सिद्धांत , अंतर तर्क सी++ 2009 डीपीएलएल-आधारित, सर्वांगसमता समापन
ऊदबिलाव लिनक्स , विंडोज़ बीएसडी v1.2 नहीं नहीं बिटवेक्टर ओकैमल 2009 SAT-सॉल्वर आधारित
बूलेक्टर लिनक्स एमआईटी v1.2 नहीं नहीं बिटवेक्टर , सरणियाँ सी 2009 SAT-सॉल्वर आधारित
सीवीसी3 लिनक्स बीएसडी v1.2 हाँ खाली सिद्धांत , रैखिक अंकगणित, सरणियाँ, टुपल्स, प्रकार, रिकॉर्ड, बिटवेक्टर, क्वांटिफायर सी / सी++ 2010 HOL को प्रूफ़ आउटपुट
सीवीसी4 लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी बीएसडी हाँ हाँ तर्कसंगत और पूर्णांक रैखिक अंकगणित, सरणियाँ, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, और अबाधित फ़ंक्शन प्रतीकों पर समानता सी++ 2021 संस्करण 1.8 मई 2021 में जारी किया गया
सीवीसी5 लिनक्स , मैक ओएस , विंडोज़ बीएसडी हाँ हाँ तर्कसंगत और पूर्णांक रैखिक अंकगणित, सरणियाँ, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, अनुक्रम, बैग, और अबाधित फ़ंक्शन प्रतीकों पर समानता सी++, पायथन, जावा 2021 संस्करण 1.0 अप्रैल 2022 में जारी किया गया
निर्णय प्रक्रिया टूलकिट (डीपीटी) लिनक्स अमरीका की एक मूल जनजाति नहीं ओकैमल नहीं डीपीएलएल-आधारित
iSAT लिनक्स संपदा नहीं अरेखीय अंकगणित नहीं डीपीएलएल-आधारित
मैथसैट लिनक्स , मैक ओएस , विंडोज़ संपदा हाँ हाँ खाली सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, सरणियाँ सी / सी++ , पायथन , जावा 2010 डीपीएलएल-आधारित
मिनीश्रीमती लिनक्स एलजीपीएल आंशिक v2.0 अरेखीय अंकगणित ओकैमल 2010 SAT-सॉल्वर आधारित, Yices-आधारित
उत्तरी स्ट्रिंग बाधाओं के लिए एसएमटी सॉल्वर
ओपनकोग लिनक्स एजीपीएल नहीं नहीं नहीं संभाव्य तर्क , अंकगणित। संबंधपरक मॉडल सी++ , स्कीम , पायथन नहीं सबग्राफ समरूपता
ओपनएसएमटी लिनक्स , मैक ओएस , विंडोज़ जीपीएलवी3 आंशिक v2.0 हाँ खाली सिद्धांत , अंतर, रैखिक अंकगणित, बिटवेक्टर सी++ 2011 आलसी श्रीमती सॉल्वर
raSAT लिनक्स जीपीएलवी3 v2.0 वास्तविक और पूर्णांक अरेखीय अंकगणित 2014, 2015 परीक्षण और मध्यवर्ती मूल्य प्रमेय के साथ अंतराल बाधा प्रसार का विस्तार
साटिन ? संपदा v1.2 रैखिक अंकगणित, अंतर तर्क कोई नहीं 2009
एसएमटीइंटरपोल लिनक्स , मैक ओएस , विंडोज़ LGPLv3 v2.5 अव्याख्यायित फलन, रैखिक वास्तविक अंकगणित, और रैखिक पूर्णांक अंकगणित जावा 2012 उच्च गुणवत्ता, कॉम्पैक्ट इंटरपोलेंट उत्पन्न करने पर ध्यान केंद्रित करता है।
एसएमसीएचआर लिनक्स , मैक ओएस , विंडोज़ जीपीएलवी3 नहीं नहीं नहीं रैखिक अंकगणित, अरेखीय अंकगणित, ढेर सी नहीं बाधा प्रबंधन नियमों का उपयोग करके नए सिद्धांतों को लागू कर सकते हैं ।
श्रीमती-चूहा लिनक्स , मैक ओएस एमआईटी v2.0 नहीं नहीं रैखिक अंकगणित, अरेखीय अंकगणित सी++ 2015 रणनीतिक और समानांतर एसएमटी समाधान के लिए टूलबॉक्स जिसमें एसएमटी अनुरूप कार्यान्वयन का संग्रह शामिल है।
सोनोलर लिनक्स , विंडोज़ संपदा आंशिक v2.0 बिटवेक्टर सी 2010 SAT-सॉल्वर आधारित
भाला लिनक्स , मैक ओएस , विंडोज़ संपदा v1.2 बिटवेक्टर 2008
एसटीपी लिनक्स , ओपनबीएसडी , विंडोज , मैक ओएस एमआईटी आंशिक v2.0 हाँ नहीं बिटवेक्टर, सरणियाँ सी , सी++ , पायथन , ओकैमल , जावा 2011 SAT-सॉल्वर आधारित
तलवार लिनक्स संपदा v1.2 बिटवेक्टर 2009
यूसीएलआईडी लिनक्स बीएसडी नहीं नहीं नहीं खाली सिद्धांत , रैखिक अंकगणित, बिटवेक्टर, और विवश लैम्ब्डा (सरणी, यादें, कैश, आदि) नहीं एसएटी-सॉल्वर आधारित, मॉस्को एमएल में लिखा गया । इनपुट भाषा एसएमवी मॉडल चेकर है। अच्छी तरह से प्रलेखित!
veriT लिनक्स , ओएस एक्स बीएसडी आंशिक v2.0 खाली सिद्धांत , तर्कसंगत और पूर्णांक रैखिक अंकगणित, परिमाणक, और अबाधित फ़ंक्शन प्रतीकों पर समानता सी / सी++ 2010 एसएटी-सॉल्वर आधारित, सबूत पेश कर सकता है
हाँ लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी जीपीएलवी3 v2.0 नहीं हाँ तर्कसंगत और पूर्णांक रैखिक अंकगणित, बिटवेक्टर, सरणियाँ, और अबाधित फ़ंक्शन प्रतीकों पर समानता सी 2014 स्रोत कोड ऑनलाइन उपलब्ध है
Z3 प्रमेय कहावत लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी एमआईटी v2.0 हाँ खाली सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, सरणियाँ, डेटाटाइप, क्वांटिफायर , स्ट्रिंग्स सी / सी++ , .NET , ओकैमल , पायथन , जावा , हास्केल 2011 स्रोत कोड ऑनलाइन उपलब्ध है

मानकीकरण और SMT-COMP सॉल्वर प्रतियोगिता

प्लेटफ़ॉर्म विशेषताएँ टिप्पणियाँ
नाम ओएस लाइसेंस एसएमटी-एलआईबी सीवीसी डायमैक अंतर्निर्मित सिद्धांत एपीआई एसएमटी-कॉम्प[1]
एबीसॉल्वर लिनक्स CPL v1.2 No Yes रैखिक अंकगणित, अरेखीय अंकगणित C++ no DPLL-based
ऑल्ट-एर्गो लिनक्स , मैक ओएस , विंडोज़ CeCILL-C (roughly equivalent to LGPL) partial v1.2 and v2.0 No No खाली सिद्धांत , रैखिक पूर्णांक और तर्कसंगत अंकगणित, गैर-रेखीय अंकगणित, बहुरूपी सरणियाँ , प्रगणित डेटा प्रकार , एसी प्रतीक , बिटवेक्टर , रिकॉर्ड डेटा प्रकार , क्वांटिफायर OCaml 2008 बहुरूपी प्रथम-क्रम इनपुट भाषा आ ला एमएल, एसएटी-सॉल्वर आधारित, तर्क मॉड्यूल सिद्धांतों के लिए शोस्ताक-जैसे और नेल्सन-ओपेन जैसे दृष्टिकोणों को जोड़ती है
बार्सेलॉजिक लिनक्स Proprietary v1.2 खोखला सिद्धांत , अंतर तर्क C++ 2009 DPLL-based, congruence closure
बीवर लिनक्स , विंडोज़ BSD v1.2 No No बिटवेक्टर OCaml 2009 SAT-solver based
बूलेक्टर लिनक्स MIT v1.2 No No बिटवेक्टर , सरणियाँ C 2009 SAT-solver based
सीवीसी3 लिनक्स BSD v1.2 Yes खाली सिद्धांत , रैखिक अंकगणित, सरणियाँ, टुपल्स, प्रकार, रिकॉर्ड, बिटवेक्टर, क्वांटिफायर C/C++ 2010 proof output to HOL
सीवीसी4 लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी BSD Yes Yes तर्कसंगत और पूर्णांक रैखिक अंकगणित, सरणियाँ, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, और अबाधित फ़ंक्शन प्रतीकों पर समानता C++ 2021 version 1.8 released May 2021
सीवीसी5 लिनक्स , मैक ओएस , विंडोज़ BSD Yes Yes तर्कसंगत और पूर्णांक रैखिक अंकगणित, सरणियाँ, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, अनुक्रम, बैग, और अबाधित फ़ंक्शन प्रतीकों पर समानता C++, Python, Java 2021 version 1.0 released April 2022
निर्णय प्रक्रिया टूलकिट (डीपीटी) लिनक्स Apache No OCaml no DPLL-based
आईसैट (iSAT) लिनक्स Proprietary No अरेखीय अंकगणित no DPLL-based
मैथसैट लिनक्स , मैक ओएस , विंडोज़ Proprietary Yes Yes खाली सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, सरणियाँ C/C++, Python, Java 2010 DPLL-based
MiniSmt लिनक्स LGPL partial v2.0 अरेखीय अंकगणित OCaml 2010 SAT-solver based, Yices-based
Norn SMT solver for string constraints
लिनक्स
OpenCog लिनक्स AGPL No No No संभाव्य तर्क , अंकगणित। संबंधपरक मॉडल C++, Scheme, Python no subgraph isomorphism
OpenSMT लिनक्स , मैक ओएस , विंडोज़ GPLv3 partial v2.0 Yes खाली सिद्धांत , अंतर, रैखिक अंकगणित, बिटवेक्टर C++ 2011 lazy SMT Solver
raSAT लिनक्स GPLv3 v2.0 वास्तविक और पूर्णांक अरेखीय अंकगणित 2014, 2015 extension of the Interval Constraint Propagation with Testing and the Intermediate Value Theorem
SatEEn ? Proprietary v1.2 रैखिक अंकगणित, अंतर तर्क none 2009
SMTInterpol लिनक्स , मैक ओएस , विंडोज़ LGPLv3 v2.5 अव्याख्यायित फलन, रैखिक वास्तविक अंकगणित, और रैखिक पूर्णांक अंकगणित Java 2012 Focuses on generating high quality, compact interpolants.
SMCHR लिनक्स , मैक ओएस , विंडोज़ GPLv3 No No No रैखिक अंकगणित, अरेखीय अंकगणित, ढेर C no Can implement new theories using Constraint Handling Rules.
एसएमटी-RAT लिनक्स , मैक ओएस MIT v2.0 No No रैखिक अंकगणित, अरेखीय अंकगणित C++ 2015 Toolbox for strategic and parallel एसएमटी solving consisting of a collection of एसएमटी compliant implementations.
SONOLAR लिनक्स , विंडोज़ Proprietary partial v2.0 बिटवेक्टर C 2010 SAT-solver based
Spear लिनक्स , मैक ओएस , विंडोज़ Proprietary v1.2 बिटवेक्टर 2008
एसटीपी लिनक्स , ओपनबीएसडी , विंडोज , मैक ओएस MIT partial v2.0 Yes No बिटवेक्टर, सरणियाँ C, C++, Python, OCaml, Java 2011 SAT-solver based
SWORD लिनक्स Proprietary v1.2 बिटवेक्टर 2009
UCLID लिनक्स BSD No No No खाली सिद्धांत , रैखिक अंकगणित, बिटवेक्टर, और विवश लैम्ब्डा (सरणी, यादें, कैश, आदि) no SAT-solver based, written in Moscow ML. Input language is SMV model checker. Well-documented!
veriT लिनक्स , ओएस एक्स BSD partial v2.0 खाली सिद्धांत , तर्कसंगत और पूर्णांक रैखिक अंकगणित, परिमाणक, और अबाधित फ़ंक्शन प्रतीकों पर समानता C/C++ 2010 SAT-solver based, can produce proofs
Yices लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी GPLv3 v2.0 No Yes तर्कसंगत और पूर्णांक रैखिक अंकगणित, बिटवेक्टर, सरणियाँ, और अबाधित फ़ंक्शन प्रतीकों पर समानता C 2014 Source code is available online
Z3 Theorem Prover लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी MIT v2.0 Yes खाली सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, सरणियाँ, डेटाटाइप, क्वांटिफायर , स्ट्रिंग्स C/C++, .NET, OCaml, Python, Java, Haskell 2011 Source code is available online

मानकीकरण और एसएमटी-COMP सॉल्वर प्रतियोगिता

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

एसएमटी-LIB प्रारूप भी कई मानकीकृत बेंचमार्क के साथ आता है और इसने एसएमटी-COMP नामक एसएमटी सॉल्वरों के बीच एक वार्षिक प्रतियोगिता को सक्षम किया है। प्रारंभ में, प्रतियोगिता कंप्यूटर एडेड सत्यापन सम्मेलन (सीएवी) के दौरान हुई थी,[5][6] लेकिन 2020 तक प्रतियोगिता को एसएमटी कार्यशाला के हिस्से के रूप में आयोजित किया गया है, जो स्वचालित तर्क (आईजेसीएआर) पर अंतर्राष्ट्रीय संयुक्त सम्मेलन से संबद्ध है)।[7]

अनुप्रयोग

एसएमटी सॉल्वर सत्यापन, प्रोग्राम की यथार्थता सिद्ध करने, प्रतीकात्मक निष्पादन के आधार पर सॉफ्टवेयर परीक्षण, और संश्लेषण के लिए, संभावित प्रोग्रमम के स्थान पर सर्च करके प्रोग्रम के भाग उत्पन्न करने के लिए उपयोगी हैं। सॉफ़्टवेयर सत्यापन के अलावा, एसएमटी सॉल्वरों का उपयोग प्रकार के अनुमान के लिए भी किया गया है[8][9] और परमाणु उपकरण नियंत्रण में साधक के विश्वासों को मॉडलिंग करने सहित सैद्धांतिक परिदृश्यों के मॉडलिंग के लिए भी है।[10]

सत्यापन

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

Z3 एसएमटी सॉल्वर के शीर्ष पर कई सत्यापनकर्ता बनाए गए हैं। बूगी एक मध्यवर्ती सत्यापन भाषा है जो सरल अनिवार्य कार्यक्रमों की स्वचालित रूप से जाँच करने के लिए Z3 का उपयोग करती है। समवर्ती सी के लिए वीसीसी सत्यापनकर्ता बूगी का उपयोग करता है, साथ ही अनिवार्य वस्तु-आधारित कार्यक्रमों के लिए डैफनी, समवर्ती कार्यक्रमों के लिए चालिस और सी# के लिए स्पेक# का उपयोग करता है। F* एक निर्भरता से टाइप की जाने वाली भाषा है जो प्रमाण खोजने के लिए Z3 का उपयोग करती है; कंपाइलर इन सबूतों को प्रूफ-ले जाने वाले बाइटकोड का उत्पादन करने के लिए ले जाता है। वाइपर सत्यापन अवसंरचना सत्यापन शर्तों को Z3 में एनकोड करती है। एसबीवी लाइब्रेरी हास्केल कार्यक्रमों का एसएमटी-आधारित सत्यापन प्रदान करती है, और उपयोगकर्ता को Z3, एबीसी, बूलेक्टर, सीवीसी5, मैथसैट और येस जैसे कई सॉल्वरों में से चुनने की सुविधा देती है।

  • ऑल्ट-एर्गो एसएमटी सॉल्वर के ऊपर कई सत्यापनकर्ता भी बनाए गए हैं। यहां परिपक्व आवेदनों की सूची दी गई है:
  • व्हाय3, डिडक्टिव प्रोग्राम सत्यापन के लिए एक मंच, ऑल्ट-एर्गो को अपने मुख्य कहावत के रूप में उपयोग करता है;
  • कैविएट, सीईए द्वारा विकसित और एयरबस द्वारा उपयोग किया जाने वाला एक सी-सत्यापनकर्ता; ऑल्ट-एर्गो को इसके हालिया विमानों में से एक की योग्यता DO-178C में शामिल किया गया था;
  • फ्रैमा-सी, सी-कोड का विश्लेषण करने के लिए एक ढांचा, जेसी और डब्ल्यूपी प्लगइन्स ("डिडक्टिव प्रोग्राम वेरिफिकेशन" के लिए समर्पित) में ऑल्ट-एर्गो का उपयोग करता है;
  • स्पार्क 2014 में कुछ दावों के सत्यापन को स्वचालित करने के लिए स्पार्क CVC4 और ऑल्ट-एर्गो (GNATprove के पीछे) का उपयोग करता है;
  • एटेलियर-बी अपने मुख्य प्रोवर के बजाय ऑल्ट-एर्गो का उपयोग कर सकता है (एएनआर बीवेयर प्रोजेक्ट बेंचमार्क पर सफलता 84% से बढ़कर 98% हो गई है);
  • रॉडिन, सिस्टरेल द्वारा विकसित एक बी-मेथड फ्रेमवर्क, ऑल्ट-एर्गो को बैक-एंड के रूप में उपयोग कर सकता है;
  • क्यूबिकल, सरणी-आधारित संक्रमण प्रणालियों की सुरक्षा गुणों की पुष्टि के लिए एक खुला स्रोत मॉडल चेकर।
  • ईज़ीक्रिप्ट, प्रतिकूल कोड के साथ संभाव्य संगणनाओं के संबंधपरक गुणों के बारे में तर्क करने के लिए एक टूलसेट।

कई एसएमटी सॉल्वर SMTLIB2 नामक एक सामान्य इंटरफ़ेस प्रारूप लागू करते हैं (ऐसी फ़ाइलों में आमतौर पर एक्सटेंशन ".smt2" होता है)।  लिक्विडहास्केल उपकरण हास्केल के लिए एक परिशोधन प्रकार-आधारित सत्यापनकर्ता लागू करता है जो किसी भी SMTLIB2 अनुरूप सॉल्वर का उपयोग कर सकता है, जैसे cvc5, MathSat, या Z3।

सांकेतिक-निष्पादन आधारित विश्लेषण एवं परीक्षण

एसएमटी सॉल्वरों का एक महत्वपूर्ण एप्लीकेशन प्रोग्राम के विश्लेषण और परीक्षण के लिए प्रतीकात्मक निष्पादन है (उदाहरण के लिए, कॉन्कोलिक परीक्षण), जिसका उद्देश्य विशेष रूप से सुरक्षा कमजोरियों का पता लगाना है। इस श्रेणी के उदाहरण टूल में माइक्रोसॉफ्ट रिसर्च से SAGE, KLEE, S2E और ट्राइटनशामिल हैं। एसएमटी सॉल्वर जिनका उपयोग प्रतीकात्मक-निष्पादन अनुप्रयोगों के लिए किया गया है, उनमें Z3, एसटीपी आर्काइव्ड 2015-04-06 वेबैक मशीन, सॉल्वर का Z3str समहू और बूलेक्टर शामिल हैं।

यह भी देखें

  • आंसर सेट प्रोग्रामिंग
  • ऑटोमेटेड थ्योरम प्रोविंग
  • एसएटी सॉल्वर
  • फर्स्ट-आर्डर लॉजिक
  • थ्योरी ऑफ़ पुरे इक्वलिटी

टिप्पणियाँ

  1. Barbosa, Haniel; Reynolds, Andrew; El Ouraoui, Daniel; Tinelli, Cesare; Barrett, Clark (2019). "Extending SMT solvers to higher-order logic". Automated Deduction – CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings. Springer. pp. 35–54. doi:10.1007/978-3-030-29436-6_3. ISBN 978-3-030-29436-6. S2CID 85443815. hal-02300986.
  2. Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. (2006), "Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)" (PDF), Journal of the ACM, vol. 53, pp. 937–977, doi:10.1145/1217856.1217859, S2CID 14058631
  3. Bauer, A.; Pister, M.; Tautschnig, M. (2007), "Tool-support for the analysis of hybrid systems and models", Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE'07), IEEE Computer Society, p. 1, CiteSeerX 10.1.1.323.6807, doi:10.1109/DATE.2007.364411, ISBN 978-3-9810801-2-4, S2CID 9159847
  4. Fränzle, M.; Herde, C.; Ratschan, S.; Schubert, T.; Teige, T. (2007), "Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure" (PDF), Journal on Satisfiability, Boolean Modeling and Computation, 1 (3–4 JSAT Special Issue on SAT/CP Integration): 209–236, doi:10.3233/SAT190012
  5. Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). "SMT-COMP: Satisfiability Modulo Theories Competition". In Etessami, Kousha; Rajamani, Sriram K. (eds.). कंप्यूटर सहायता प्राप्त सत्यापन. Lecture Notes in Computer Science. Vol. 3576. Springer. pp. 20–23. doi:10.1007/11513988_4. ISBN 978-3-540-31686-2.
  6. Barrett, Clark; de Moura, Leonardo; Ranise, Silvio; Stump, Aaron; Tinelli, Cesare (2011). "The SMT-LIB Initiative and the Rise of SMT". In Barner, Sharon; Harris, Ian; Kroening, Daniel; Raz, Orna (eds.). Hardware and Software: Verification and Testing. Lecture Notes in Computer Science. Vol. 6504. Springer. p. 3. Bibcode:2011LNCS.6504....3B. doi:10.1007/978-3-642-19583-9_2. ISBN 978-3-642-19583-9.
  7. "SMT-COMP 2020". SMT-COMP (in English). Retrieved 2020-10-19.
  8. Hassan, Mostafa; Urban, Caterina; Eilers, Marco; Müller, Peter (2018). "MaxSMT-Based Type Inference for Python 3". कंप्यूटर सहायता प्राप्त सत्यापन. Lecture Notes in Computer Science. Vol. 10982. pp. 12–19. doi:10.1007/978-3-319-96142-2_2. ISBN 978-3-319-96141-5.
  9. Loncaric, Calvin, et al. "A practical framework for type inference error explanation." ACM SIGPLAN Notices 51.10 (2016): 781-799.
  10. Beaumont, Paul; Evans, Neil; Huth, Michael; Plant, Tom (2015). Pernul, Günther; Y A Ryan, Peter; Weippl, Edgar (eds.). "Confidence Analysis for Nuclear Arms Control: SMT Abstractions of Bayesian Belief Networks". Computer Security – ESORICS 2015. Lecture Notes in Computer Science. Springer. 9326: 521–540. doi:10.1007/978-3-319-24174-6_27. ISBN 978-3-319-24174-6.


संदर्भ