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

From Vigyanwiki
No edit summary
No edit summary
 
(4 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}}


[[कंप्यूटर विज्ञान]] और [[गणितीय तर्क]] में, '''[[संतुष्टि]] मॉड्यूल सिद्धांत (एसएमटी)''' यह निर्धारित करने की समस्या है कि कोई गणितीय सूत्र संतोषजनक है या नहीं। यह [[बूलियन संतुष्टि समस्या]] (SAT) को वास्तविक संख्याओं, [[पूर्णांकों]] और/या सूचियों, ऐरे, बिट वैक्टर और स्ट्रिंग्स जैसी विभिन्न डेटा संरचनाओं को शामिल करने वाले अधिक जटिल सूत्रों में सामान्यीकृत करता है। यह नाम इस तथ्य से लिया गया है कि इन अभिव्यक्तियों की व्याख्या समानता के साथ प्रथम-क्रम तर्क में एक निश्चित औपचारिक सिद्धांत ("मॉड्यूलो") के भीतर की जाती है (अक्सर क्वांटिफायर की अनुमति नहीं दी जाती है)। एसएमटी सॉल्वर ऐसे उपकरण हैं जिनका लक्ष्य इनपुट के व्यावहारिक सबसेट के लिए एसएमटी समस्या को हल करना है। Z3 और cvc5 जैसे '''एसएमटी सॉल्वर''' का उपयोग कंप्यूटर विज्ञान में अनुप्रयोगों की एक विस्तृत श्रृंखला के लिए बिल्डिंग ब्लॉक के रूप में किया गया है, जिसमें स्वचालित प्रमेय सिद्ध करना, प्रोग्राम विश्लेषण, प्रोग्राम सत्यापन और सॉफ़्टवेयर परीक्षण शामिल हैं।
[[कंप्यूटर विज्ञान]] और [[गणितीय तर्क]] में, '''[[संतुष्टि]] मॉड्यूल सिद्धांत (SMT)''' यह निर्धारित करने की समस्या है कि कोई गणितीय सूत्र संतोषजनक है या नहीं। यह [[बूलियन संतुष्टि समस्या]] (SAT) को वास्तविक संख्याओं, [[पूर्णांकों]] और/या सूचियों, ऐरे, बिट वैक्टर और स्ट्रिंग्स जैसी विभिन्न डेटा संरचनाओं को सम्मिलित करने वाले अधिक जटिल सूत्रों में सामान्यीकृत करता है। यह नाम इस तथ्य से लिया गया है कि इन अभिव्यक्तियों की व्याख्या समानता के साथ प्रथम-क्रम तर्क में एक निश्चित औपचारिक सिद्धांत ("मॉड्यूलो") के भीतर की जाती है (प्रायः क्वांटिफायर की अनुमति नहीं दी जाती है)। SMT सॉल्वर ऐसे उपकरण हैं जिनका लक्ष्य इनपुट के व्यावहारिक सबसेट के लिए SMT समस्या को हल करना है। Z3 और cvc5 जैसे '''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) के एक उदाहरण की कल्पना करें जिसमें कुछ बाइनरी वैरिएबल को गैर-बाइनरी वैरिएबल के उपयुक्त सेट पर विधेय द्वारा प्रतिस्थापित किया जाता है। एक विधेय गैर-बाइनरी चर का एक द्विआधारी-मूल्यवान फ़ंक्शन है। उदाहरण विधेय में रैखिक असमानताएँ (उदाहरण के लिए, <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 सूत्र किसी को बिट स्तर के बजाय शब्द पर [[माइक्रोप्रोसेसर]] के डेटापथ संचालन को मॉडल करने की अनुमति देता है।


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


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


==सॉल्वर दृष्टिकोण==
==सॉल्वर दृष्टिकोण==
एसएमटी उदाहरणों को हल करने के शुरुआती प्रयासों में उन्हें बूलियन एसएटी उदाहरणों में अनुवाद करना शामिल था (उदाहरण के लिए, एक 32-बिट पूर्णांक चर को उचित वजन के साथ 32 एकल-बिट चर द्वारा एन्कोड किया जाएगा और 'प्लस' जैसे शब्द-स्तरीय संचालन को निम्न द्वारा प्रतिस्थापित किया जाएगा- बिट्स पर लेवल लॉजिक ऑपरेशंस) और इस फॉर्मूले को बूलियन एसएटी सॉल्वर में पास करना। इस दृष्टिकोण, जिसे उत्सुक दृष्टिकोण के रूप में जाना जाता है, की अपनी खूबियां हैं: एसएमटी फॉर्मूला को समकक्ष बूलियन एसएटी फॉर्मूला में पूर्व-प्रसंस्करण द्वारा मौजूदा बूलियन एसएटी सॉल्वरों का उपयोग "जैसा है" किया जा सकता है और समय के साथ उनके प्रदर्शन और क्षमता में सुधार किया जा सकता है। दूसरी ओर, अंतर्निहित सिद्धांतों के उच्च-स्तरीय शब्दार्थ के नुकसान का मतलब है कि बूलियन एसएटी सॉल्वर को "स्पष्ट" तथ्यों (जैसे कि पूर्णांक जोड़ के लिए <math>x + y = y + x</math>) की खोज के लिए आवश्यकता से अधिक कठिन काम करना पड़ता है।) इस अवलोकन से कई एसएमटी सॉल्वरों का विकास हुआ जो डीपीएलएल-शैली खोज के बूलियन तर्क को सिद्धांत-विशिष्ट सॉल्वरों (टी-सॉल्वर्स) के साथ मजबूती से एकीकृत करते हैं जो किसी दिए गए सिद्धांत से विधेय के संयोजन (एएनडी) को संभालते हैं। इस दृष्टिकोण को लेजी दृष्टिकोण के रूप में जाना जाता है.
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> यह आर्किटेक्चर डीपीएलएल-बेस्ड एसएटी सॉल्वर को बूलियन तर्क की जिम्मेदारी देता है, जो बदले में, एक अच्छी तरह से परिभाषित इंटरफ़ेस के माध्यम से सिद्धांत टी के लिए एक सॉल्वर के साथ बातचीत करता है। सिद्धांत सॉल्वर को केवल SAT सॉल्वर से पारित सिद्धांत विधेय के संयोजन की व्यवहार्यता की जांच करने के बारे में चिंता करने की ज़रूरत है क्योंकि यह सूत्र के बूलियन सर्च स्थान की खोज करता है। हालाँकि, इस एकीकरण के अच्छी तरह से काम करने के लिए, सिद्धांत समाधानकर्ता को प्रसार और संघर्ष विश्लेषण में भाग लेने में सक्षम होना चाहिए, अर्थात, उसे पहले से स्थापित तथ्यों से नए तथ्यों का अनुमान लगाने में सक्षम होना चाहिए, साथ ही सैद्धांतिक विरोधिता उत्पन्न होने पर अव्यवहार्यता की संक्षिप्त व्याख्या प्रदान करना। दूसरे शब्दों में, थ्योरी सॉल्वर वृद्धिशील और बैकट्रैकेबल होना चाहिए।
  }}</ref> यह आर्किटेक्चर डीपीएलएल-बेस्ड SAT सॉल्वर को बूलियन तर्क की जिम्मेदारी देता है, जो बदले में, एक अच्छी तरह से परिभाषित इंटरफ़ेस के माध्यम से सिद्धांत टी के लिए एक सॉल्वर के साथ बातचीत करता है। सिद्धांत सॉल्वर को केवल SAT सॉल्वर से पारित सिद्धांत विधेय के संयोजन की व्यवहार्यता की जांच करने के बारे में चिंता करने की ज़रूरत है क्योंकि यह सूत्र के बूलियन सर्च स्थान की खोज करता है। हालाँकि, इस एकीकरण के अच्छी तरह से काम करने के लिए, सिद्धांत समाधानकर्ता को प्रसार और संघर्ष विश्लेषण में भाग लेने में सक्षम होना चाहिए, अर्थात, उसे पहले से स्थापित तथ्यों से नए तथ्यों का अनुमान लगाने में सक्षम होना चाहिए, साथ ही सैद्धांतिक विरोधिता उत्पन्न होने पर अव्यवहार्यता की संक्षिप्त व्याख्या प्रदान करना। दूसरे शब्दों में, थ्योरी सॉल्वर वृद्धिशील और बैकट्रैकेबल होना चाहिए।


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


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


वास्तविकताओं पर अनिर्णीत अंकगणितीय सिद्धांतों से सिद्धांत परमाणुओं के बूलियन संयोजनों को संबोधित करने वाले एसएमटी सॉल्वर के उदाहरण एबीएसॉल्वर हैं,<ref>{{Citation
वास्तविकताओं पर अनिर्णीत अंकगणितीय सिद्धांतों से सिद्धांत परमाणुओं के बूलियन संयोजनों को संबोधित करने वाले 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>{{Citation
  }}</ref> जो एक गैर-रेखीय अनुकूलन पैकेट के साथ एक शास्त्रीय डीपीएलएल (टी) आर्किटेक्चर को (आवश्यक रूप से अपूर्ण) अधीनस्थ सिद्धांत सॉल्वर और आईएसएटी के रूप में नियोजित करता है। , डीपीएलएल SAT-समाधान और अंतराल बाधा प्रसार के एकीकरण पर निर्माण, जिसे आईएसएटी एल्गोरिदम कहा जाता है।<ref>{{Citation
     | first1 = M.
     | first1 = M.
     | last1 = Fränzle
     | last1 = Fränzle
Line 85: Line 85:


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


परियोजनाएं न केवल सुविधाओं और प्रदर्शन में भिन्न होती हैं, बल्कि आसपास के समुदाय की व्यवहार्यता, परियोजना में इसकी चल रही रुचि और दस्तावेज़ीकरण, सुधार, परीक्षण और संवर्द्धन में योगदान करने की क्षमता में भी भिन्न होती हैं।
परियोजनाएं न केवल सुविधाओं और प्रदर्शन में भिन्न होती हैं, बल्कि आसपास के समुदाय की व्यवहार्यता, परियोजना में इसकी चल रही रुचि और दस्तावेज़ीकरण, सुधार, परीक्षण और संवर्द्धन में योगदान करने की क्षमता में भी भिन्न होती हैं।
Line 98: Line 98:
! style="background:#ffdead;" | ओएस
! style="background:#ffdead;" | ओएस
! style="background:#ffdead;" | लाइसेंस
! style="background:#ffdead;" | लाइसेंस
! style="background:#ffdead;" | एसएमटी-एलआईबी
! style="background:#ffdead;" | SMT-LIB
! style="background:#ffdead;" | सीवीसी
! 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;" | एसएमटी-कॉम्प[http://www.smtcomp.org/]
! style="background:#ffdead;" | SMT-कॉम्प[http://www.smtcomp.org/]
!
!
|-
|-
| एबीसॉल्वर
| ABsolver
| लिनक्स
| लिनक्स
| [[Common Public License|CPL]]
| [[Common Public License|CPL]]
Line 117: Line 117:
| डीपीएलएल-बेस्ड
| डीपीएलएल-बेस्ड
|-
|-
| [[Alt-Ergo|ऑल्ट-एर्गो]]
| [[Alt-Ergo]]
| लिनक्स , मैक ओएस , विंडोज़
| लिनक्स , मैक ओएस , विंडोज़
| [[CeCILL-C]] (roughly equivalent to [[LGPL]])
| [[CeCILL-C]] (roughly equivalent to [[LGPL]])
Line 123: Line 123:
| {{no}}
| {{no}}
| {{no}}
| {{no}}
| खाली सिद्धांत , रैखिक पूर्णांक और तर्कसंगत अंकगणित, गैर-रेखीय अंकगणित, बहुरूपी सरणियाँ , प्रगणित डेटा प्रकार , एसी प्रतीक , बिटवेक्टर , रिकॉर्ड डेटा प्रकार , क्वांटिफायर
| रिक्त सिद्धांत , रैखिक पूर्णांक और तर्कसंगत अंकगणित, गैर-रेखीय अंकगणित, बहुरूपी ऐरे , प्रगणित डेटा प्रकार , एसी प्रतीक , बिटवेक्टर , रिकॉर्ड डेटा प्रकार , क्वांटिफायर
| [[OCaml]]
| [[OCaml]]
| 2008
| 2008
|बहुरूपी प्रथम-क्रम इनपुट लैंग्वेज à la ML, एसएटी-सॉल्वर बेस्ड, तर्क मॉड्यूल सिद्धांतों के लिए शोस्ताक-जैसे और नेल्सन-ओपेन जैसे दृष्टिकोणों को जोड़ती है
|बहुरूपी प्रथम-क्रम इनपुट लैंग्वेज à la ML, SAT-सॉल्वर बेस्ड, तर्क मॉड्यूल सिद्धांतों के लिए शोस्ताक-जैसे और नेल्सन-ओपेन जैसे दृष्टिकोणों को जोड़ती है
|-
|-
| बार्सेलॉजिक
| Barcelogic
| लिनक्स
| लिनक्स
| Proprietary
| Proprietary
Line 139: Line 139:
| डीपीएलएल-बेस्ड, सर्वांगसमता समापन
| डीपीएलएल-बेस्ड, सर्वांगसमता समापन
|-
|-
| बीवर
| Beaver
| लिनक्स , विंडोज़
| लिनक्स , विंडोज़
| [[BSD licenses|BSD]]
| [[BSD licenses|BSD]]
Line 150: Line 150:
| SAT-सॉल्वर बेस्ड
| SAT-सॉल्वर बेस्ड
|-
|-
| बूलेक्टर
| Boolector
| लिनक्स
| लिनक्स
| [[MIT License|MIT]]
| [[MIT License|MIT]]
Line 156: Line 156:
| {{no}}
| {{no}}
| {{no}}
| {{no}}
| बिटवेक्टर , सरणियाँ
| बिटवेक्टर , ऐरे
| [[C (programming language)|C]]
| [[C (programming language)|C]]
| 2009
| 2009
| SAT-सॉल्वर बेस्ड
| SAT-सॉल्वर बेस्ड
|-
|-
| सीवीसी3
| CVC3
| लिनक्स
| लिनक्स
| [[BSD licenses|BSD]]
| [[BSD licenses|BSD]]
Line 167: Line 167:
| {{yes}}
| {{yes}}
|
|
| खाली सिद्धांत , रैखिक अंकगणित, सरणियाँ, टुपल्स, प्रकार, रिकॉर्ड, बिटवेक्टर, क्वांटिफायर
| रिक्त सिद्धांत , रैखिक अंकगणित, ऐरे, टुपल्स, प्रकार, रिकॉर्ड, बिटवेक्टर, क्वांटिफायर
| [[C (programming language)|C]]/[[C++]]
| [[C (programming language)|C]]/[[C++]]
| 2010
| 2010
| HOL को प्रूफ़ आउटपुट
| HOL को प्रूफ़ आउटपुट
|-
|-
| सीवीसी4
| CVC4
| लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी
| लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी
| [[BSD licenses|BSD]]
| [[BSD licenses|BSD]]
Line 178: Line 178:
| {{yes}}
| {{yes}}
|
|
| तर्कसंगत और पूर्णांक रैखिक अंकगणित, सरणियाँ, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, और अबाधित फ़ंक्शन प्रतीकों पर समानता
| तर्कसंगत और पूर्णांक रैखिक अंकगणित, ऐरे, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, और अबाधित फ़ंक्शन प्रतीकों पर समानता
| C++
| C++
| 2021
| 2021
| संस्करण 1.8 मई 2021 में जारी किया गया
| संस्करण 1.8 मई 2021 में जारी किया गया
|-
|-
| सीवीसी5
| CVC5
| लिनक्स , मैक ओएस , विंडोज़
| लिनक्स , मैक ओएस , विंडोज़
| [[BSD licenses|BSD]]
| [[BSD licenses|BSD]]
Line 189: Line 189:
| {{yes}}
| {{yes}}
|
|
| तर्कसंगत और पूर्णांक रैखिक अंकगणित, सरणियाँ, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, अनुक्रम, बैग, और अबाधित फ़ंक्शन प्रतीकों पर समानता
| तर्कसंगत और पूर्णांक रैखिक अंकगणित, ऐरे, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, अनुक्रम, बैग, और अबाधित फ़ंक्शन प्रतीकों पर समानता
| C++, Python, Java
| C++, Python, Java
| 2021
| 2021
| संस्करण 1.0 अप्रैल 2022 में जारी किया गया
| संस्करण 1.0 अप्रैल 2022 में जारी किया गया
|-
|-
|निर्णय प्रक्रिया टूलकिट (डीपीटी)
|Decision Procedure Toolkit (DPT)
| लिनक्स
| लिनक्स
| [[Apache license|Apache]]
| [[Apache license|Apache]]
Line 205: Line 205:
| डीपीएलएल-बेस्ड
| डीपीएलएल-बेस्ड
|-
|-
| आईसैट (iSAT)
| iSAT
| लिनक्स
| लिनक्स
| Proprietary
| Proprietary
Line 216: Line 216:
| डीपीएलएल-बेस्ड
| डीपीएलएल-बेस्ड
|-
|-
| मैथसैट
| MathSAT
| लिनक्स , मैक ओएस , विंडोज़
| लिनक्स , मैक ओएस , विंडोज़
| Proprietary
| Proprietary
Line 222: Line 222:
|
|
| {{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
Line 247: Line 247:
|
|
|
|
| स्ट्रिंग बाधाओं के लिए एसएमटी सॉल्वर
| स्ट्रिंग बाधाओं के लिए SMT सॉल्वर
|-
|-
|
|
Line 269: Line 269:
|
|
| {{yes}}
| {{yes}}
| खाली सिद्धांत , अंतर, रैखिक अंकगणित, बिटवेक्टर
| रिक्त सिद्धांत , अंतर, रैखिक अंकगणित, बिटवेक्टर
| [[C++]]
| [[C++]]
| 2011
| 2011
| लेजी एसएमटी सॉल्वर
| लेजी SMT सॉल्वर
|-
|-
|raSAT
|raSAT
Line 313: Line 313:
| {{no}}
| {{no}}
| {{no}}
| {{no}}
| रैखिक अंकगणित, अरेखीय अंकगणित, ढेर
| रैखिक अंकगणित, अरेखीय अंकगणित, हीप
| [[C (programming language)|C]]
| [[C (programming language)|C]]
| no
| no
| बाधा प्रबंधन नियमों का उपयोग करके नए सिद्धांतों को लागू कर सकते हैं ।
| बाधा प्रबंधन नियमों का उपयोग करके नए सिद्धांतों को लागू कर सकते हैं ।
|-
|-
| एसएमटी-RAT
| SMT-RAT
| लिनक्स , मैक ओएस
| लिनक्स , मैक ओएस
| [[MIT License|MIT]]
| [[MIT License|MIT]]
Line 327: Line 327:
| [[C++]]
| [[C++]]
| 2015
| 2015
| रणनीतिक और समानांतर एसएमटी समाधान के लिए टूलबॉक्स जिसमें एसएमटी अनुरूप कार्यान्वयन का संग्रह शामिल है।
| रणनीतिक और समानांतर SMT समाधान के लिए टूलबॉक्स जिसमें SMT अनुरूप कार्यान्वयन का संग्रह सम्मिलित है।
|-
|-
| SONOLAR
| SONOLAR
Line 351: Line 351:
|
|
|-
|-
| एसटीपी
| STP
| लिनक्स , ओपनबीएसडी , विंडोज , मैक ओएस
| लिनक्स , ओपनबीएसडी , विंडोज , मैक ओएस
| [[MIT License|MIT]]
| [[MIT License|MIT]]
Line 357: Line 357:
| {{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
Line 379: Line 379:
| {{no}}
| {{no}}
| {{no}}
| {{no}}
| खाली सिद्धांत , रैखिक अंकगणित, बिटवेक्टर, और विवश लैम्ब्डा (सरणी, यादें, कैश, आदि)
| रिक्त सिद्धांत , रैखिक अंकगणित, बिटवेक्टर, और विवश लैम्ब्डा (सरणी, यादें, कैश, आदि)
|
|
| no
| no
| एसएटी-सॉल्वर बेस्ड, मॉस्को एमएल में लिखा गया । इनपुट लैंग्वेज एसएमवी मॉडल चेकर है। अच्छी तरह से प्रलेखित!
| SAT-सॉल्वर बेस्ड, मॉस्को एमएल में लिखा गया । इनपुट लैंग्वेज एसएमवी मॉडल चेकर है। अच्छी तरह से प्रलेखित!
|-
|-
| veriT
| veriT
Line 390: Line 390:
|
|
|
|
| खाली सिद्धांत , तर्कसंगत और पूर्णांक रैखिक अंकगणित, परिमाणक, और अबाधित फ़ंक्शन प्रतीकों पर समानता
| रिक्त सिद्धांत , तर्कसंगत और पूर्णांक रैखिक अंकगणित, परिमाणक, और अबाधित फ़ंक्शन प्रतीकों पर समानता
| [[C (programming language)|C]]/[[C++]]
| [[C (programming language)|C]]/[[C++]]
| 2010
| 2010
| एसएटी-सॉल्वर बेस्ड, सबूत पेश कर सकता है
| SAT-सॉल्वर बेस्ड, प्रमाण प्रस्तुत कर सकते हैं
|-
|-
| {{Visible anchor|Yices}}
| {{Visible anchor|Yices}}
Line 401: Line 401:
| {{no}}
| {{no}}
| {{yes}}
| {{yes}}
| तर्कसंगत और पूर्णांक रैखिक अंकगणित, बिटवेक्टर, सरणियाँ, और अबाधित फ़ंक्शन प्रतीकों पर समानता
| तर्कसंगत और पूर्णांक रैखिक अंकगणित, बिटवेक्टर, ऐरे, और अबाधित फ़ंक्शन प्रतीकों पर समानता
| [[C (programming language)|C]]
| [[C (programming language)|C]]
| 2014
| 2014
| स्रोत कोड ऑनलाइन उपलब्ध है
| सोर्स कोड ऑनलाइन उपलब्ध है
|-
|-
| [[Z3 Theorem Prover]]
| [[Z3 Theorem Prover]]
Line 412: Line 412:
|
|
| {{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
| स्रोत कोड ऑनलाइन उपलब्ध है
| सोर्स कोड ऑनलाइन उपलब्ध है
|}
|}
=== मानकीकरण और एसएमटी-COMP सॉल्वर प्रतियोगिता ===
=== मानकीकरण और SMT-COMP सॉल्वर प्रतियोगिता ===
एसएमटी सॉल्वरों (और स्वचालित प्रमेय प्रोवर्स, एक शब्द जिसे अक्सर समानार्थक रूप से उपयोग किया जाता है) के लिए एक मानकीकृत इंटरफ़ेस का वर्णन करने के कई प्रयास किए गए हैं। सबसे प्रमुख एसएमटी-LIB मानक है, जो S-अभिव्यक्ति पर बेस्ड लैंग्वेज प्रदान करता है। आमतौर पर समर्थित अन्य मानकीकृत प्रारूप कई बूलियन एसएटी सॉल्वरों द्वारा समर्थित डीआईएमएसीएस प्रारूप हैं, और सीवीसी प्रारूप सीवीसी स्वचालित प्रमेय प्रोवर द्वारा उपयोग किया जाता है।
SMT सॉल्वरों (और स्वचालित प्रमेय प्रोवर्स, एक शब्द जिसे प्रायः समानार्थक रूप से उपयोग किया जाता है) के लिए एक मानकीकृत इंटरफ़ेस का वर्णन करने के कई प्रयास किए गए हैं। सबसे प्रमुख SMT-LIB मानक है, जो S-अभिव्यक्ति पर बेस्ड लैंग्वेज प्रदान करता है। सामान्यतः समर्थित अन्य मानकीकृत प्रारूप कई बूलियन SAT सॉल्वरों द्वारा समर्थित डीआईएमएसीएस प्रारूप हैं, और CVC प्रारूप CVC स्वचालित प्रमेय प्रोवर द्वारा उपयोग किया जाता है।


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


==अनुप्रयोग==
==अनुप्रयोग==
एसएमटी सॉल्वर सत्यापन, प्रोग्राम की यथार्थता सिद्ध करने, प्रतीकात्मक निष्पादन के आधार पर सॉफ्टवेयर परीक्षण, और संश्लेषण के लिए, संभावित प्रोग्रमम के स्थान पर सर्च करके प्रोग्रम के भाग उत्पन्न करने के लिए उपयोगी हैं। सॉफ़्टवेयर सत्यापन के अलावा, एसएमटी सॉल्वरों का उपयोग प्रकार के अनुमान के लिए भी किया गया है<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>
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 का उपयोग करती है। समवर्ती सी के लिए वीसीसी सत्यापनकर्ता बूगी का उपयोग करता है, साथ ही अनिवार्य वस्तु-बेस्ड कार्यक्रमों के लिए डैफनी, समवर्ती कार्यक्रमों के लिए चालिस और सी# के लिए स्पेक# का उपयोग करता है। F* एक निर्भरता से टाइप की जाने वाली लैंग्वेज है जो प्रमाण खोजने के लिए Z3 का उपयोग करती है; कंपाइलर इन सबूतों को प्रूफ-ले जाने वाले बाइटकोड का उत्पादन करने के लिए ले जाता है। वाइपर सत्यापन अवसंरचना सत्यापन शर्तों को Z3 में एनकोड करती है। एसबीवी लाइब्रेरी हास्केल कार्यक्रमों का एसएमटी-बेस्ड सत्यापन प्रदान करती है, और उपयोगकर्ता को Z3, एबीसी, बूलेक्टर, सीवीसी5, मैथसैट और येस जैसे कई सॉल्वरों में से चुनने की सुविधा देती है।
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% हो गई है);
* रॉडिन, सिस्टरेल द्वारा विकसित एक बी-मेथड फ्रेमवर्क, ऑल्ट-एर्गो को बैक-एंड के रूप में उपयोग कर सकता है;
* रॉडिन, सिस्टरेल द्वारा विकसित एक बी-मेथड फ्रेमवर्क, ऑल्ट-एर्गो को बैक-एंड के रूप में उपयोग कर सकता है;
* क्यूबिकल, सरणी-बेस्ड संक्रमण प्रणालियों की सुरक्षा गुणों की पुष्टि के लिए एक खुला स्रोत मॉडल चेकर।
* क्यूबिकल, सरणी-बेस्ड संक्रमण प्रणालियों की सुरक्षा गुणों की पुष्टि के लिए एक खुला सोर्स मॉडल चेकर।
* ईज़ीक्रिप्ट, प्रतिकूल कोड के साथ संभाव्य संगणनाओं के संबंधपरक गुणों के बारे में तर्क करने के लिए एक टूलसेट।
* ईज़ीक्रिप्ट, प्रतिकूल कोड के साथ संभाव्य संगणनाओं के संबंधपरक गुणों के बारे में तर्क करने के लिए एक टूलसेट।


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


===सांकेतिक-निष्पादन बेस्ड विश्लेषण एवं परीक्षण===
===सांकेतिक-निष्पादन बेस्ड विश्लेषण एवं परीक्षण===
एसएमटी सॉल्वरों का एक महत्वपूर्ण एप्लीकेशन प्रोग्राम के विश्लेषण और परीक्षण के लिए प्रतीकात्मक निष्पादन है (उदाहरण के लिए, कॉन्कोलिक परीक्षण), जिसका उद्देश्य विशेष रूप से सुरक्षा कमजोरियों का पता लगाना है। इस श्रेणी के उदाहरण टूल में [[माइक्रोसॉफ्ट रिसर्च]] से [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 ट्राइटन]शामिल हैं। एसएमटी सॉल्वर जिनका उपयोग प्रतीकात्मक-निष्पादन अनुप्रयोगों के लिए किया गया है, उनमें [https://github.com/Z3Prover/z3 Z3], [https://sites.google.com/site/stpfastprover/ एसटीपी] आर्काइव्ड 2015-04-06 वेबैक मशीन, सॉल्वर का Z3str समहू और बूलेक्टर शामिल हैं।
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 448: Line 448:
* आंसर सेट प्रोग्रामिंग  
* आंसर सेट प्रोग्रामिंग  
* ऑटोमेटेड थ्योरम प्रोविंग  
* ऑटोमेटेड थ्योरम प्रोविंग  
* एसएटी सॉल्वर  
* SAT सॉल्वर
* फर्स्ट-आर्डर लॉजिक  
* फर्स्ट-आर्डर लॉजिक  
* थ्योरी ऑफ़ पुरे इक्वलिटी  
* थ्योरी ऑफ़ पुरे इक्वलिटी  
Line 474: Line 474:
{{refend}}
{{refend}}
{{Mathematical logic}}
{{Mathematical logic}}
[[Category: बाधा प्रोग्रामिंग]] [[Category: इलेक्ट्रॉनिक डिज़ाइन स्वचालन]] [[Category: औपचारिक तरीके]] [[Category: कंप्यूटर विज्ञान में तर्क]] [[Category: एनपी-पूर्ण समस्याएँ]] [[Category: संतुष्टि की समस्या]] [[Category: श्रीमती सॉल्वर]]


[[Category: Machine Translated Page]]
[[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 सॉल्वर
  • फर्स्ट-आर्डर लॉजिक
  • थ्योरी ऑफ़ पुरे इक्वलिटी

टिप्पणियाँ

  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.


संदर्भ

Retrieved from ‘https://www.vigyanwiki.in/index.php?title=संतुष्टि_मॉड्यूलो_सिद्धांत&oldid=245566’