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

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


==बुनियादी शब्दावली==
==मूल शब्दावली==
औपचारिक रूप से कहें तो, एक एसएमटी उदाहरण प्रथम-क्रम तर्क में एक अच्छी तरह से गठित सूत्र है, जहां कुछ फ़ंक्शन और विधेय प्रतीकों की अतिरिक्त व्याख्याएं होती हैं, और एसएमटी यह निर्धारित करने की समस्या है कि क्या ऐसा सूत्र संतोषजनक है। दूसरे शब्दों में, बूलियन संतुष्टि समस्या (एसएटी) के एक उदाहरण की कल्पना करें जिसमें कुछ [[बाइनरी डेटा]] को गैर-बाइनरी चर के उपयुक्त सेट पर [[विधेय (गणितीय तर्क)]] द्वारा प्रतिस्थापित किया जाता है। एक विधेय गैर-बाइनरी चर का एक द्विआधारी-मूल्यवान फ़ंक्शन है। उदाहरण विधेय में रैखिक [[असमानता (गणित)]] शामिल है (उदाहरण के लिए, <math>3x + 2y - z \geq 4</math>) या [[अव्याख्यायित शब्द]]ों और फ़ंक्शन प्रतीकों वाली समानताएं (उदाहरण के लिए, <math>f(f(u, v), v) = f(u, v)</math> कहाँ <math>f</math> दो तर्कों का कुछ अनिर्दिष्ट कार्य है)। इन विधेयों को निर्दिष्ट प्रत्येक संबंधित सिद्धांत के अनुसार वर्गीकृत किया गया है। उदाहरण के लिए, वास्तविक चर पर रैखिक असमानताओं का मूल्यांकन रैखिक वास्तविक [[अंकगणित]] के सिद्धांत के नियमों का उपयोग करके किया जाता है, जबकि गैर-व्याख्यायित शब्दों और फ़ंक्शन प्रतीकों से जुड़े विधेय का मूल्यांकन समानता के साथ गैर-व्याख्यायित कार्यों के सिद्धांत के नियमों का उपयोग करके किया जाता है (कभी-कभी खाली सिद्धांत के रूप में जाना जाता है)अन्य सिद्धांतों में सरणी डेटा संरचना और सूची (कंप्यूटिंग) संरचनाओं के सिद्धांत ([[कंप्यूटर प्रोग्राम]]ों के मॉडलिंग और सत्यापन के लिए उपयोगी), और [[बिट वैक्टर]] के सिद्धांत ([[हार्डवेयर डिज़ाइन]] के मॉडलिंग और सत्यापन में उपयोगी) शामिल हैं। उप-सिद्धांत भी संभव हैं: उदाहरण के लिए, अंतर तर्क रैखिक अंकगणित का एक उप-सिद्धांत है जिसमें प्रत्येक असमानता को रूप तक सीमित किया जाता है <math>x - y > c</math> चर के लिए <math>x</math> और <math>y</math> और स्थिर <math>c</math>.
औपचारिक रूप से कहें तो, एक एसएमटी उदाहरण प्रथम-क्रम तर्क में एक सूत्र है, जहां कुछ फ़ंक्शन और विधेय प्रतीकों की अतिरिक्त व्याख्याएं होती हैं, और एसएमटी यह निर्धारित करने की समस्या है कि क्या ऐसा सूत्र संतोषजनक है। दूसरे शब्दों में, बूलियन संतुष्टि समस्या (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> रूप तक सीमित रखा जाता है।


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


==अभिव्यंजक शक्ति==
==अभिव्यंजक शक्ति==

Revision as of 10:10, 7 August 2023

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

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

मूल शब्दावली

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

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

अभिव्यंजक शक्ति

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

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

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


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

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

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

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

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

कहाँ

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

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


समाधानकर्ता

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

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

Platform Features Notes
Name OS License SMT-LIB CVC DIMACS Built-in theories API SMT-COMP [1]
ABsolver Linux CPL v1.2 No Yes linear arithmetic, non-linear arithmetic C++ no DPLL-based
Alt-Ergo Linux, Mac OS, Windows CeCILL-C (roughly equivalent to LGPL) partial v1.2 and v2.0 No No empty theory, linear integer and rational arithmetic, non-linear arithmetic, polymorphic arrays, enumerated datatypes, AC symbols, bitvectors, record datatypes, quantifiers OCaml 2008 Polymorphic first-order input language à la ML, SAT-solver based, combines Shostak-like and Nelson-Oppen like approaches for reasoning modulo theories
Barcelogic Linux Proprietary v1.2 empty theory, difference logic C++ 2009 DPLL-based, congruence closure
Beaver Linux, Windows BSD v1.2 No No bitvectors OCaml 2009 SAT-solver based
Boolector Linux MIT v1.2 No No bitvectors, arrays C 2009 SAT-solver based
CVC3 Linux BSD v1.2 Yes empty theory, linear arithmetic, arrays, tuples, types, records, bitvectors, quantifiers C/C++ 2010 proof output to HOL
CVC4 Linux, Mac OS, Windows, FreeBSD BSD Yes Yes rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bitvectors, strings, and equality over uninterpreted function symbols C++ 2021 version 1.8 released May 2021
cvc5 Linux, Mac OS, Windows BSD Yes Yes rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bitvectors, strings, sequences, bags, and equality over uninterpreted function symbols C++, Python, Java 2021 version 1.0 released April 2022
Decision Procedure Toolkit (DPT) Linux Apache No OCaml no DPLL-based
iSAT Linux Proprietary No non-linear arithmetic no DPLL-based
MathSAT Linux, Mac OS, Windows Proprietary Yes Yes empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays C/C++, Python, Java 2010 DPLL-based
MiniSmt Linux LGPL partial v2.0 non-linear arithmetic OCaml 2010 SAT-solver based, Yices-based
Norn SMT solver for string constraints
OpenCog Linux AGPL No No No probabilistic logic, arithmetic. relational models C++, Scheme, Python no subgraph isomorphism
OpenSMT Linux, Mac OS, Windows GPLv3 partial v2.0 Yes empty theory, differences, linear arithmetic, bitvectors C++ 2011 lazy SMT Solver
raSAT Linux GPLv3 v2.0 real and integer nonlinear arithmetic 2014, 2015 extension of the Interval Constraint Propagation with Testing and the Intermediate Value Theorem
SatEEn ? Proprietary v1.2 linear arithmetic, difference logic none 2009
SMTInterpol Linux, Mac OS, Windows LGPLv3 v2.5 uninterpreted functions, linear real arithmetic, and linear integer arithmetic Java 2012 Focuses on generating high quality, compact interpolants.
SMCHR Linux, Mac OS, Windows GPLv3 No No No linear arithmetic, nonlinear arithmetic, heaps C no Can implement new theories using Constraint Handling Rules.
SMT-RAT Linux, Mac OS MIT v2.0 No No linear arithmetic, nonlinear arithmetic C++ 2015 Toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations.
SONOLAR Linux, Windows Proprietary partial v2.0 bitvectors C 2010 SAT-solver based
Spear Linux, Mac OS, Windows Proprietary v1.2 bitvectors 2008
STP Linux, OpenBSD, Windows, Mac OS MIT partial v2.0 Yes No bitvectors, arrays C, C++, Python, OCaml, Java 2011 SAT-solver based
SWORD Linux Proprietary v1.2 bitvectors 2009
UCLID Linux BSD No No No empty theory, linear arithmetic, bitvectors, and constrained lambda (arrays, memories, cache, etc.) no SAT-solver based, written in Moscow ML. Input language is SMV model checker. Well-documented!
veriT Linux, OS X BSD partial v2.0 empty theory, rational and integer linear arithmetics, quantifiers, and equality over uninterpreted function symbols C/C++ 2010 SAT-solver based, can produce proofs
Yices Linux, Mac OS, Windows, FreeBSD GPLv3 v2.0 No Yes rational and integer linear arithmetic, bitvectors, arrays, and equality over uninterpreted function symbols C 2014 Source code is available online
Z3 Theorem Prover Linux, Mac OS, Windows, FreeBSD MIT v2.0 Yes empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays, datatypes, quantifiers, strings C/C++, .NET, OCaml, Python, Java, Haskell 2011 Source code is available online


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

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

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


अनुप्रयोग

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


सत्यापन

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

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

Alt-Ergo SMT सॉल्वर के शीर्ष पर कई सत्यापनकर्ता भी बनाए गए हैं। यहां परिपक्व अनुप्रयोगों की एक सूची दी गई है:

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

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

प्रतीकात्मक-निष्पादन आधारित विश्लेषण और परीक्षण

एसएमटी सॉल्वरों का एक महत्वपूर्ण अनुप्रयोग कार्यक्रमों के विश्लेषण और परीक्षण के लिए प्रतीकात्मक निष्पादन है (उदाहरण के लिए, कॉन्कोलिक परीक्षण), जिसका उद्देश्य विशेष रूप से सुरक्षा कमजोरियों का पता लगाना है।[citation needed] इस श्रेणी के उदाहरण टूल में माइक्रोसॉफ्ट रिसर्च से SAGE, KLEE, S2E, और ट्राइटन शामिल हैं। एसएमटी सॉल्वर जिनका उपयोग प्रतीकात्मक-निष्पादन अनुप्रयोगों के लिए किया गया है उनमें Z3, STP शामिल हैं Archived 2015-04-06 at the Wayback Machine, सॉल्वरों का Z3str परिवार, और Boolector[citation needed]

यह भी देखें

  • उत्तर सेट प्रोग्रामिंग
  • स्वचालित प्रमेय सिद्ध करना
  • बूलियन संतुष्टि समस्या#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.


संदर्भ