संतुष्टि मॉड्यूलो सिद्धांत: Difference between revisions
No edit summary |
|||
(6 intermediate revisions by 3 users not shown) | |||
Line 1: | Line 1: | ||
{{Short description|Logical problem studied in computer science}} | {{Short description|Logical problem studied in computer science}} | ||
[[कंप्यूटर विज्ञान]] और [[गणितीय तर्क]] में, '''[[संतुष्टि]] मॉड्यूल सिद्धांत ( | [[कंप्यूटर विज्ञान]] और [[गणितीय तर्क]] में, '''[[संतुष्टि]] मॉड्यूल सिद्धांत (SMT)''' यह निर्धारित करने की समस्या है कि कोई गणितीय सूत्र संतोषजनक है या नहीं। यह [[बूलियन संतुष्टि समस्या]] (SAT) को वास्तविक संख्याओं, [[पूर्णांकों]] और/या सूचियों, ऐरे, बिट वैक्टर और स्ट्रिंग्स जैसी विभिन्न डेटा संरचनाओं को सम्मिलित करने वाले अधिक जटिल सूत्रों में सामान्यीकृत करता है। यह नाम इस तथ्य से लिया गया है कि इन अभिव्यक्तियों की व्याख्या समानता के साथ प्रथम-क्रम तर्क में एक निश्चित औपचारिक सिद्धांत ("मॉड्यूलो") के भीतर की जाती है (प्रायः क्वांटिफायर की अनुमति नहीं दी जाती है)। SMT सॉल्वर ऐसे उपकरण हैं जिनका लक्ष्य इनपुट के व्यावहारिक सबसेट के लिए SMT समस्या को हल करना है। Z3 और cvc5 जैसे '''SMT सॉल्वर''' का उपयोग कंप्यूटर विज्ञान में अनुप्रयोगों की एक विस्तृत श्रृंखला के लिए बिल्डिंग ब्लॉक के रूप में किया गया है, जिसमें स्वचालित प्रमेय सिद्ध करना, प्रोग्राम विश्लेषण, प्रोग्राम सत्यापन और सॉफ़्टवेयर परीक्षण सम्मिलित हैं। | ||
चूँकि बूलियन संतुष्टि पहले से ही एनपी-पूर्ण है, | चूँकि बूलियन संतुष्टि पहले से ही एनपी-पूर्ण है, SMT समस्या सामान्यतः एनपी-हार्ड है, और कई सिद्धांतों के लिए यह अनिर्णीत है। शोधकर्ता अध्ययन करते हैं कि कौन से सिद्धांत या सिद्धांतों के उपसमुच्चय एक निर्णायक SMT समस्या और निर्णायक स्थितियों की कम्प्यूटेशनल सम्मिश्रता को उत्त्पन्न करते हैं। परिणामी निर्णय प्रक्रियाएँ प्रायः सीधे SMT सॉल्वर में लागू की जाती हैं; उदाहरण के लिए, प्रेस्बर्गर अंकगणित की निर्णायकता देखें। SMT को एक बाधा संतुष्टि समस्या के रूप में सोचा जा सकता है और इस प्रकार कन्सट्रैन्ट प्रोग्रामिंग के लिए एक निश्चित औपचारिक दृष्टिकोण माना जा सकता है। | ||
==मूल शब्दावली== | ==मूल शब्दावली== | ||
औपचारिक रूप से कहें तो, एक | औपचारिक रूप से कहें तो, एक SMT उदाहरण प्रथम-क्रम तर्क में एक सूत्र है, जहां कुछ फ़ंक्शन और विधेय प्रतीकों की अतिरिक्त व्याख्याएं होती हैं, और SMT यह निर्धारित करने की समस्या है कि क्या ऐसा सूत्र संतोषजनक है। दूसरे शब्दों में, बूलियन संतुष्टि समस्या (SAT) के एक उदाहरण की कल्पना करें जिसमें कुछ बाइनरी वैरिएबल को गैर-बाइनरी वैरिएबल के उपयुक्त सेट पर विधेय द्वारा प्रतिस्थापित किया जाता है। एक विधेय गैर-बाइनरी चर का एक द्विआधारी-मूल्यवान फ़ंक्शन है। उदाहरण विधेय में रैखिक असमानताएँ (उदाहरण के लिए, <math>3x + 2y - z \geq 4</math>) या बिना व्याख्या किए गए शब्दों और फ़ंक्शन प्रतीकों वाली समानताएं सम्मिलित हैं (उदाहरण के लिए, <math>f(f(u, v), v) = f(u, v)</math> जहां <math>f</math> दो तर्कों का कुछ अनिर्दिष्ट कार्य है)। इन विधेयों को निर्दिष्ट प्रत्येक संबंधित सिद्धांत के अनुसार वर्गीकृत किया गया है। उदाहरण के लिए, वास्तविक चर पर रैखिक असमानताओं का मूल्यांकन रैखिक वास्तविक अंकगणित के सिद्धांत के नियमों का उपयोग करके किया जाता है, जबकि गैर-व्याख्यायित शब्दों और फ़ंक्शन प्रतीकों को सम्मिलित करने वाले विधेय का मूल्यांकन समानता के साथ गैर-व्याख्यायित कार्यों के सिद्धांत के नियमों का उपयोग करके किया जाता है (कभी-कभी इसे रिक्त सिद्धांत के रूप में जाना जाता है) ). अन्य सिद्धांतों में सरणियों और सूची संरचनाओं के सिद्धांत (कंप्यूटर प्रोग्रामों के मॉडलिंग और सत्यापन के लिए उपयोगी), और [[बिट वैक्टर]] के सिद्धांत (मॉडलिंग और हार्डवेयर डिजाइन के सत्यापन में उपयोगी) सम्मिलित हैं। उप-सिद्धांत भी संभव हैं: उदाहरण के लिए, अंतर तर्क रैखिक अंकगणित का एक उप-सिद्धांत है जिसमें प्रत्येक असमानता को चर <math>x</math> और <math>y</math> और स्थिरांक <math>c</math> के लिए <math>x - y > c</math> रूप तक सीमित रखा जाता है। | ||
अधिकांश | अधिकांश SMT सॉल्वर अपने तर्कों के केवल क्वांटिफायर-मुक्त अंशों का समर्थन करते हैं। | ||
==अभिव्यंजक घात== | ==अभिव्यंजक घात== | ||
एक | एक SMT उदाहरण एक बूलियन SAT उदाहरण का सामान्यीकरण है जिसमें चर के विभिन्न सेटों को विभिन्न अंतर्निहित सिद्धांतों से विधेय द्वारा प्रतिस्थापित किया जाता है। SMT सूत्र बूलियन SAT सूत्रों की तुलना में कहीं अधिक समृद्ध [[मॉडलिंग भाषा|मॉडलिंग लैंग्वेज]] प्रदान करते हैं। उदाहरण के लिए, एक SMT सूत्र किसी को बिट स्तर के बजाय शब्द पर [[माइक्रोप्रोसेसर]] के डेटापथ संचालन को मॉडल करने की अनुमति देता है। | ||
तुलनात्मक रूप से, आंसर सेट प्रोग्रामिंग भी विधेय पर | तुलनात्मक रूप से, आंसर सेट प्रोग्रामिंग भी विधेय पर बेस्ड है (अधिक सटीक रूप से, [[परमाणु सूत्र]] से निर्मित परमाणु वाक्यों पर)। SMT के विपरीत, उत्तर-सेट कार्यक्रमों में क्वांटिफायर नहीं होते हैं, और [[रैखिक अंकगणित]] या अंतर तर्क जैसी बाधाओं को आसानी से व्यक्त नहीं कर सकते हैं - एएसपी बूलियन समस्याओं के लिए सबसे उपयुक्त है जो अबाधित कार्यों के मुक्त सिद्धांत को कम करते हैं। एएसपी में बिटवेक्टर के रूप में 32-बिट पूर्णांकों को लागू करने में उन्हीं समस्याओं का सामना करना पड़ता है जिनका प्रारंभिक SMT सॉल्वरों को सामना करना पड़ा था: ''x+y=y+x'' जैसी "स्पष्ट" समरूपता निकालना मुश्किल है। | ||
[[बाधा तर्क प्रोग्रामिंग|कन्सट्रैन्ट लॉजिक प्रोग्रामिंग]] रैखिक अंकगणितीय बाधाओं के लिए समर्थन प्रदान करती है, लेकिन एक पूरी तरह से अलग सैद्धांतिक ढांचे के भीतर। उच्च-क्रम तर्क में सूत्रों को हल करने के लिए | [[बाधा तर्क प्रोग्रामिंग|कन्सट्रैन्ट लॉजिक प्रोग्रामिंग]] रैखिक अंकगणितीय बाधाओं के लिए समर्थन प्रदान करती है, लेकिन एक पूरी तरह से अलग सैद्धांतिक ढांचे के भीतर। उच्च-क्रम तर्क में सूत्रों को हल करने के लिए SMT सॉल्वरों को भी बढ़ाया गया है।<ref>{{cite book |first1=Haniel |last1=Barbosa |first2=Andrew |last2=Reynolds |first3=Daniel |last3=El Ouraoui |first4=Cesare |last4=Tinelli |first5=Clark |last5=Barrett |chapter=Extending SMT solvers to higher-order logic |chapter-url=https://hal.archives-ouvertes.fr/hal-02300986/document |title=Automated Deduction – CADE 27: 27th International Conference on Automated Deduction, Natal, Brazil, August 27–30, 2019, Proceedings |publisher=Springer |date=2019 |isbn=978-3-030-29436-6 |pages=35–54 |doi=10.1007/978-3-030-29436-6_3 |s2cid=85443815 |id=hal-02300986}}</ref> | ||
==सॉल्वर दृष्टिकोण== | ==सॉल्वर दृष्टिकोण== | ||
SMT उदाहरणों को हल करने के प्रारंभिक प्रयासों में उन्हें बूलियन SAT उदाहरणों में अनुवाद करना सम्मिलित था (उदाहरण के लिए, एक 32-बिट पूर्णांक चर को उचित वजन के साथ 32 एकल-बिट चर द्वारा एन्कोड किया जाएगा और 'प्लस' जैसे शब्द-स्तरीय संचालन को निम्न द्वारा प्रतिस्थापित किया जाएगा- बिट्स पर लेवल लॉजिक ऑपरेशंस) और इस फॉर्मूले को बूलियन SAT सॉल्वर में पास करना। इस दृष्टिकोण, जिसे उत्सुक दृष्टिकोण के रूप में जाना जाता है, की अपनी खूबियां हैं: SMT फॉर्मूला को समकक्ष बूलियन SAT फॉर्मूला में पूर्व-प्रसंस्करण द्वारा उपस्थित बूलियन SAT सॉल्वरों का उपयोग "जैसा है" किया जा सकता है और समय के साथ उनके प्रदर्शन और क्षमता में सुधार किया जा सकता है। दूसरी ओर, अंतर्निहित सिद्धांतों के उच्च-स्तरीय शब्दार्थ के नुकसान का मतलब है कि बूलियन SAT सॉल्वर को "स्पष्ट" तथ्यों (जैसे कि पूर्णांक जोड़ के लिए <math>x + y = y + x</math>) की खोज के लिए आवश्यकता से अधिक कठिन काम करना पड़ता है।) इस अवलोकन से कई SMT सॉल्वरों का विकास हुआ जो डीपीएलएल-शैली खोज के बूलियन तर्क को सिद्धांत-विशिष्ट सॉल्वरों (टी-सॉल्वर्स) के साथ मजबूती से एकीकृत करते हैं जो किसी दिए गए सिद्धांत से विधेय के संयोजन (एएनडी) को संभालते हैं। इस दृष्टिकोण को लेजी दृष्टिकोण के रूप में जाना जाता है. | |||
डब किया गया [[डीपीएलएल(टी)]],<ref>{{Citation | डब किया गया [[डीपीएलएल(टी)]],<ref>{{Citation | ||
Line 34: | Line 34: | ||
| year = 2006 |doi=10.1145/1217856.1217859 | | year = 2006 |doi=10.1145/1217856.1217859 | ||
| issue=6| s2cid = 14058631 | | issue=6| s2cid = 14058631 | ||
}}</ref> यह आर्किटेक्चर डीपीएलएल- | }}</ref> यह आर्किटेक्चर डीपीएलएल-बेस्ड SAT सॉल्वर को बूलियन तर्क की जिम्मेदारी देता है, जो बदले में, एक अच्छी तरह से परिभाषित इंटरफ़ेस के माध्यम से सिद्धांत टी के लिए एक सॉल्वर के साथ बातचीत करता है। सिद्धांत सॉल्वर को केवल SAT सॉल्वर से पारित सिद्धांत विधेय के संयोजन की व्यवहार्यता की जांच करने के बारे में चिंता करने की ज़रूरत है क्योंकि यह सूत्र के बूलियन सर्च स्थान की खोज करता है। हालाँकि, इस एकीकरण के अच्छी तरह से काम करने के लिए, सिद्धांत समाधानकर्ता को प्रसार और संघर्ष विश्लेषण में भाग लेने में सक्षम होना चाहिए, अर्थात, उसे पहले से स्थापित तथ्यों से नए तथ्यों का अनुमान लगाने में सक्षम होना चाहिए, साथ ही सैद्धांतिक विरोधिता उत्पन्न होने पर अव्यवहार्यता की संक्षिप्त व्याख्या प्रदान करना। दूसरे शब्दों में, थ्योरी सॉल्वर वृद्धिशील और बैकट्रैकेबल होना चाहिए। | ||
==अनिर्णीत सिद्धांतों के लिए | ==अनिर्णीत सिद्धांतों के लिए SMT== | ||
अधिकांश सामान्य | अधिकांश सामान्य SMT दृष्टिकोण निर्णायक सिद्धांतों का समर्थन करते हैं। हालाँकि, कई वास्तविक दुनिया प्रणालियाँ, जैसे कि एक विमान और उसका व्यवहार, केवल पारमार्थिक फंक्शन से जुड़े वास्तविक संख्याओं पर गैर-रैखिक अंकगणित के माध्यम से मॉडलिंग की जा सकती हैं। यह तथ्य SMT समस्या के गैर-रेखीय सिद्धांतों तक विस्तार को प्रेरित करता है, जैसे यह निर्धारित करना कि क्या निम्नलिखित समीकरण संतोषजनक है: | ||
: <math> | : <math> | ||
Line 49: | Line 49: | ||
हालाँकि, ऐसी समस्याएँ सामान्यतः अनिर्णीत होती हैं। (दूसरी ओर, वास्तविक बंद क्षेत्रों का सिद्धांत, और इस प्रकार वास्तविक संख्याओं का पूर्ण प्रथम क्रम सिद्धांत, क्वांटिफायर उन्मूलन का उपयोग करके तय किया जा सकता है। यह [[अल्फ्रेड टार्स्की]] के कारण है।) जोड़ के साथ प्राकृतिक संख्याओं का पहला क्रम सिद्धांत ( लेकिन गुणा नहीं), जिसे प्रेस्बर्गर अंकगणित कहा जाता है, भी निर्णय योग्य है। चूँकि स्थिरांकों द्वारा गुणन को नेस्टेड परिवर्धन के रूप में कार्यान्वित किया जा सकता है, कई कंप्यूटर प्रोग्रामों में अंकगणित को प्रेसबर्गर अंकगणित का उपयोग करके व्यक्त किया जा सकता है, जिसके परिणामस्वरूप निर्णायक सूत्र प्राप्त होते हैं। | हालाँकि, ऐसी समस्याएँ सामान्यतः अनिर्णीत होती हैं। (दूसरी ओर, वास्तविक बंद क्षेत्रों का सिद्धांत, और इस प्रकार वास्तविक संख्याओं का पूर्ण प्रथम क्रम सिद्धांत, क्वांटिफायर उन्मूलन का उपयोग करके तय किया जा सकता है। यह [[अल्फ्रेड टार्स्की]] के कारण है।) जोड़ के साथ प्राकृतिक संख्याओं का पहला क्रम सिद्धांत ( लेकिन गुणा नहीं), जिसे प्रेस्बर्गर अंकगणित कहा जाता है, भी निर्णय योग्य है। चूँकि स्थिरांकों द्वारा गुणन को नेस्टेड परिवर्धन के रूप में कार्यान्वित किया जा सकता है, कई कंप्यूटर प्रोग्रामों में अंकगणित को प्रेसबर्गर अंकगणित का उपयोग करके व्यक्त किया जा सकता है, जिसके परिणामस्वरूप निर्णायक सूत्र प्राप्त होते हैं। | ||
वास्तविकताओं पर अनिर्णीत अंकगणितीय सिद्धांतों से सिद्धांत परमाणुओं के बूलियन संयोजनों को संबोधित करने वाले | वास्तविकताओं पर अनिर्णीत अंकगणितीय सिद्धांतों से सिद्धांत परमाणुओं के बूलियन संयोजनों को संबोधित करने वाले SMT सॉल्वर के उदाहरण एबीएसॉल्वर हैं,<ref>{{Citation | ||
| first1 = A. | | first1 = A. | ||
| last1 = Bauer | | last1 = Bauer | ||
Line 66: | Line 66: | ||
| citeseerx = 10.1.1.323.6807 | | citeseerx = 10.1.1.323.6807 | ||
| s2cid = 9159847 | | s2cid = 9159847 | ||
}}</ref> जो एक गैर-रेखीय अनुकूलन पैकेट के साथ एक शास्त्रीय डीपीएलएल (टी) आर्किटेक्चर को (आवश्यक रूप से अपूर्ण) अधीनस्थ सिद्धांत सॉल्वर और आईएसएटी के रूप में नियोजित करता है। , डीपीएलएल | }}</ref> जो एक गैर-रेखीय अनुकूलन पैकेट के साथ एक शास्त्रीय डीपीएलएल (टी) आर्किटेक्चर को (आवश्यक रूप से अपूर्ण) अधीनस्थ सिद्धांत सॉल्वर और आईएसएटी के रूप में नियोजित करता है। , डीपीएलएल SAT-समाधान और अंतराल बाधा प्रसार के एकीकरण पर निर्माण, जिसे आईएसएटी एल्गोरिदम कहा जाता है।<ref>{{Citation | ||
| first1 = M. | | first1 = M. | ||
| last1 = Fränzle | | last1 = Fränzle | ||
Line 85: | Line 85: | ||
==सॉल्वर{{anchor|SMT solvers}}== | ==सॉल्वर{{anchor|SMT solvers}}== | ||
नीचे दी गई तालिका कई उपलब्ध | नीचे दी गई तालिका कई उपलब्ध SMT सॉल्वरों की कुछ विशेषताओं का सारांश प्रस्तुत करती है। कॉलम "SMT-LIB" SMT-LIB लैंग्वेज के साथ अनुकूलता दर्शाता है; 'हाँ' चिह्नित कई प्रणालियाँ केवल SMT-LIB के पुराने संस्करणों का समर्थन कर सकती हैं, या लैंग्वेज के लिए केवल आंशिक समर्थन प्रदान कर सकती हैं। कॉलम "CVC" CVC लैंग्वेज के लिए समर्थन दर्शाता है। कॉलम "DIMACS" DIMACS प्रारूप के लिए समर्थन दर्शाता है। | ||
परियोजनाएं न केवल सुविधाओं और प्रदर्शन में भिन्न होती हैं, बल्कि आसपास के समुदाय की व्यवहार्यता, परियोजना में इसकी चल रही रुचि और दस्तावेज़ीकरण, सुधार, परीक्षण और संवर्द्धन में योगदान करने की क्षमता में भी भिन्न होती हैं। | परियोजनाएं न केवल सुविधाओं और प्रदर्शन में भिन्न होती हैं, बल्कि आसपास के समुदाय की व्यवहार्यता, परियोजना में इसकी चल रही रुचि और दस्तावेज़ीकरण, सुधार, परीक्षण और संवर्द्धन में योगदान करने की क्षमता में भी भिन्न होती हैं। | ||
=== मानकीकरण और SMT-COMP सॉल्वर प्रतियोगिता === | |||
{| class="wikitable" | {| class="wikitable" | ||
|- | |- | ||
! colspan="3" | | ! colspan="3" | प्लेटफ़ॉर्म | ||
! colspan="6" | | ! colspan="6" | विशेषताएँ | ||
! colspan="1" | | ! colspan="1" | टिप्पणियाँ | ||
|- | |- | ||
! style="background:#ffdead;" | | ! style="background:#ffdead;" | नाम | ||
! style="background:#ffdead;" | | ! style="background:#ffdead;" | ओएस | ||
! style="background:#ffdead;" | | ! style="background:#ffdead;" | लाइसेंस | ||
! style="background:#ffdead;" | | ! style="background:#ffdead;" | SMT-LIB | ||
! style="background:#ffdead;" | CVC | ! style="background:#ffdead;" | CVC | ||
! style="background:#ffdead;" | | ! style="background:#ffdead;" | डायमैक | ||
! style="background:#ffdead;" | | ! style="background:#ffdead;" | अंतर्निर्मित सिद्धांत | ||
! style="background:#ffdead;" | | ! style="background:#ffdead;" | एपीआई | ||
! style="background:#ffdead;" | | ! style="background:#ffdead;" | SMT-कॉम्प[http://www.smtcomp.org/] | ||
! | ! | ||
|- | |- | ||
| ABsolver | | ABsolver | ||
| | | लिनक्स | ||
| [[Common Public License|CPL]] | | [[Common Public License|CPL]] | ||
| {{yes|v1.2}} | | {{yes|v1.2}} | ||
| {{no}} | | {{no}} | ||
| {{yes}} | | {{yes}} | ||
| | | रैखिक अंकगणित, अरेखीय अंकगणित | ||
| [[C++]] | | [[C++]] | ||
| no | | no | ||
| | | डीपीएलएल-बेस्ड | ||
|- | |- | ||
| [[Alt-Ergo | | [[Alt-Ergo]] | ||
| | | लिनक्स , मैक ओएस , विंडोज़ | ||
| [[CeCILL-C]] (roughly equivalent to [[LGPL]]) | | [[CeCILL-C]] (roughly equivalent to [[LGPL]]) | ||
| {{yes|partial v1.2 and v2.0}} | | {{yes|partial v1.2 and v2.0}} | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| | | रिक्त सिद्धांत , रैखिक पूर्णांक और तर्कसंगत अंकगणित, गैर-रेखीय अंकगणित, बहुरूपी ऐरे , प्रगणित डेटा प्रकार , एसी प्रतीक , बिटवेक्टर , रिकॉर्ड डेटा प्रकार , क्वांटिफायर | ||
| [[OCaml]] | | [[OCaml]] | ||
| 2008 | | 2008 | ||
| | |बहुरूपी प्रथम-क्रम इनपुट लैंग्वेज à la ML, SAT-सॉल्वर बेस्ड, तर्क मॉड्यूल सिद्धांतों के लिए शोस्ताक-जैसे और नेल्सन-ओपेन जैसे दृष्टिकोणों को जोड़ती है | ||
|- | |- | ||
| Barcelogic | | Barcelogic | ||
| | | लिनक्स | ||
| Proprietary | | Proprietary | ||
| {{yes|v1.2}} | | {{yes|v1.2}} | ||
| | | | ||
| | | | ||
| | | खोखला सिद्धांत , अंतर तर्क | ||
| [[C++]] | | [[C++]] | ||
| 2009 | | 2009 | ||
| | | डीपीएलएल-बेस्ड, सर्वांगसमता समापन | ||
|- | |- | ||
| Beaver | | Beaver | ||
| | | लिनक्स , विंडोज़ | ||
| [[BSD licenses|BSD]] | | [[BSD licenses|BSD]] | ||
| {{yes|v1.2}} | | {{yes|v1.2}} | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| | | बिटवेक्टर | ||
| [[OCaml]] | | [[OCaml]] | ||
| 2009 | | 2009 | ||
| SAT- | | SAT-सॉल्वर बेस्ड | ||
|- | |- | ||
| Boolector | | Boolector | ||
| | | लिनक्स | ||
| [[MIT License|MIT]] | | [[MIT License|MIT]] | ||
| {{yes|v1.2}} | | {{yes|v1.2}} | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| | | बिटवेक्टर , ऐरे | ||
| [[C (programming language)|C]] | | [[C (programming language)|C]] | ||
| 2009 | | 2009 | ||
| SAT- | | SAT-सॉल्वर बेस्ड | ||
|- | |- | ||
| CVC3 | | CVC3 | ||
| | | लिनक्स | ||
| [[BSD licenses|BSD]] | | [[BSD licenses|BSD]] | ||
| {{yes|v1.2}} | | {{yes|v1.2}} | ||
| {{yes}} | | {{yes}} | ||
| | | | ||
| | | रिक्त सिद्धांत , रैखिक अंकगणित, ऐरे, टुपल्स, प्रकार, रिकॉर्ड, बिटवेक्टर, क्वांटिफायर | ||
| [[C (programming language)|C]]/[[C++]] | | [[C (programming language)|C]]/[[C++]] | ||
| 2010 | | 2010 | ||
| HOL को प्रूफ़ आउटपुट | |||
|- | |- | ||
| CVC4 | | CVC4 | ||
| | | लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी | ||
| [[BSD licenses|BSD]] | | [[BSD licenses|BSD]] | ||
| {{yes}} | | {{yes}} | ||
| {{yes}} | | {{yes}} | ||
| | | | ||
| | | तर्कसंगत और पूर्णांक रैखिक अंकगणित, ऐरे, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, और अबाधित फ़ंक्शन प्रतीकों पर समानता | ||
| C++ | | C++ | ||
| 2021 | | 2021 | ||
| | | संस्करण 1.8 मई 2021 में जारी किया गया | ||
|- | |- | ||
| | | CVC5 | ||
| | | लिनक्स , मैक ओएस , विंडोज़ | ||
| [[BSD licenses|BSD]] | | [[BSD licenses|BSD]] | ||
| {{yes}} | | {{yes}} | ||
| {{yes}} | | {{yes}} | ||
| | | | ||
| | | तर्कसंगत और पूर्णांक रैखिक अंकगणित, ऐरे, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, अनुक्रम, बैग, और अबाधित फ़ंक्शन प्रतीकों पर समानता | ||
| C++, Python, Java | | C++, Python, Java | ||
| 2021 | | 2021 | ||
| | | संस्करण 1.0 अप्रैल 2022 में जारी किया गया | ||
|- | |- | ||
| Decision Procedure Toolkit (DPT) | |Decision Procedure Toolkit (DPT) | ||
| | | लिनक्स | ||
| [[Apache license|Apache]] | | [[Apache license|Apache]] | ||
| {{no}} | | {{no}} | ||
Line 202: | Line 203: | ||
| [[OCaml]] | | [[OCaml]] | ||
| no | | no | ||
| | | डीपीएलएल-बेस्ड | ||
|- | |- | ||
| iSAT | | iSAT | ||
| | | लिनक्स | ||
| Proprietary | | Proprietary | ||
| {{no}} | | {{no}} | ||
| | | | ||
| | | | ||
| | | अरेखीय अंकगणित | ||
| | | | ||
| no | | no | ||
| | | डीपीएलएल-बेस्ड | ||
|- | |- | ||
| MathSAT | | MathSAT | ||
| | | लिनक्स , मैक ओएस , विंडोज़ | ||
| Proprietary | | Proprietary | ||
| {{yes}} | | {{yes}} | ||
| | | | ||
| {{yes}} | | {{yes}} | ||
| | | रिक्त सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, ऐरे | ||
| [[C (programming language)|C]]/[[C++]], [[Python (programming language)|Python]], [[Java (programming language)|Java]] | | [[C (programming language)|C]]/[[C++]], [[Python (programming language)|Python]], [[Java (programming language)|Java]] | ||
| 2010 | | 2010 | ||
| | | डीपीएलएल-बेस्ड | ||
|- | |- | ||
| MiniSmt | | MiniSmt | ||
| | | लिनक्स | ||
| [[LGPL]] | | [[LGPL]] | ||
| {{yes|partial v2.0}} | | {{yes|partial v2.0}} | ||
| | | | ||
| | | | ||
| | | अरेखीय अंकगणित | ||
|[[OCaml]] | |[[OCaml]] | ||
| 2010 | | 2010 | ||
| SAT- | | SAT-सॉल्वर बेस्ड, Yices-बेस्ड | ||
|- | |- | ||
| Norn | | Norn | ||
Line 246: | Line 247: | ||
| | | | ||
| | | | ||
| | | स्ट्रिंग बाधाओं के लिए SMT सॉल्वर | ||
|- | |- | ||
| | |||
|लिनक्स | |||
|- | |- | ||
| [[OpenCog]] | | [[OpenCog]] | ||
| | | लिनक्स | ||
| [[Affero General Public License|AGPL]] | | [[Affero General Public License|AGPL]] | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| | | संभाव्य तर्क , अंकगणित। संबंधपरक मॉडल | ||
| [[C++]], [[Scheme (programming language)|Scheme]], [[Python (programming language)|Python]] | | [[C++]], [[Scheme (programming language)|Scheme]], [[Python (programming language)|Python]] | ||
| no | | no | ||
| | | सबग्राफ समरूपता | ||
|- | |- | ||
| OpenSMT | | OpenSMT | ||
| | | लिनक्स , मैक ओएस , विंडोज़ | ||
| [[GPLv3]] | | [[GPLv3]] | ||
| {{yes|partial v2.0}} | | {{yes|partial v2.0}} | ||
| | | | ||
| {{yes}} | | {{yes}} | ||
| | | रिक्त सिद्धांत , अंतर, रैखिक अंकगणित, बिटवेक्टर | ||
| [[C++]] | | [[C++]] | ||
| 2011 | | 2011 | ||
| | | लेजी SMT सॉल्वर | ||
|- | |- | ||
|raSAT | |raSAT | ||
| | |लिनक्स | ||
|GPLv3 | |GPLv3 | ||
|v2.0 | |v2.0 | ||
| | | | ||
| | | | ||
| | |वास्तविक और पूर्णांक अरेखीय अंकगणित | ||
| | | | ||
|2014, 2015 | |2014, 2015 | ||
| | |परीक्षण और मध्यवर्ती मूल्य प्रमेय के साथ अंतराल बाधा प्रसार का विस्तार | ||
|- | |- | ||
| SatEEn | | SatEEn | ||
Line 288: | Line 291: | ||
| | | | ||
| | | | ||
| | | रैखिक अंकगणित, अंतर तर्क | ||
| none | | none | ||
| 2009 | | 2009 | ||
Line 294: | Line 297: | ||
|- | |- | ||
| SMTInterpol | | SMTInterpol | ||
| | | लिनक्स , मैक ओएस , विंडोज़ | ||
| [[LGPLv3]] | | [[LGPLv3]] | ||
| {{yes|v2.5|align=|style=|color=}} | | {{yes|v2.5|align=|style=|color=}} | ||
| | | | ||
| | | | ||
| | | अव्याख्यायित फलन, रैखिक वास्तविक अंकगणित, और रैखिक पूर्णांक अंकगणित | ||
| [[Java (programming language)|Java]] | | [[Java (programming language)|Java]] | ||
| 2012 | | 2012 | ||
| | | उच्च गुणवत्ता, कॉम्पैक्ट इंटरपोलेंट उत्पन्न करने पर ध्यान केंद्रित करता है। | ||
|- | |- | ||
| SMCHR | | SMCHR | ||
| | | लिनक्स , मैक ओएस , विंडोज़ | ||
| [[GPLv3]] | | [[GPLv3]] | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| | | रैखिक अंकगणित, अरेखीय अंकगणित, हीप | ||
| [[C (programming language)|C]] | | [[C (programming language)|C]] | ||
| no | | no | ||
| | | बाधा प्रबंधन नियमों का उपयोग करके नए सिद्धांतों को लागू कर सकते हैं । | ||
|- | |- | ||
| | | SMT-RAT | ||
| | | लिनक्स , मैक ओएस | ||
| [[MIT License|MIT]] | | [[MIT License|MIT]] | ||
| {{yes|v2.0}} | | {{yes|v2.0}} | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| | | रैखिक अंकगणित, अरेखीय अंकगणित | ||
| [[C++]] | | [[C++]] | ||
| 2015 | | 2015 | ||
| | | रणनीतिक और समानांतर SMT समाधान के लिए टूलबॉक्स जिसमें SMT अनुरूप कार्यान्वयन का संग्रह सम्मिलित है। | ||
|- | |- | ||
| SONOLAR | | SONOLAR | ||
| | | लिनक्स , विंडोज़ | ||
| Proprietary | | Proprietary | ||
| {{yes|partial v2.0}} | | {{yes|partial v2.0}} | ||
| | | | ||
| | | | ||
| | | बिटवेक्टर | ||
| [[C (programming language)|C]] | | [[C (programming language)|C]] | ||
| 2010 | | 2010 | ||
| SAT- | | SAT-सॉल्वर बेस्ड | ||
|- | |- | ||
| Spear | | Spear | ||
| | | लिनक्स , मैक ओएस , विंडोज़ | ||
| Proprietary | | Proprietary | ||
| {{yes|v1.2}} | | {{yes|v1.2}} | ||
| | | | ||
| | | | ||
| | | बिटवेक्टर | ||
| | | | ||
| 2008 | | 2008 | ||
| | | | ||
|- | |- | ||
| | | STP | ||
| | | लिनक्स , ओपनबीएसडी , विंडोज , मैक ओएस | ||
| [[MIT License|MIT]] | | [[MIT License|MIT]] | ||
| {{yes|partial v2.0}} | | {{yes|partial v2.0}} | ||
| {{yes}} | | {{yes}} | ||
| {{no}} | | {{no}} | ||
| | | बिटवेक्टर, ऐरे | ||
| [[C (programming language)|C]], [[C++]], [[Python (programming language)|Python]], [[OCaml]], [[Java (programming language)|Java]] | | [[C (programming language)|C]], [[C++]], [[Python (programming language)|Python]], [[OCaml]], [[Java (programming language)|Java]] | ||
| 2011 | | 2011 | ||
| SAT- | | SAT-सॉल्वर बेस्ड | ||
|- | |- | ||
| SWORD | | SWORD | ||
| | | लिनक्स | ||
| Proprietary | | Proprietary | ||
| {{yes|v1.2}} | | {{yes|v1.2}} | ||
| | | | ||
| | | | ||
| | | बिटवेक्टर | ||
| | | | ||
| 2009 | | 2009 | ||
Line 371: | Line 374: | ||
|- | |- | ||
| UCLID | | UCLID | ||
| | | लिनक्स | ||
| [[BSD licenses|BSD]] | | [[BSD licenses|BSD]] | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| {{no}} | | {{no}} | ||
| | | रिक्त सिद्धांत , रैखिक अंकगणित, बिटवेक्टर, और विवश लैम्ब्डा (सरणी, यादें, कैश, आदि) | ||
| | | | ||
| no | | no | ||
| SAT- | | SAT-सॉल्वर बेस्ड, मॉस्को एमएल में लिखा गया । इनपुट लैंग्वेज एसएमवी मॉडल चेकर है। अच्छी तरह से प्रलेखित! | ||
|- | |- | ||
| veriT | | veriT | ||
| | | लिनक्स , ओएस एक्स | ||
| [[BSD licenses|BSD]] | | [[BSD licenses|BSD]] | ||
| {{yes|partial v2.0}} | | {{yes|partial v2.0}} | ||
| | | | ||
| | | | ||
| | | रिक्त सिद्धांत , तर्कसंगत और पूर्णांक रैखिक अंकगणित, परिमाणक, और अबाधित फ़ंक्शन प्रतीकों पर समानता | ||
| [[C (programming language)|C]]/[[C++]] | | [[C (programming language)|C]]/[[C++]] | ||
| 2010 | | 2010 | ||
| SAT- | | SAT-सॉल्वर बेस्ड, प्रमाण प्रस्तुत कर सकते हैं | ||
|- | |- | ||
| {{Visible anchor|Yices}} | | {{Visible anchor|Yices}} | ||
| | | लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी | ||
| [[GPLv3]] | | [[GPLv3]] | ||
| {{yes| v2.0}} | | {{yes| v2.0}} | ||
| {{no}} | | {{no}} | ||
| {{yes}} | | {{yes}} | ||
| | | तर्कसंगत और पूर्णांक रैखिक अंकगणित, बिटवेक्टर, ऐरे, और अबाधित फ़ंक्शन प्रतीकों पर समानता | ||
| [[C (programming language)|C]] | | [[C (programming language)|C]] | ||
| 2014 | | 2014 | ||
| | | सोर्स कोड ऑनलाइन उपलब्ध है | ||
|- | |- | ||
| [[Z3 Theorem Prover]] | | [[Z3 Theorem Prover]] | ||
| | | लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी | ||
| [[MIT License|MIT]] | | [[MIT License|MIT]] | ||
| {{yes| v2.0}} | | {{yes| v2.0}} | ||
| | | | ||
| {{yes}} | | {{yes}} | ||
| | | रिक्त सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, ऐरे, डेटाटाइप, क्वांटिफायर , स्ट्रिंग्स | ||
| [[C (programming language)|C]]/[[C++]], [[.NET Framework|.NET]], [[OCaml]], [[Python (programming language)|Python]], [[Java (programming language)|Java]], [[Haskell (programming language)|Haskell]] | | [[C (programming language)|C]]/[[C++]], [[.NET Framework|.NET]], [[OCaml]], [[Python (programming language)|Python]], [[Java (programming language)|Java]], [[Haskell (programming language)|Haskell]] | ||
| 2011 | | 2011 | ||
| | | सोर्स कोड ऑनलाइन उपलब्ध है | ||
|} | |} | ||
=== मानकीकरण और | === मानकीकरण और SMT-COMP सॉल्वर प्रतियोगिता === | ||
SMT सॉल्वरों (और स्वचालित प्रमेय प्रोवर्स, एक शब्द जिसे प्रायः समानार्थक रूप से उपयोग किया जाता है) के लिए एक मानकीकृत इंटरफ़ेस का वर्णन करने के कई प्रयास किए गए हैं। सबसे प्रमुख SMT-LIB मानक है, जो S-अभिव्यक्ति पर बेस्ड लैंग्वेज प्रदान करता है। सामान्यतः समर्थित अन्य मानकीकृत प्रारूप कई बूलियन SAT सॉल्वरों द्वारा समर्थित डीआईएमएसीएस प्रारूप हैं, और CVC प्रारूप CVC स्वचालित प्रमेय प्रोवर द्वारा उपयोग किया जाता है। | |||
SMT-LIB प्रारूप भी कई मानकीकृत बेंचमार्क के साथ आता है और इसने SMT-COMP नामक SMT सॉल्वरों के बीच एक वार्षिक प्रतियोगिता को सक्षम किया है। प्रारंभ में, प्रतियोगिता कंप्यूटर एडेड सत्यापन सम्मेलन (सीएवी) के दौरान हुई थी,<ref>{{Cite book|last1=Barrett|first1=Clark|last2=de Moura|first2=Leonardo|last3=Stump|first3=Aaron|date=2005|editor-last=Etessami|editor-first=Kousha|editor2-last=Rajamani|editor2-first=Sriram K.|chapter=SMT-COMP: Satisfiability Modulo Theories Competition|url=https://link.springer.com/chapter/10.1007%2F11513988_4|title=कंप्यूटर सहायता प्राप्त सत्यापन|series=Lecture Notes in Computer Science|volume=3576|publisher=Springer|pages=20–23|doi=10.1007/11513988_4|isbn=978-3-540-31686-2}}</ref><ref>{{Cite book|last1=Barrett|first1=Clark|last2=de Moura|first2=Leonardo|last3=Ranise|first3=Silvio|last4=Stump|first4=Aaron|last5=Tinelli|first5=Cesare|date=2011|editor-last=Barner|editor-first=Sharon|editor2-last=Harris|editor2-first=Ian|editor3-last=Kroening|editor3-first=Daniel|editor4-last=Raz|editor4-first=Orna|chapter=The SMT-LIB Initiative and the Rise of SMT|title=Hardware and Software: Verification and Testing|series=Lecture Notes in Computer Science|volume=6504|publisher=Springer|pages=3|doi=10.1007/978-3-642-19583-9_2|bibcode=2011LNCS.6504....3B|isbn=978-3-642-19583-9|doi-access=free}}</ref> लेकिन 2020 तक प्रतियोगिता को SMT कार्यशाला के हिस्से के रूप में आयोजित किया गया है, जो स्वचालित तर्क (आईजेसीएआर) पर अंतर्राष्ट्रीय संयुक्त सम्मेलन से संबद्ध है)।<ref>{{Cite web|title=SMT-COMP 2020|url=https://smt-comp.github.io/2020/|access-date=2020-10-19|website=SMT-COMP|language=en-US}}</ref> | |||
==अनुप्रयोग== | ==अनुप्रयोग== | ||
SMT सॉल्वर सत्यापन, प्रोग्राम की यथार्थता सिद्ध करने, प्रतीकात्मक निष्पादन के आधार पर सॉफ्टवेयर परीक्षण, और संश्लेषण के लिए, संभावित प्रोग्रमम के स्थान पर सर्च करके प्रोग्रम के भाग उत्पन्न करने के लिए उपयोगी हैं। सॉफ़्टवेयर सत्यापन के अलावा, SMT सॉल्वरों का उपयोग प्रकार के अनुमान के लिए भी किया गया है<ref>{{Cite book|chapter-url=https://link.springer.com/chapter/10.1007/978-3-319-96142-2_2|doi=10.1007/978-3-319-96142-2_2|chapter=MaxSMT-Based Type Inference for Python 3|title=कंप्यूटर सहायता प्राप्त सत्यापन|series=Lecture Notes in Computer Science|year=2018|last1=Hassan|first1=Mostafa|last2=Urban|first2=Caterina|last3=Eilers|first3=Marco|last4=Müller|first4=Peter|volume=10982|pages=12–19|isbn=978-3-319-96141-5}}</ref><ref>Loncaric, Calvin, et al. [https://manu.sridharan.net/files/mycroft-preprint.pdf "A practical framework for type inference error explanation."] ACM SIGPLAN Notices 51.10 (2016): 781-799.</ref> और परमाणु उपकरण नियंत्रण में साधक के विश्वासों को मॉडलिंग करने सहित सैद्धांतिक परिदृश्यों के मॉडलिंग के लिए भी है।<ref>{{Cite journal|last1=Beaumont|first1=Paul|last2=Evans|first2=Neil|last3=Huth|first3=Michael|last4=Plant|first4=Tom|date=2015|editor-last=Pernul|editor-first=Günther|editor2-last=Y A Ryan|editor2-first=Peter|editor3-last=Weippl|editor3-first=Edgar|title=Confidence Analysis for Nuclear Arms Control: SMT Abstractions of Bayesian Belief Networks|journal=Computer Security – ESORICS 2015|series=Lecture Notes in Computer Science|volume=9326|publisher=Springer |pages=521–540|doi=10.1007/978-3-319-24174-6_27|isbn=978-3-319-24174-6|doi-access=free}}</ref> | |||
===सत्यापन<!--'CVC4' redirects here-->=== | ===सत्यापन<!--'CVC4' redirects here-->=== | ||
कंप्यूटर प्रोग्रामों का कंप्यूटर समर्थित सत्यापन | कंप्यूटर प्रोग्रामों का कंप्यूटर समर्थित सत्यापन प्रायः SMT सॉल्वर का उपयोग करता है। यह निर्धारित करने के लिए कि क्या सभी गुण धारण किए जा सकते हैं, एक सामान्य तकनीक पूर्व शर्त, पोस्टकंडिशन, लूप स्थिति और SMT सूत्रों में दावे का अनुवाद करना है। | ||
Z3 | Z3 SMT सॉल्वर के शीर्ष पर कई सत्यापनकर्ता बनाए गए हैं। बूगी एक मध्यवर्ती सत्यापन लैंग्वेज है जो सरल अनिवार्य कार्यक्रमों की स्वचालित रूप से जाँच करने के लिए Z3 का उपयोग करती है। समवर्ती सी के लिए वीसीसी सत्यापनकर्ता बूगी का उपयोग करता है, साथ ही अनिवार्य वस्तु-बेस्ड कार्यक्रमों के लिए डैफनी, समवर्ती कार्यक्रमों के लिए चालिस और सी# के लिए स्पेक# का उपयोग करता है। F* एक निर्भरता से टाइप की जाने वाली लैंग्वेज है जो प्रमाण खोजने के लिए Z3 का उपयोग करती है; कंपाइलर इन सबूतों को प्रूफ-ले जाने वाले बाइटकोड का उत्पादन करने के लिए ले जाता है। वाइपर सत्यापन अवसंरचना सत्यापन शर्तों को Z3 में एनकोड करती है। एसबीवी लाइब्रेरी हास्केल कार्यक्रमों का SMT-बेस्ड सत्यापन प्रदान करती है, और उपयोगकर्ता को Z3, एबीसी, बूलेक्टर, CVC5, मैथसैट और येस जैसे कई सॉल्वरों में से चुनने की सुविधा देती है। | ||
* ऑल्ट-एर्गो | * ऑल्ट-एर्गो SMT सॉल्वर के ऊपर कई सत्यापनकर्ता भी बनाए गए हैं। यहां परिपक्व आवेदनों की सूची दी गई है: | ||
* व्हाय3, डिडक्टिव प्रोग्राम सत्यापन के लिए एक मंच, ऑल्ट-एर्गो को अपने मुख्य कहावत के रूप में उपयोग करता है; | * व्हाय3, डिडक्टिव प्रोग्राम सत्यापन के लिए एक मंच, ऑल्ट-एर्गो को अपने मुख्य कहावत के रूप में उपयोग करता है; | ||
* कैविएट, सीईए द्वारा विकसित और एयरबस द्वारा उपयोग किया जाने वाला एक सी-सत्यापनकर्ता; ऑल्ट-एर्गो को इसके हालिया विमानों में से एक की योग्यता DO-178C में | * कैविएट, सीईए द्वारा विकसित और एयरबस द्वारा उपयोग किया जाने वाला एक सी-सत्यापनकर्ता; ऑल्ट-एर्गो को इसके हालिया विमानों में से एक की योग्यता DO-178C में सम्मिलित किया गया था; | ||
* फ्रैमा-सी, सी-कोड का विश्लेषण करने के लिए एक ढांचा, जेसी और डब्ल्यूपी प्लगइन्स ("डिडक्टिव प्रोग्राम वेरिफिकेशन" के लिए समर्पित) में ऑल्ट-एर्गो का उपयोग करता है; | * फ्रैमा-सी, सी-कोड का विश्लेषण करने के लिए एक ढांचा, जेसी और डब्ल्यूपी प्लगइन्स ("डिडक्टिव प्रोग्राम वेरिफिकेशन" के लिए समर्पित) में ऑल्ट-एर्गो का उपयोग करता है; | ||
* स्पार्क 2014 में कुछ दावों के सत्यापन को स्वचालित करने के लिए स्पार्क CVC4 और ऑल्ट-एर्गो (GNATprove के पीछे) का उपयोग करता है; | * स्पार्क 2014 में कुछ दावों के सत्यापन को स्वचालित करने के लिए स्पार्क CVC4 और ऑल्ट-एर्गो (GNATprove के पीछे) का उपयोग करता है; | ||
* एटेलियर-बी अपने मुख्य प्रोवर के बजाय ऑल्ट-एर्गो का उपयोग कर सकता है (एएनआर बीवेयर प्रोजेक्ट बेंचमार्क पर सफलता 84% से बढ़कर 98% हो गई है); | * एटेलियर-बी अपने मुख्य प्रोवर के बजाय ऑल्ट-एर्गो का उपयोग कर सकता है (एएनआर बीवेयर प्रोजेक्ट बेंचमार्क पर सफलता 84% से बढ़कर 98% हो गई है); | ||
* रॉडिन, सिस्टरेल द्वारा विकसित एक बी-मेथड फ्रेमवर्क, ऑल्ट-एर्गो को बैक-एंड के रूप में उपयोग कर सकता है; | * रॉडिन, सिस्टरेल द्वारा विकसित एक बी-मेथड फ्रेमवर्क, ऑल्ट-एर्गो को बैक-एंड के रूप में उपयोग कर सकता है; | ||
* क्यूबिकल, सरणी- | * क्यूबिकल, सरणी-बेस्ड संक्रमण प्रणालियों की सुरक्षा गुणों की पुष्टि के लिए एक खुला सोर्स मॉडल चेकर। | ||
* ईज़ीक्रिप्ट, प्रतिकूल कोड के साथ संभाव्य संगणनाओं के संबंधपरक गुणों के बारे में तर्क करने के लिए एक टूलसेट। | * ईज़ीक्रिप्ट, प्रतिकूल कोड के साथ संभाव्य संगणनाओं के संबंधपरक गुणों के बारे में तर्क करने के लिए एक टूलसेट। | ||
कई | कई SMT सॉल्वर SMTLIB2 नामक एक सामान्य इंटरफ़ेस प्रारूप लागू करते हैं (ऐसी फ़ाइलों में सामान्यतः एक्सटेंशन "<code>.smt2</code>" होता है)। लिक्विडहास्केल उपकरण हास्केल के लिए एक परिशोधन प्रकार-बेस्ड सत्यापनकर्ता लागू करता है जो किसी भी SMTLIB2 अनुरूप सॉल्वर का उपयोग कर सकता है, जैसे cvc5, MathSat, या Z3। | ||
===सांकेतिक-निष्पादन | ===सांकेतिक-निष्पादन बेस्ड विश्लेषण एवं परीक्षण=== | ||
SMT सॉल्वरों का एक महत्वपूर्ण एप्लीकेशन प्रोग्राम के विश्लेषण और परीक्षण के लिए प्रतीकात्मक निष्पादन है (उदाहरण के लिए, कॉन्कोलिक परीक्षण), जिसका उद्देश्य विशेष रूप से सुरक्षा कमजोरियों का पता लगाना है। इस श्रेणी के उदाहरण टूल में [[माइक्रोसॉफ्ट रिसर्च]] से [http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf SAGE], [https://klee.github.io/ KLEE], [http://s2e.epfl.ch/ S2E] और [https://triton.quarkslab.com ट्राइटन]शामिल हैं। SMT सॉल्वर जिनका उपयोग प्रतीकात्मक-निष्पादन अनुप्रयोगों के लिए किया गया है, उनमें [https://github.com/Z3Prover/z3 Z3], [https://sites.google.com/site/stpfastprover/ एसटीपी] आर्काइव्ड 2015-04-06 वेबैक मशीन, सॉल्वर का Z3str समहू और बूलेक्टर सम्मिलित हैं। | |||
==यह भी देखें== | ==यह भी देखें== | ||
Line 445: | Line 448: | ||
* आंसर सेट प्रोग्रामिंग | * आंसर सेट प्रोग्रामिंग | ||
* ऑटोमेटेड थ्योरम प्रोविंग | * ऑटोमेटेड थ्योरम प्रोविंग | ||
* | * SAT सॉल्वर | ||
* फर्स्ट-आर्डर लॉजिक | * फर्स्ट-आर्डर लॉजिक | ||
* थ्योरी ऑफ़ पुरे इक्वलिटी | * थ्योरी ऑफ़ पुरे इक्वलिटी | ||
Line 471: | Line 474: | ||
{{refend}} | {{refend}} | ||
{{Mathematical logic}} | {{Mathematical logic}} | ||
[[Category: | [[Category:CS1 English-language sources (en)]] | ||
[[Category:Collapse templates]] | |||
[[Category:Created On 24/07/2023]] | [[Category:Created On 24/07/2023]] | ||
[[Category:Lua-based templates]] | |||
[[Category:Machine Translated Page]] | |||
[[Category:Mathematics navigational boxes]] | |||
[[Category:Navbox orphans]] | |||
[[Category:Navigational boxes| ]] | |||
[[Category:Navigational boxes without horizontal lists]] | |||
[[Category:Pages with empty portal template]] | |||
[[Category:Pages with script errors]] | |||
[[Category:Philosophy and thinking navigational boxes]] | |||
[[Category:Portal-inline template with redlinked portals]] | |||
[[Category:Short description with empty Wikidata description]] | |||
[[Category:Sidebars with styles needing conversion]] | |||
[[Category:Template documentation pages|Documentation/doc]] | |||
[[Category:Templates Translated in Hindi]] | |||
[[Category:Templates Vigyan Ready]] | |||
[[Category:Templates generating microformats]] | |||
[[Category:Templates that add a tracking category]] | |||
[[Category:Templates that are not mobile friendly]] | |||
[[Category:Templates that generate short descriptions]] | |||
[[Category:Templates using TemplateData]] | |||
[[Category:Wikipedia metatemplates]] | |||
[[Category:इलेक्ट्रॉनिक डिज़ाइन स्वचालन]] | |||
[[Category:एनपी-पूर्ण समस्याएँ]] | |||
[[Category:औपचारिक तरीके]] | |||
[[Category:कंप्यूटर विज्ञान में तर्क]] | |||
[[Category:बाधा प्रोग्रामिंग]] | |||
[[Category:श्रीमती सॉल्वर]] | |||
[[Category:संतुष्टि की समस्या]] |
Latest revision as of 13:58, 14 August 2023
कंप्यूटर विज्ञान और गणितीय तर्क में, संतुष्टि मॉड्यूल सिद्धांत (SMT) यह निर्धारित करने की समस्या है कि कोई गणितीय सूत्र संतोषजनक है या नहीं। यह बूलियन संतुष्टि समस्या (SAT) को वास्तविक संख्याओं, पूर्णांकों और/या सूचियों, ऐरे, बिट वैक्टर और स्ट्रिंग्स जैसी विभिन्न डेटा संरचनाओं को सम्मिलित करने वाले अधिक जटिल सूत्रों में सामान्यीकृत करता है। यह नाम इस तथ्य से लिया गया है कि इन अभिव्यक्तियों की व्याख्या समानता के साथ प्रथम-क्रम तर्क में एक निश्चित औपचारिक सिद्धांत ("मॉड्यूलो") के भीतर की जाती है (प्रायः क्वांटिफायर की अनुमति नहीं दी जाती है)। SMT सॉल्वर ऐसे उपकरण हैं जिनका लक्ष्य इनपुट के व्यावहारिक सबसेट के लिए SMT समस्या को हल करना है। Z3 और cvc5 जैसे SMT सॉल्वर का उपयोग कंप्यूटर विज्ञान में अनुप्रयोगों की एक विस्तृत श्रृंखला के लिए बिल्डिंग ब्लॉक के रूप में किया गया है, जिसमें स्वचालित प्रमेय सिद्ध करना, प्रोग्राम विश्लेषण, प्रोग्राम सत्यापन और सॉफ़्टवेयर परीक्षण सम्मिलित हैं।
चूँकि बूलियन संतुष्टि पहले से ही एनपी-पूर्ण है, SMT समस्या सामान्यतः एनपी-हार्ड है, और कई सिद्धांतों के लिए यह अनिर्णीत है। शोधकर्ता अध्ययन करते हैं कि कौन से सिद्धांत या सिद्धांतों के उपसमुच्चय एक निर्णायक SMT समस्या और निर्णायक स्थितियों की कम्प्यूटेशनल सम्मिश्रता को उत्त्पन्न करते हैं। परिणामी निर्णय प्रक्रियाएँ प्रायः सीधे SMT सॉल्वर में लागू की जाती हैं; उदाहरण के लिए, प्रेस्बर्गर अंकगणित की निर्णायकता देखें। SMT को एक बाधा संतुष्टि समस्या के रूप में सोचा जा सकता है और इस प्रकार कन्सट्रैन्ट प्रोग्रामिंग के लिए एक निश्चित औपचारिक दृष्टिकोण माना जा सकता है।
मूल शब्दावली
औपचारिक रूप से कहें तो, एक SMT उदाहरण प्रथम-क्रम तर्क में एक सूत्र है, जहां कुछ फ़ंक्शन और विधेय प्रतीकों की अतिरिक्त व्याख्याएं होती हैं, और SMT यह निर्धारित करने की समस्या है कि क्या ऐसा सूत्र संतोषजनक है। दूसरे शब्दों में, बूलियन संतुष्टि समस्या (SAT) के एक उदाहरण की कल्पना करें जिसमें कुछ बाइनरी वैरिएबल को गैर-बाइनरी वैरिएबल के उपयुक्त सेट पर विधेय द्वारा प्रतिस्थापित किया जाता है। एक विधेय गैर-बाइनरी चर का एक द्विआधारी-मूल्यवान फ़ंक्शन है। उदाहरण विधेय में रैखिक असमानताएँ (उदाहरण के लिए, ) या बिना व्याख्या किए गए शब्दों और फ़ंक्शन प्रतीकों वाली समानताएं सम्मिलित हैं (उदाहरण के लिए, जहां दो तर्कों का कुछ अनिर्दिष्ट कार्य है)। इन विधेयों को निर्दिष्ट प्रत्येक संबंधित सिद्धांत के अनुसार वर्गीकृत किया गया है। उदाहरण के लिए, वास्तविक चर पर रैखिक असमानताओं का मूल्यांकन रैखिक वास्तविक अंकगणित के सिद्धांत के नियमों का उपयोग करके किया जाता है, जबकि गैर-व्याख्यायित शब्दों और फ़ंक्शन प्रतीकों को सम्मिलित करने वाले विधेय का मूल्यांकन समानता के साथ गैर-व्याख्यायित कार्यों के सिद्धांत के नियमों का उपयोग करके किया जाता है (कभी-कभी इसे रिक्त सिद्धांत के रूप में जाना जाता है) ). अन्य सिद्धांतों में सरणियों और सूची संरचनाओं के सिद्धांत (कंप्यूटर प्रोग्रामों के मॉडलिंग और सत्यापन के लिए उपयोगी), और बिट वैक्टर के सिद्धांत (मॉडलिंग और हार्डवेयर डिजाइन के सत्यापन में उपयोगी) सम्मिलित हैं। उप-सिद्धांत भी संभव हैं: उदाहरण के लिए, अंतर तर्क रैखिक अंकगणित का एक उप-सिद्धांत है जिसमें प्रत्येक असमानता को चर और और स्थिरांक के लिए रूप तक सीमित रखा जाता है।
अधिकांश SMT सॉल्वर अपने तर्कों के केवल क्वांटिफायर-मुक्त अंशों का समर्थन करते हैं।
अभिव्यंजक घात
एक SMT उदाहरण एक बूलियन SAT उदाहरण का सामान्यीकरण है जिसमें चर के विभिन्न सेटों को विभिन्न अंतर्निहित सिद्धांतों से विधेय द्वारा प्रतिस्थापित किया जाता है। SMT सूत्र बूलियन SAT सूत्रों की तुलना में कहीं अधिक समृद्ध मॉडलिंग लैंग्वेज प्रदान करते हैं। उदाहरण के लिए, एक SMT सूत्र किसी को बिट स्तर के बजाय शब्द पर माइक्रोप्रोसेसर के डेटापथ संचालन को मॉडल करने की अनुमति देता है।
तुलनात्मक रूप से, आंसर सेट प्रोग्रामिंग भी विधेय पर बेस्ड है (अधिक सटीक रूप से, परमाणु सूत्र से निर्मित परमाणु वाक्यों पर)। SMT के विपरीत, उत्तर-सेट कार्यक्रमों में क्वांटिफायर नहीं होते हैं, और रैखिक अंकगणित या अंतर तर्क जैसी बाधाओं को आसानी से व्यक्त नहीं कर सकते हैं - एएसपी बूलियन समस्याओं के लिए सबसे उपयुक्त है जो अबाधित कार्यों के मुक्त सिद्धांत को कम करते हैं। एएसपी में बिटवेक्टर के रूप में 32-बिट पूर्णांकों को लागू करने में उन्हीं समस्याओं का सामना करना पड़ता है जिनका प्रारंभिक SMT सॉल्वरों को सामना करना पड़ा था: x+y=y+x जैसी "स्पष्ट" समरूपता निकालना मुश्किल है।
कन्सट्रैन्ट लॉजिक प्रोग्रामिंग रैखिक अंकगणितीय बाधाओं के लिए समर्थन प्रदान करती है, लेकिन एक पूरी तरह से अलग सैद्धांतिक ढांचे के भीतर। उच्च-क्रम तर्क में सूत्रों को हल करने के लिए SMT सॉल्वरों को भी बढ़ाया गया है।[1]
सॉल्वर दृष्टिकोण
SMT उदाहरणों को हल करने के प्रारंभिक प्रयासों में उन्हें बूलियन SAT उदाहरणों में अनुवाद करना सम्मिलित था (उदाहरण के लिए, एक 32-बिट पूर्णांक चर को उचित वजन के साथ 32 एकल-बिट चर द्वारा एन्कोड किया जाएगा और 'प्लस' जैसे शब्द-स्तरीय संचालन को निम्न द्वारा प्रतिस्थापित किया जाएगा- बिट्स पर लेवल लॉजिक ऑपरेशंस) और इस फॉर्मूले को बूलियन SAT सॉल्वर में पास करना। इस दृष्टिकोण, जिसे उत्सुक दृष्टिकोण के रूप में जाना जाता है, की अपनी खूबियां हैं: SMT फॉर्मूला को समकक्ष बूलियन SAT फॉर्मूला में पूर्व-प्रसंस्करण द्वारा उपस्थित बूलियन SAT सॉल्वरों का उपयोग "जैसा है" किया जा सकता है और समय के साथ उनके प्रदर्शन और क्षमता में सुधार किया जा सकता है। दूसरी ओर, अंतर्निहित सिद्धांतों के उच्च-स्तरीय शब्दार्थ के नुकसान का मतलब है कि बूलियन SAT सॉल्वर को "स्पष्ट" तथ्यों (जैसे कि पूर्णांक जोड़ के लिए ) की खोज के लिए आवश्यकता से अधिक कठिन काम करना पड़ता है।) इस अवलोकन से कई SMT सॉल्वरों का विकास हुआ जो डीपीएलएल-शैली खोज के बूलियन तर्क को सिद्धांत-विशिष्ट सॉल्वरों (टी-सॉल्वर्स) के साथ मजबूती से एकीकृत करते हैं जो किसी दिए गए सिद्धांत से विधेय के संयोजन (एएनडी) को संभालते हैं। इस दृष्टिकोण को लेजी दृष्टिकोण के रूप में जाना जाता है.
डब किया गया डीपीएलएल(टी),[2] यह आर्किटेक्चर डीपीएलएल-बेस्ड SAT सॉल्वर को बूलियन तर्क की जिम्मेदारी देता है, जो बदले में, एक अच्छी तरह से परिभाषित इंटरफ़ेस के माध्यम से सिद्धांत टी के लिए एक सॉल्वर के साथ बातचीत करता है। सिद्धांत सॉल्वर को केवल SAT सॉल्वर से पारित सिद्धांत विधेय के संयोजन की व्यवहार्यता की जांच करने के बारे में चिंता करने की ज़रूरत है क्योंकि यह सूत्र के बूलियन सर्च स्थान की खोज करता है। हालाँकि, इस एकीकरण के अच्छी तरह से काम करने के लिए, सिद्धांत समाधानकर्ता को प्रसार और संघर्ष विश्लेषण में भाग लेने में सक्षम होना चाहिए, अर्थात, उसे पहले से स्थापित तथ्यों से नए तथ्यों का अनुमान लगाने में सक्षम होना चाहिए, साथ ही सैद्धांतिक विरोधिता उत्पन्न होने पर अव्यवहार्यता की संक्षिप्त व्याख्या प्रदान करना। दूसरे शब्दों में, थ्योरी सॉल्वर वृद्धिशील और बैकट्रैकेबल होना चाहिए।
अनिर्णीत सिद्धांतों के लिए SMT
अधिकांश सामान्य SMT दृष्टिकोण निर्णायक सिद्धांतों का समर्थन करते हैं। हालाँकि, कई वास्तविक दुनिया प्रणालियाँ, जैसे कि एक विमान और उसका व्यवहार, केवल पारमार्थिक फंक्शन से जुड़े वास्तविक संख्याओं पर गैर-रैखिक अंकगणित के माध्यम से मॉडलिंग की जा सकती हैं। यह तथ्य SMT समस्या के गैर-रेखीय सिद्धांतों तक विस्तार को प्रेरित करता है, जैसे यह निर्धारित करना कि क्या निम्नलिखित समीकरण संतोषजनक है:
जहाँ
हालाँकि, ऐसी समस्याएँ सामान्यतः अनिर्णीत होती हैं। (दूसरी ओर, वास्तविक बंद क्षेत्रों का सिद्धांत, और इस प्रकार वास्तविक संख्याओं का पूर्ण प्रथम क्रम सिद्धांत, क्वांटिफायर उन्मूलन का उपयोग करके तय किया जा सकता है। यह अल्फ्रेड टार्स्की के कारण है।) जोड़ के साथ प्राकृतिक संख्याओं का पहला क्रम सिद्धांत ( लेकिन गुणा नहीं), जिसे प्रेस्बर्गर अंकगणित कहा जाता है, भी निर्णय योग्य है। चूँकि स्थिरांकों द्वारा गुणन को नेस्टेड परिवर्धन के रूप में कार्यान्वित किया जा सकता है, कई कंप्यूटर प्रोग्रामों में अंकगणित को प्रेसबर्गर अंकगणित का उपयोग करके व्यक्त किया जा सकता है, जिसके परिणामस्वरूप निर्णायक सूत्र प्राप्त होते हैं।
वास्तविकताओं पर अनिर्णीत अंकगणितीय सिद्धांतों से सिद्धांत परमाणुओं के बूलियन संयोजनों को संबोधित करने वाले SMT सॉल्वर के उदाहरण एबीएसॉल्वर हैं,[3] जो एक गैर-रेखीय अनुकूलन पैकेट के साथ एक शास्त्रीय डीपीएलएल (टी) आर्किटेक्चर को (आवश्यक रूप से अपूर्ण) अधीनस्थ सिद्धांत सॉल्वर और आईएसएटी के रूप में नियोजित करता है। , डीपीएलएल SAT-समाधान और अंतराल बाधा प्रसार के एकीकरण पर निर्माण, जिसे आईएसएटी एल्गोरिदम कहा जाता है।[4]
सॉल्वर
नीचे दी गई तालिका कई उपलब्ध SMT सॉल्वरों की कुछ विशेषताओं का सारांश प्रस्तुत करती है। कॉलम "SMT-LIB" SMT-LIB लैंग्वेज के साथ अनुकूलता दर्शाता है; 'हाँ' चिह्नित कई प्रणालियाँ केवल SMT-LIB के पुराने संस्करणों का समर्थन कर सकती हैं, या लैंग्वेज के लिए केवल आंशिक समर्थन प्रदान कर सकती हैं। कॉलम "CVC" CVC लैंग्वेज के लिए समर्थन दर्शाता है। कॉलम "DIMACS" DIMACS प्रारूप के लिए समर्थन दर्शाता है।
परियोजनाएं न केवल सुविधाओं और प्रदर्शन में भिन्न होती हैं, बल्कि आसपास के समुदाय की व्यवहार्यता, परियोजना में इसकी चल रही रुचि और दस्तावेज़ीकरण, सुधार, परीक्षण और संवर्द्धन में योगदान करने की क्षमता में भी भिन्न होती हैं।
मानकीकरण और SMT-COMP सॉल्वर प्रतियोगिता
प्लेटफ़ॉर्म | विशेषताएँ | टिप्पणियाँ | |||||||
---|---|---|---|---|---|---|---|---|---|
नाम | ओएस | लाइसेंस | SMT-LIB | CVC | डायमैक | अंतर्निर्मित सिद्धांत | एपीआई | SMT-कॉम्प[1] | |
ABsolver | लिनक्स | CPL | v1.2 | No | Yes | रैखिक अंकगणित, अरेखीय अंकगणित | C++ | no | डीपीएलएल-बेस्ड |
Alt-Ergo | लिनक्स , मैक ओएस , विंडोज़ | CeCILL-C (roughly equivalent to LGPL) | partial v1.2 and v2.0 | No | No | रिक्त सिद्धांत , रैखिक पूर्णांक और तर्कसंगत अंकगणित, गैर-रेखीय अंकगणित, बहुरूपी ऐरे , प्रगणित डेटा प्रकार , एसी प्रतीक , बिटवेक्टर , रिकॉर्ड डेटा प्रकार , क्वांटिफायर | OCaml | 2008 | बहुरूपी प्रथम-क्रम इनपुट लैंग्वेज à la ML, SAT-सॉल्वर बेस्ड, तर्क मॉड्यूल सिद्धांतों के लिए शोस्ताक-जैसे और नेल्सन-ओपेन जैसे दृष्टिकोणों को जोड़ती है |
Barcelogic | लिनक्स | Proprietary | v1.2 | खोखला सिद्धांत , अंतर तर्क | C++ | 2009 | डीपीएलएल-बेस्ड, सर्वांगसमता समापन | ||
Beaver | लिनक्स , विंडोज़ | BSD | v1.2 | No | No | बिटवेक्टर | OCaml | 2009 | SAT-सॉल्वर बेस्ड |
Boolector | लिनक्स | MIT | v1.2 | No | No | बिटवेक्टर , ऐरे | C | 2009 | SAT-सॉल्वर बेस्ड |
CVC3 | लिनक्स | BSD | v1.2 | Yes | रिक्त सिद्धांत , रैखिक अंकगणित, ऐरे, टुपल्स, प्रकार, रिकॉर्ड, बिटवेक्टर, क्वांटिफायर | C/C++ | 2010 | HOL को प्रूफ़ आउटपुट | |
CVC4 | लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी | BSD | Yes | Yes | तर्कसंगत और पूर्णांक रैखिक अंकगणित, ऐरे, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, और अबाधित फ़ंक्शन प्रतीकों पर समानता | C++ | 2021 | संस्करण 1.8 मई 2021 में जारी किया गया | |
CVC5 | लिनक्स , मैक ओएस , विंडोज़ | BSD | Yes | Yes | तर्कसंगत और पूर्णांक रैखिक अंकगणित, ऐरे, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, अनुक्रम, बैग, और अबाधित फ़ंक्शन प्रतीकों पर समानता | C++, Python, Java | 2021 | संस्करण 1.0 अप्रैल 2022 में जारी किया गया | |
Decision Procedure Toolkit (DPT) | लिनक्स | Apache | No | OCaml | no | डीपीएलएल-बेस्ड | |||
iSAT | लिनक्स | Proprietary | No | अरेखीय अंकगणित | no | डीपीएलएल-बेस्ड | |||
MathSAT | लिनक्स , मैक ओएस , विंडोज़ | Proprietary | Yes | Yes | रिक्त सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, ऐरे | C/C++, Python, Java | 2010 | डीपीएलएल-बेस्ड | |
MiniSmt | लिनक्स | LGPL | partial v2.0 | अरेखीय अंकगणित | OCaml | 2010 | SAT-सॉल्वर बेस्ड, Yices-बेस्ड | ||
Norn | स्ट्रिंग बाधाओं के लिए SMT सॉल्वर | ||||||||
लिनक्स | |||||||||
OpenCog | लिनक्स | AGPL | No | No | No | संभाव्य तर्क , अंकगणित। संबंधपरक मॉडल | C++, Scheme, Python | no | सबग्राफ समरूपता |
OpenSMT | लिनक्स , मैक ओएस , विंडोज़ | GPLv3 | partial v2.0 | Yes | रिक्त सिद्धांत , अंतर, रैखिक अंकगणित, बिटवेक्टर | C++ | 2011 | लेजी SMT सॉल्वर | |
raSAT | लिनक्स | GPLv3 | v2.0 | वास्तविक और पूर्णांक अरेखीय अंकगणित | 2014, 2015 | परीक्षण और मध्यवर्ती मूल्य प्रमेय के साथ अंतराल बाधा प्रसार का विस्तार | |||
SatEEn | ? | Proprietary | v1.2 | रैखिक अंकगणित, अंतर तर्क | none | 2009 | |||
SMTInterpol | लिनक्स , मैक ओएस , विंडोज़ | LGPLv3 | v2.5 | अव्याख्यायित फलन, रैखिक वास्तविक अंकगणित, और रैखिक पूर्णांक अंकगणित | Java | 2012 | उच्च गुणवत्ता, कॉम्पैक्ट इंटरपोलेंट उत्पन्न करने पर ध्यान केंद्रित करता है। | ||
SMCHR | लिनक्स , मैक ओएस , विंडोज़ | GPLv3 | No | No | No | रैखिक अंकगणित, अरेखीय अंकगणित, हीप | C | no | बाधा प्रबंधन नियमों का उपयोग करके नए सिद्धांतों को लागू कर सकते हैं । |
SMT-RAT | लिनक्स , मैक ओएस | MIT | v2.0 | No | No | रैखिक अंकगणित, अरेखीय अंकगणित | C++ | 2015 | रणनीतिक और समानांतर SMT समाधान के लिए टूलबॉक्स जिसमें SMT अनुरूप कार्यान्वयन का संग्रह सम्मिलित है। |
SONOLAR | लिनक्स , विंडोज़ | Proprietary | partial v2.0 | बिटवेक्टर | C | 2010 | SAT-सॉल्वर बेस्ड | ||
Spear | लिनक्स , मैक ओएस , विंडोज़ | Proprietary | v1.2 | बिटवेक्टर | 2008 | ||||
STP | लिनक्स , ओपनबीएसडी , विंडोज , मैक ओएस | MIT | partial v2.0 | Yes | No | बिटवेक्टर, ऐरे | C, C++, Python, OCaml, Java | 2011 | SAT-सॉल्वर बेस्ड |
SWORD | लिनक्स | Proprietary | v1.2 | बिटवेक्टर | 2009 | ||||
UCLID | लिनक्स | BSD | No | No | No | रिक्त सिद्धांत , रैखिक अंकगणित, बिटवेक्टर, और विवश लैम्ब्डा (सरणी, यादें, कैश, आदि) | no | SAT-सॉल्वर बेस्ड, मॉस्को एमएल में लिखा गया । इनपुट लैंग्वेज एसएमवी मॉडल चेकर है। अच्छी तरह से प्रलेखित! | |
veriT | लिनक्स , ओएस एक्स | BSD | partial v2.0 | रिक्त सिद्धांत , तर्कसंगत और पूर्णांक रैखिक अंकगणित, परिमाणक, और अबाधित फ़ंक्शन प्रतीकों पर समानता | C/C++ | 2010 | SAT-सॉल्वर बेस्ड, प्रमाण प्रस्तुत कर सकते हैं | ||
Yices | लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी | GPLv3 | v2.0 | No | Yes | तर्कसंगत और पूर्णांक रैखिक अंकगणित, बिटवेक्टर, ऐरे, और अबाधित फ़ंक्शन प्रतीकों पर समानता | C | 2014 | सोर्स कोड ऑनलाइन उपलब्ध है |
Z3 Theorem Prover | लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी | MIT | v2.0 | Yes | रिक्त सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, ऐरे, डेटाटाइप, क्वांटिफायर , स्ट्रिंग्स | C/C++, .NET, OCaml, Python, Java, Haskell | 2011 | सोर्स कोड ऑनलाइन उपलब्ध है |
मानकीकरण और SMT-COMP सॉल्वर प्रतियोगिता
SMT सॉल्वरों (और स्वचालित प्रमेय प्रोवर्स, एक शब्द जिसे प्रायः समानार्थक रूप से उपयोग किया जाता है) के लिए एक मानकीकृत इंटरफ़ेस का वर्णन करने के कई प्रयास किए गए हैं। सबसे प्रमुख SMT-LIB मानक है, जो S-अभिव्यक्ति पर बेस्ड लैंग्वेज प्रदान करता है। सामान्यतः समर्थित अन्य मानकीकृत प्रारूप कई बूलियन SAT सॉल्वरों द्वारा समर्थित डीआईएमएसीएस प्रारूप हैं, और CVC प्रारूप CVC स्वचालित प्रमेय प्रोवर द्वारा उपयोग किया जाता है।
SMT-LIB प्रारूप भी कई मानकीकृत बेंचमार्क के साथ आता है और इसने SMT-COMP नामक SMT सॉल्वरों के बीच एक वार्षिक प्रतियोगिता को सक्षम किया है। प्रारंभ में, प्रतियोगिता कंप्यूटर एडेड सत्यापन सम्मेलन (सीएवी) के दौरान हुई थी,[5][6] लेकिन 2020 तक प्रतियोगिता को SMT कार्यशाला के हिस्से के रूप में आयोजित किया गया है, जो स्वचालित तर्क (आईजेसीएआर) पर अंतर्राष्ट्रीय संयुक्त सम्मेलन से संबद्ध है)।[7]
अनुप्रयोग
SMT सॉल्वर सत्यापन, प्रोग्राम की यथार्थता सिद्ध करने, प्रतीकात्मक निष्पादन के आधार पर सॉफ्टवेयर परीक्षण, और संश्लेषण के लिए, संभावित प्रोग्रमम के स्थान पर सर्च करके प्रोग्रम के भाग उत्पन्न करने के लिए उपयोगी हैं। सॉफ़्टवेयर सत्यापन के अलावा, SMT सॉल्वरों का उपयोग प्रकार के अनुमान के लिए भी किया गया है[8][9] और परमाणु उपकरण नियंत्रण में साधक के विश्वासों को मॉडलिंग करने सहित सैद्धांतिक परिदृश्यों के मॉडलिंग के लिए भी है।[10]
सत्यापन
कंप्यूटर प्रोग्रामों का कंप्यूटर समर्थित सत्यापन प्रायः SMT सॉल्वर का उपयोग करता है। यह निर्धारित करने के लिए कि क्या सभी गुण धारण किए जा सकते हैं, एक सामान्य तकनीक पूर्व शर्त, पोस्टकंडिशन, लूप स्थिति और SMT सूत्रों में दावे का अनुवाद करना है।
Z3 SMT सॉल्वर के शीर्ष पर कई सत्यापनकर्ता बनाए गए हैं। बूगी एक मध्यवर्ती सत्यापन लैंग्वेज है जो सरल अनिवार्य कार्यक्रमों की स्वचालित रूप से जाँच करने के लिए Z3 का उपयोग करती है। समवर्ती सी के लिए वीसीसी सत्यापनकर्ता बूगी का उपयोग करता है, साथ ही अनिवार्य वस्तु-बेस्ड कार्यक्रमों के लिए डैफनी, समवर्ती कार्यक्रमों के लिए चालिस और सी# के लिए स्पेक# का उपयोग करता है। F* एक निर्भरता से टाइप की जाने वाली लैंग्वेज है जो प्रमाण खोजने के लिए Z3 का उपयोग करती है; कंपाइलर इन सबूतों को प्रूफ-ले जाने वाले बाइटकोड का उत्पादन करने के लिए ले जाता है। वाइपर सत्यापन अवसंरचना सत्यापन शर्तों को Z3 में एनकोड करती है। एसबीवी लाइब्रेरी हास्केल कार्यक्रमों का SMT-बेस्ड सत्यापन प्रदान करती है, और उपयोगकर्ता को Z3, एबीसी, बूलेक्टर, CVC5, मैथसैट और येस जैसे कई सॉल्वरों में से चुनने की सुविधा देती है।
- ऑल्ट-एर्गो SMT सॉल्वर के ऊपर कई सत्यापनकर्ता भी बनाए गए हैं। यहां परिपक्व आवेदनों की सूची दी गई है:
- व्हाय3, डिडक्टिव प्रोग्राम सत्यापन के लिए एक मंच, ऑल्ट-एर्गो को अपने मुख्य कहावत के रूप में उपयोग करता है;
- कैविएट, सीईए द्वारा विकसित और एयरबस द्वारा उपयोग किया जाने वाला एक सी-सत्यापनकर्ता; ऑल्ट-एर्गो को इसके हालिया विमानों में से एक की योग्यता DO-178C में सम्मिलित किया गया था;
- फ्रैमा-सी, सी-कोड का विश्लेषण करने के लिए एक ढांचा, जेसी और डब्ल्यूपी प्लगइन्स ("डिडक्टिव प्रोग्राम वेरिफिकेशन" के लिए समर्पित) में ऑल्ट-एर्गो का उपयोग करता है;
- स्पार्क 2014 में कुछ दावों के सत्यापन को स्वचालित करने के लिए स्पार्क CVC4 और ऑल्ट-एर्गो (GNATprove के पीछे) का उपयोग करता है;
- एटेलियर-बी अपने मुख्य प्रोवर के बजाय ऑल्ट-एर्गो का उपयोग कर सकता है (एएनआर बीवेयर प्रोजेक्ट बेंचमार्क पर सफलता 84% से बढ़कर 98% हो गई है);
- रॉडिन, सिस्टरेल द्वारा विकसित एक बी-मेथड फ्रेमवर्क, ऑल्ट-एर्गो को बैक-एंड के रूप में उपयोग कर सकता है;
- क्यूबिकल, सरणी-बेस्ड संक्रमण प्रणालियों की सुरक्षा गुणों की पुष्टि के लिए एक खुला सोर्स मॉडल चेकर।
- ईज़ीक्रिप्ट, प्रतिकूल कोड के साथ संभाव्य संगणनाओं के संबंधपरक गुणों के बारे में तर्क करने के लिए एक टूलसेट।
कई SMT सॉल्वर SMTLIB2 नामक एक सामान्य इंटरफ़ेस प्रारूप लागू करते हैं (ऐसी फ़ाइलों में सामान्यतः एक्सटेंशन ".smt2
" होता है)। लिक्विडहास्केल उपकरण हास्केल के लिए एक परिशोधन प्रकार-बेस्ड सत्यापनकर्ता लागू करता है जो किसी भी SMTLIB2 अनुरूप सॉल्वर का उपयोग कर सकता है, जैसे cvc5, MathSat, या Z3।
सांकेतिक-निष्पादन बेस्ड विश्लेषण एवं परीक्षण
SMT सॉल्वरों का एक महत्वपूर्ण एप्लीकेशन प्रोग्राम के विश्लेषण और परीक्षण के लिए प्रतीकात्मक निष्पादन है (उदाहरण के लिए, कॉन्कोलिक परीक्षण), जिसका उद्देश्य विशेष रूप से सुरक्षा कमजोरियों का पता लगाना है। इस श्रेणी के उदाहरण टूल में माइक्रोसॉफ्ट रिसर्च से SAGE, KLEE, S2E और ट्राइटनशामिल हैं। SMT सॉल्वर जिनका उपयोग प्रतीकात्मक-निष्पादन अनुप्रयोगों के लिए किया गया है, उनमें Z3, एसटीपी आर्काइव्ड 2015-04-06 वेबैक मशीन, सॉल्वर का Z3str समहू और बूलेक्टर सम्मिलित हैं।
यह भी देखें
- आंसर सेट प्रोग्रामिंग
- ऑटोमेटेड थ्योरम प्रोविंग
- SAT सॉल्वर
- फर्स्ट-आर्डर लॉजिक
- थ्योरी ऑफ़ पुरे इक्वलिटी
टिप्पणियाँ
- ↑ 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.
- ↑ 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
- ↑ 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
- ↑ 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
- ↑ 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.
- ↑ 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.
- ↑ "SMT-COMP 2020". SMT-COMP (in English). Retrieved 2020-10-19.
- ↑ 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.
- ↑ Loncaric, Calvin, et al. "A practical framework for type inference error explanation." ACM SIGPLAN Notices 51.10 (2016): 781-799.
- ↑ 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.
संदर्भ
- Barrett, C.; Sebastiani, R.; Seshia, S.; Tinelli, C. (2009). "Satisfiability Modulo Theories". In Biere, A.; Heule, M.J.H.; van Maaren, H.; Walsh, T. (eds.). Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications. Vol. 185. IOS Press. pp. 825–885. ISBN 9781607503767.
- Ganesh, Vijay (September 2007). Decision Procedures for Bit-Vectors, Arrays and Integers (PDF) (PhD). Computer Science Department, Stanford University.
- Jha, Susmit; Limaye, Rhishikesh; Seshia, Sanjit A. (2009). "Beaver: Engineering an efficient SMT solver for bit-vector arithmetic". Proceedings of 21st International Conference on Computer-Aided Verification. pp. 668–674. doi:10.1007/978-3-642-02658-4_53. ISBN 978-3-642-02658-4.
- Bryant, R.E.; German, S.M.; Velev, M.N. (1999). "Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions" (PDF). Analytic Tableaux and Related Methods. pp. 1–13., pp. , .
- Davis, M.; Putnam, H. (1960). "A Computing Procedure for Quantification Theory". Journal of the Association for Computing Machinery. 7 (3): 201–215. doi:10.1145/321033.321034. S2CID 31888376.
- Davis, M.; Logemann, G.; Loveland, D. (1962). "A Machine Program for Theorem-Proving". Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. S2CID 15866917.
- Kroening, D.; Strichman, O. (2008). Decision Procedures — an algorithmic point of view. Theoretical Computer Science series. Springer. ISBN 978-3-540-74104-6.
- Nam, G.-J.; Sakallah, K.A.; Rutenbar, R. (2002). "A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability". IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 21 (6): 674–684. doi:10.1109/TCAD.2002.1004311.
- SMT-LIB: The Satisfiability Modulo Theories Library
- SMT-COMP: The Satisfiability Modulo Theories Competition
- Decision procedures - an algorithmic point of view
- Sebastiani, R. (2007). "Lazy Satisfiability Modulo Theories". Journal on Satisfiability, Boolean Modeling and Computation. 3 (3–4): 141–224. CiteSeerX 10.1.1.100.221. doi:10.3233/SAT190034.
- Yurichev, D. "Quick introduction into SAT/SMT solvers and symbolic execution" (PDF).
- This article is adapted from a column in the ACM SIGDA e-newsletter by Prof. Karem Sakallah. Original text is available here