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

From Vigyanwiki
Line 348: Line 348:
|
|
|-
|-
| STP
| एसटीपी
| [[Linux]], [[OpenBSD]], [[Microsoft Windows|Windows]], [[Mac OS]]
| [[Linux]], [[OpenBSD]], [[Microsoft Windows|Windows]], [[Mac OS]]
| [[MIT License|MIT]]
| [[MIT License|MIT]]
Line 438: Line 438:
कई एसएमटी सॉल्वर SMTLIB2 नामक एक सामान्य इंटरफ़ेस प्रारूप लागू करते हैं (ऐसी फ़ाइलों में आमतौर पर एक्सटेंशन "<code>.smt2</code>" होता है)।  लिक्विडहास्केल उपकरण हास्केल के लिए एक परिशोधन प्रकार-आधारित सत्यापनकर्ता लागू करता है जो किसी भी SMTLIB2 अनुरूप सॉल्वर का उपयोग कर सकता है, जैसे cvc5, MathSat, या Z3।
कई एसएमटी सॉल्वर 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 समहू और बूलेक्टर शामिल हैं।


एसएमटी सॉल्वरों का एक महत्वपूर्ण अनुप्रयोग कार्यक्रमों के विश्लेषण और परीक्षण के लिए प्रतीकात्मक निष्पादन है (उदाहरण के लिए, कॉन्कोलिक परीक्षण), जिसका उद्देश्य विशेष रूप से सुरक्षा कमजोरियों का पता लगाना है।{{citation needed|date=November 2021}} इस श्रेणी के उदाहरण टूल में [[माइक्रोसॉफ्ट रिसर्च]] से [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/ STP] शामिल हैं {{Webarchive|url=https://web.archive.org/web/20150406115407/https://sites.google.com/site/stpfastprover/ |date=2015-04-06 }}, [https://z3string.github.io/ सॉल्वरों का Z3str परिवार], और [http://fmv.jku.at/boolector/ Boolector]।{{citation needed|date=November 2021}}
==यह भी देखें==


==यह भी देखें==
* आंसर सेट प्रोग्रामिंग  
* उत्तर सेट प्रोग्रामिंग
* ऑटोमेटेड थ्योरम प्रोविंग
* स्वचालित प्रमेय सिद्ध करना
* एसएटी सॉल्वर
* बूलियन संतुष्टि समस्या#SAT को हल करने के लिए एल्गोरिदम
* फर्स्ट-आर्डर लॉजिक
* प्रथम-क्रम तर्क
* थ्योरी ऑफ़ पुरे इक्वलिटी
*[[शुद्ध समानता का सिद्धांत]]


==टिप्पणियाँ==
==टिप्पणियाँ==

Revision as of 10:59, 7 August 2023

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

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

मूल शब्दावली

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

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

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

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

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

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

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

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

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

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

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

जहाँ

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

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

सॉल्वर

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

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

Platform Features Notes
Name OS License एसएमटी-LIB CVC DIMACS Built-in theories API एसएमटी-COMP [1]
ABsolver Linux CPL v1.2 No Yes linear arithmetic, non-linear arithmetic C++ no DPLL-based
ऑल्ट-एर्गो 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 एसएमटी 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 एसएमटी 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.
एसएमटी-RAT Linux, Mac OS MIT v2.0 No No linear arithmetic, nonlinear arithmetic C++ 2015 Toolbox for strategic and parallel एसएमटी solving consisting of a collection of एसएमटी 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
एसटीपी 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

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

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

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

अनुप्रयोग

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

सत्यापन

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

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

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

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

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

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

यह भी देखें

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

टिप्पणियाँ

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


संदर्भ