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

Latest revision as of 13:58, 14 August 2023

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

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

मूल शब्दावली

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

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

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

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

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

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

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

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

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

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

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

{\begin{array}{lr}&(\sin(x)^{3}=\cos(\log(y)\cdot x)\vee b\vee -x^{2}\geq 2.3y)\wedge \left(\neg b\vee y<-34.4\vee \exp(x)>{y \over x}\right)\end{array}}

जहाँ

b\in {\mathbb {B} },x,y\in {\mathbb {R} }.

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

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

सॉल्वर

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

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

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

प्लेटफ़ॉर्म			विशेषताएँ						टिप्पणियाँ
नाम	ओएस	लाइसेंस	SMT-LIB	CVC	डायमैक	अंतर्निर्मित सिद्धांत	एपीआई	SMT-कॉम्प[1]
ABsolver	लिनक्स	CPL	v1.2	No	Yes	रैखिक अंकगणित, अरेखीय अंकगणित	C++	no	डीपीएलएल-बेस्ड
Alt-Ergo	लिनक्स , मैक ओएस , विंडोज़	CeCILL-C (roughly equivalent to LGPL)	partial v1.2 and v2.0	No	No	रिक्त सिद्धांत , रैखिक पूर्णांक और तर्कसंगत अंकगणित, गैर-रेखीय अंकगणित, बहुरूपी ऐरे , प्रगणित डेटा प्रकार , एसी प्रतीक , बिटवेक्टर , रिकॉर्ड डेटा प्रकार , क्वांटिफायर	OCaml	2008	बहुरूपी प्रथम-क्रम इनपुट लैंग्वेज à la ML, SAT-सॉल्वर बेस्ड, तर्क मॉड्यूल सिद्धांतों के लिए शोस्ताक-जैसे और नेल्सन-ओपेन जैसे दृष्टिकोणों को जोड़ती है
Barcelogic	लिनक्स	Proprietary	v1.2			खोखला सिद्धांत , अंतर तर्क	C++	2009	डीपीएलएल-बेस्ड, सर्वांगसमता समापन
Beaver	लिनक्स , विंडोज़	BSD	v1.2	No	No	बिटवेक्टर	OCaml	2009	SAT-सॉल्वर बेस्ड
Boolector	लिनक्स	MIT	v1.2	No	No	बिटवेक्टर , ऐरे	C	2009	SAT-सॉल्वर बेस्ड
CVC3	लिनक्स	BSD	v1.2	Yes		रिक्त सिद्धांत , रैखिक अंकगणित, ऐरे, टुपल्स, प्रकार, रिकॉर्ड, बिटवेक्टर, क्वांटिफायर	C/C++	2010	HOL को प्रूफ़ आउटपुट
CVC4	लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी	BSD	Yes	Yes		तर्कसंगत और पूर्णांक रैखिक अंकगणित, ऐरे, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, और अबाधित फ़ंक्शन प्रतीकों पर समानता	C++	2021	संस्करण 1.8 मई 2021 में जारी किया गया
CVC5	लिनक्स , मैक ओएस , विंडोज़	BSD	Yes	Yes		तर्कसंगत और पूर्णांक रैखिक अंकगणित, ऐरे, टुपल्स, रिकॉर्ड, आगमनात्मक डेटा प्रकार, बिटवेक्टर, स्ट्रिंग्स, अनुक्रम, बैग, और अबाधित फ़ंक्शन प्रतीकों पर समानता	C++, Python, Java	2021	संस्करण 1.0 अप्रैल 2022 में जारी किया गया
Decision Procedure Toolkit (DPT)	लिनक्स	Apache	No				OCaml	no	डीपीएलएल-बेस्ड
iSAT	लिनक्स	Proprietary	No			अरेखीय अंकगणित		no	डीपीएलएल-बेस्ड
MathSAT	लिनक्स , मैक ओएस , विंडोज़	Proprietary	Yes		Yes	रिक्त सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, ऐरे	C/C++, Python, Java	2010	डीपीएलएल-बेस्ड
MiniSmt	लिनक्स	LGPL	partial v2.0			अरेखीय अंकगणित	OCaml	2010	SAT-सॉल्वर बेस्ड, Yices-बेस्ड
Norn									स्ट्रिंग बाधाओं के लिए SMT सॉल्वर
	लिनक्स
OpenCog	लिनक्स	AGPL	No	No	No	संभाव्य तर्क , अंकगणित। संबंधपरक मॉडल	C++, Scheme, Python	no	सबग्राफ समरूपता
OpenSMT	लिनक्स , मैक ओएस , विंडोज़	GPLv3	partial v2.0		Yes	रिक्त सिद्धांत , अंतर, रैखिक अंकगणित, बिटवेक्टर	C++	2011	लेजी SMT सॉल्वर
raSAT	लिनक्स	GPLv3	v2.0			वास्तविक और पूर्णांक अरेखीय अंकगणित		2014, 2015	परीक्षण और मध्यवर्ती मूल्य प्रमेय के साथ अंतराल बाधा प्रसार का विस्तार
SatEEn	?	Proprietary	v1.2			रैखिक अंकगणित, अंतर तर्क	none	2009
SMTInterpol	लिनक्स , मैक ओएस , विंडोज़	LGPLv3	v2.5			अव्याख्यायित फलन, रैखिक वास्तविक अंकगणित, और रैखिक पूर्णांक अंकगणित	Java	2012	उच्च गुणवत्ता, कॉम्पैक्ट इंटरपोलेंट उत्पन्न करने पर ध्यान केंद्रित करता है।
SMCHR	लिनक्स , मैक ओएस , विंडोज़	GPLv3	No	No	No	रैखिक अंकगणित, अरेखीय अंकगणित, हीप	C	no	बाधा प्रबंधन नियमों का उपयोग करके नए सिद्धांतों को लागू कर सकते हैं ।
SMT-RAT	लिनक्स , मैक ओएस	MIT	v2.0	No	No	रैखिक अंकगणित, अरेखीय अंकगणित	C++	2015	रणनीतिक और समानांतर SMT समाधान के लिए टूलबॉक्स जिसमें SMT अनुरूप कार्यान्वयन का संग्रह सम्मिलित है।
SONOLAR	लिनक्स , विंडोज़	Proprietary	partial v2.0			बिटवेक्टर	C	2010	SAT-सॉल्वर बेस्ड
Spear	लिनक्स , मैक ओएस , विंडोज़	Proprietary	v1.2			बिटवेक्टर		2008
STP	लिनक्स , ओपनबीएसडी , विंडोज , मैक ओएस	MIT	partial v2.0	Yes	No	बिटवेक्टर, ऐरे	C, C++, Python, OCaml, Java	2011	SAT-सॉल्वर बेस्ड
SWORD	लिनक्स	Proprietary	v1.2			बिटवेक्टर		2009
UCLID	लिनक्स	BSD	No	No	No	रिक्त सिद्धांत , रैखिक अंकगणित, बिटवेक्टर, और विवश लैम्ब्डा (सरणी, यादें, कैश, आदि)		no	SAT-सॉल्वर बेस्ड, मॉस्को एमएल में लिखा गया । इनपुट लैंग्वेज एसएमवी मॉडल चेकर है। अच्छी तरह से प्रलेखित!
veriT	लिनक्स , ओएस एक्स	BSD	partial v2.0			रिक्त सिद्धांत , तर्कसंगत और पूर्णांक रैखिक अंकगणित, परिमाणक, और अबाधित फ़ंक्शन प्रतीकों पर समानता	C/C++	2010	SAT-सॉल्वर बेस्ड, प्रमाण प्रस्तुत कर सकते हैं
Yices	लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी	GPLv3	v2.0	No	Yes	तर्कसंगत और पूर्णांक रैखिक अंकगणित, बिटवेक्टर, ऐरे, और अबाधित फ़ंक्शन प्रतीकों पर समानता	C	2014	सोर्स कोड ऑनलाइन उपलब्ध है
Z3 Theorem Prover	लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी	MIT	v2.0		Yes	रिक्त सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, ऐरे, डेटाटाइप, क्वांटिफायर , स्ट्रिंग्स	C/C++, .NET, OCaml, Python, Java, Haskell	2011	सोर्स कोड ऑनलाइन उपलब्ध है

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

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

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

अनुप्रयोग

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

सत्यापन

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

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

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

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

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

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

यह भी देखें

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

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

संदर्भ

Barrett, C.; Sebastiani, R.; Seshia, S.; Tinelli, C. (2009). "Satisfiability Modulo Theories". In Biere, A.; Heule, M.J.H.; van Maaren, H.; Walsh, T. (eds.). Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications. Vol. 185. IOS Press. pp. 825–885. ISBN 9781607503767.
Ganesh, Vijay (September 2007). Decision Procedures for Bit-Vectors, Arrays and Integers (PDF) (PhD). Computer Science Department, Stanford University.
Jha, Susmit; Limaye, Rhishikesh; Seshia, Sanjit A. (2009). "Beaver: Engineering an efficient SMT solver for bit-vector arithmetic". Proceedings of 21st International Conference on Computer-Aided Verification. pp. 668–674. doi:10.1007/978-3-642-02658-4_53. ISBN 978-3-642-02658-4.
Bryant, R.E.; German, S.M.; Velev, M.N. (1999). "Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions" (PDF). Analytic Tableaux and Related Methods. pp. 1–13., pp. , .
Davis, M.; Putnam, H. (1960). "A Computing Procedure for Quantification Theory". Journal of the Association for Computing Machinery. 7 (3): 201–215. doi:10.1145/321033.321034. S2CID 31888376.
Davis, M.; Logemann, G.; Loveland, D. (1962). "A Machine Program for Theorem-Proving". Communications of the ACM. 5 (7): 394–397. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. S2CID 15866917.
Kroening, D.; Strichman, O. (2008). Decision Procedures — an algorithmic point of view. Theoretical Computer Science series. Springer. ISBN 978-3-540-74104-6.
Nam, G.-J.; Sakallah, K.A.; Rutenbar, R. (2002). "A New FPGA Detailed Routing Approach via Search-Based Boolean Satisfiability". IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 21 (6): 674–684. doi:10.1109/TCAD.2002.1004311.
SMT-LIB: The Satisfiability Modulo Theories Library
SMT-COMP: The Satisfiability Modulo Theories Competition
Decision procedures - an algorithmic point of view
Sebastiani, R. (2007). "Lazy Satisfiability Modulo Theories". Journal on Satisfiability, Boolean Modeling and Computation. 3 (3–4): 141–224. CiteSeerX 10.1.1.100.221. doi:10.3233/SAT190034.
Yurichev, D. "Quick introduction into SAT/SMT solvers and symbolic execution" (PDF).
This article is adapted from a column in the ACM SIGDA e-newsletter by Prof. Karem Sakallah. Original text is available here

[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.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

Anonymous

Search

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

Namespaces

More

Page actions

Latest revision as of 13:58, 14 August 2023

Contents

मूल शब्दावली

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

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

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

सॉल्वर

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

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

अनुप्रयोग

सत्यापन

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

यह भी देखें

टिप्पणियाँ

संदर्भ

Navigation

Navigation

Wiki tools

Wiki tools

@@ Line 1: / Line 1: @@
 {{Short description|Logical problem studied in computer science}}
-[[कंप्यूटर विज्ञान]] और [[गणितीय तर्क]] में, '''[[संतुष्टि]] मॉड्यूल सिद्धांत (एसएमटी)''' यह निर्धारित करने की समस्या है कि कोई गणितीय सूत्र संतोषजनक है या नहीं। यह [[बूलियन संतुष्टि समस्या]] (SAT) को वास्तविक संख्याओं, [[पूर्णांकों]] और/या सूचियों, ऐरे, बिट वैक्टर और स्ट्रिंग्स जैसी विभिन्न डेटा संरचनाओं को शामिल करने वाले अधिक जटिल सूत्रों में सामान्यीकृत करता है। यह नाम इस तथ्य से लिया गया है कि इन अभिव्यक्तियों की व्याख्या समानता के साथ प्रथम-क्रम तर्क में एक निश्चित औपचारिक सिद्धांत ("मॉड्यूलो") के भीतर की जाती है (अक्सर क्वांटिफायर की अनुमति नहीं दी जाती है)। एसएमटी सॉल्वर ऐसे उपकरण हैं जिनका लक्ष्य इनपुट के व्यावहारिक सबसेट के लिए एसएमटी समस्या को हल करना है। Z3 और cvc5 जैसे '''SMT सॉल्वर''' का उपयोग कंप्यूटर विज्ञान में अनुप्रयोगों की एक विस्तृत श्रृंखला के लिए बिल्डिंग ब्लॉक के रूप में किया गया है, जिसमें स्वचालित प्रमेय सिद्ध करना, प्रोग्राम विश्लेषण, प्रोग्राम सत्यापन और सॉफ़्टवेयर परीक्षण शामिल हैं।
+[[कंप्यूटर विज्ञान]] और [[गणितीय तर्क]] में, '''[[संतुष्टि]] मॉड्यूल सिद्धांत (SMT)''' यह निर्धारित करने की समस्या है कि कोई गणितीय सूत्र संतोषजनक है या नहीं। यह [[बूलियन संतुष्टि समस्या]] (SAT) को वास्तविक संख्याओं, [[पूर्णांकों]] और/या सूचियों, ऐरे, बिट वैक्टर और स्ट्रिंग्स जैसी विभिन्न डेटा संरचनाओं को सम्मिलित करने वाले अधिक जटिल सूत्रों में सामान्यीकृत करता है। यह नाम इस तथ्य से लिया गया है कि इन अभिव्यक्तियों की व्याख्या समानता के साथ प्रथम-क्रम तर्क में एक निश्चित औपचारिक सिद्धांत ("मॉड्यूलो") के भीतर की जाती है (प्रायः क्वांटिफायर की अनुमति नहीं दी जाती है)। SMT सॉल्वर ऐसे उपकरण हैं जिनका लक्ष्य इनपुट के व्यावहारिक सबसेट के लिए SMT समस्या को हल करना है। Z3 और cvc5 जैसे '''SMT सॉल्वर''' का उपयोग कंप्यूटर विज्ञान में अनुप्रयोगों की एक विस्तृत श्रृंखला के लिए बिल्डिंग ब्लॉक के रूप में किया गया है, जिसमें स्वचालित प्रमेय सिद्ध करना, प्रोग्राम विश्लेषण, प्रोग्राम सत्यापन और सॉफ़्टवेयर परीक्षण सम्मिलित हैं।
-चूँकि बूलियन संतुष्टि पहले से ही एनपी-पूर्ण है, एसएमटी समस्या आमतौर पर एनपी-हार्ड है, और कई सिद्धांतों के लिए यह अनिर्णीत है। शोधकर्ता अध्ययन करते हैं कि कौन से सिद्धांत या सिद्धांतों के उपसमुच्चय एक निर्णायक एसएमटी समस्या और निर्णायक मामलों की कम्प्यूटेशनल जटिलता को जन्म देते हैं। परिणामी निर्णय प्रक्रियाएँ अक्सर सीधे एसएमटी सॉल्वर में लागू की जाती हैं; उदाहरण के लिए, प्रेस्बर्गर अंकगणित की निर्णायकता देखें। एसएमटी को एक बाधा संतुष्टि समस्या के रूप में सोचा जा सकता है और इस प्रकार कन्सट्रैन्ट प्रोग्रामिंग के लिए एक निश्चित औपचारिक दृष्टिकोण माना जा सकता है।
+चूँकि बूलियन संतुष्टि पहले से ही एनपी-पूर्ण है, SMT समस्या सामान्यतः एनपी-हार्ड है, और कई सिद्धांतों के लिए यह अनिर्णीत है। शोधकर्ता अध्ययन करते हैं कि कौन से सिद्धांत या सिद्धांतों के उपसमुच्चय एक निर्णायक SMT समस्या और निर्णायक स्थितियों की कम्प्यूटेशनल सम्मिश्रता को उत्त्पन्न करते हैं। परिणामी निर्णय प्रक्रियाएँ प्रायः सीधे SMT सॉल्वर में लागू की जाती हैं; उदाहरण के लिए, प्रेस्बर्गर अंकगणित की निर्णायकता देखें। SMT को एक बाधा संतुष्टि समस्या के रूप में सोचा जा सकता है और इस प्रकार कन्सट्रैन्ट प्रोग्रामिंग के लिए एक निश्चित औपचारिक दृष्टिकोण माना जा सकता है।
-==बुनियादी शब्दावली==
+==मूल शब्दावली==
-औपचारिक रूप से कहें तो, एक एसएमटी उदाहरण प्रथम-क्रम तर्क में एक अच्छी तरह से गठित सूत्र है, जहां कुछ फ़ंक्शन और विधेय प्रतीकों की अतिरिक्त व्याख्याएं होती हैं, और एसएमटी यह निर्धारित करने की समस्या है कि क्या ऐसा सूत्र संतोषजनक है। दूसरे शब्दों में, बूलियन संतुष्टि समस्या (एसएटी) के एक उदाहरण की कल्पना करें जिसमें कुछ [[बाइनरी डेटा]] को गैर-बाइनरी चर के उपयुक्त सेट पर [[विधेय (गणितीय तर्क)]] द्वारा प्रतिस्थापित किया जाता है। एक विधेय गैर-बाइनरी चर का एक द्विआधारी-मूल्यवान फ़ंक्शन है। उदाहरण विधेय में रैखिक [[असमानता (गणित)]] शामिल है (उदाहरण के लिए, <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>.
+औपचारिक रूप से कहें तो, एक 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'' जैसी "स्पष्ट" समरूपता निकालना मुश्किल है।
-[[बाधा तर्क प्रोग्रामिंग]] रैखिक अंकगणितीय बाधाओं के लिए समर्थन प्रदान करती है, लेकिन एक पूरी तरह से अलग सैद्धांतिक ढांचे के भीतर।{{citation needed|date=July 2020}} [[उच्च-क्रम तर्क]] में सूत्रों को हल करने के लिए एसएमटी सॉल्वर का भी विस्तार किया गया है।<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
@@ Line 35: / Line 34: @@
      | year = 2006 |doi=10.1145/1217856.1217859
 | issue=6| s2cid = 14058631
-  }}</ref> यह आर्किटेक्चर डीपीएलएल-आधारित एसएटी सॉल्वर को बूलियन तर्क की जिम्मेदारी देता है, जो बदले में, एक अच्छी तरह से परिभाषित इंटरफ़ेस के माध्यम से सिद्धांत टी के लिए सॉल्वर के साथ इंटरैक्ट करता है। सिद्धांत सॉल्वर को केवल SAT सॉल्वर से प्राप्त सिद्धांत विधेय के संयोजन की व्यवहार्यता की जांच करने के बारे में चिंता करने की आवश्यकता है क्योंकि यह सूत्र के बूलियन खोज स्थान की खोज करता है। हालाँकि, इस एकीकरण के अच्छी तरह से काम करने के लिए, सिद्धांत समाधानकर्ता को प्रसार और संघर्ष विश्लेषण में भाग लेने में सक्षम होना चाहिए, अर्थात, उसे पहले से स्थापित तथ्यों से नए तथ्यों का अनुमान लगाने में सक्षम होना चाहिए, साथ ही सिद्धांत संघर्ष उत्पन्न होने पर अव्यवहार्यता की संक्षिप्त व्याख्या प्रदान करने में सक्षम होना चाहिए। दूसरे शब्दों में, सिद्धांत समाधानकर्ता को वृद्धिशील और [[ बैक ट्रैकिंग ]] होना चाहिए।
+  }}</ref> यह आर्किटेक्चर डीपीएलएल-बेस्ड SAT सॉल्वर को बूलियन तर्क की जिम्मेदारी देता है, जो बदले में, एक अच्छी तरह से परिभाषित इंटरफ़ेस के माध्यम से सिद्धांत टी के लिए एक सॉल्वर के साथ बातचीत करता है। सिद्धांत सॉल्वर को केवल SAT सॉल्वर से पारित सिद्धांत विधेय के संयोजन की व्यवहार्यता की जांच करने के बारे में चिंता करने की ज़रूरत है क्योंकि यह सूत्र के बूलियन सर्च स्थान की खोज करता है। हालाँकि, इस एकीकरण के अच्छी तरह से काम करने के लिए, सिद्धांत समाधानकर्ता को प्रसार और संघर्ष विश्लेषण में भाग लेने में सक्षम होना चाहिए, अर्थात, उसे पहले से स्थापित तथ्यों से नए तथ्यों का अनुमान लगाने में सक्षम होना चाहिए, साथ ही सैद्धांतिक विरोधिता उत्पन्न होने पर अव्यवहार्यता की संक्षिप्त व्याख्या प्रदान करना। दूसरे शब्दों में, थ्योरी सॉल्वर वृद्धिशील और बैकट्रैकेबल होना चाहिए।
-==अनिर्णायक सिद्धांतों के लिए एसएमटी==
+==अनिर्णीत सिद्धांतों के लिए SMT==
-अधिकांश सामान्य एसएमटी दृष्टिकोण निर्णायकता (तर्क) सिद्धांतों का समर्थन करते हैं। हालाँकि, कई वास्तविक दुनिया प्रणालियाँ, जैसे कि एक विमान और उसका व्यवहार, केवल [[पारलौकिक कार्य]]ों से जुड़े वास्तविक संख्याओं पर गैर-रेखीय अंकगणित के माध्यम से मॉडलिंग की जा सकती हैं। यह तथ्य एसएमटी समस्या को गैर-रेखीय सिद्धांतों तक विस्तारित करने के लिए प्रेरित करता है, जैसे कि यह निर्धारित करना कि क्या निम्नलिखित समीकरण संतोषजनक है:
+अधिकांश सामान्य SMT दृष्टिकोण निर्णायक सिद्धांतों का समर्थन करते हैं। हालाँकि, कई वास्तविक दुनिया प्रणालियाँ, जैसे कि एक विमान और उसका व्यवहार, केवल पारमार्थिक फंक्शन से जुड़े वास्तविक संख्याओं पर गैर-रैखिक अंकगणित के माध्यम से मॉडलिंग की जा सकती हैं। यह तथ्य SMT समस्या के गैर-रेखीय सिद्धांतों तक विस्तार को प्रेरित करता है, जैसे यह निर्धारित करना कि क्या निम्नलिखित समीकरण संतोषजनक है:
 : <math>
@@ Line 45: / Line 44: @@
 \end{array}
 </math>
-कहाँ
+जहाँ
 : <math>b \in {\mathbb B}, x,y \in {\mathbb R}.</math>
-हालाँकि, ऐसी समस्याएँ सामान्य रूप से अनिर्णीत समस्या हैं। (दूसरी ओर, [[वास्तविक बंद क्षेत्र]]ों का सिद्धांत, और इस प्रकार [[वास्तविक संख्या]]ओं का पूर्ण प्रथम क्रम सिद्धांत, क्वांटिफायर उन्मूलन का उपयोग करके निर्णायकता (तर्क) है। यह [[अल्फ्रेड टार्स्की]] के कारण है।) जोड़ (लेकिन गुणा नहीं) के साथ [[प्राकृतिक संख्या]]ओं का पहला क्रम सिद्धांत, जिसे प्रेस्बर्गर अंकगणित कहा जाता है, भी निर्णायक है। चूँकि स्थिरांकों द्वारा गुणन को नेस्टेड परिवर्धन के रूप में कार्यान्वित किया जा सकता है, कई कंप्यूटर प्रोग्रामों में अंकगणित को प्रेस्बर्गर अंकगणित का उपयोग करके व्यक्त किया जा सकता है, जिसके परिणामस्वरूप निर्णय लेने योग्य सूत्र प्राप्त होते हैं।
+हालाँकि, ऐसी समस्याएँ सामान्यतः अनिर्णीत होती हैं। (दूसरी ओर, वास्तविक बंद क्षेत्रों का सिद्धांत, और इस प्रकार वास्तविक संख्याओं का पूर्ण प्रथम क्रम सिद्धांत, क्वांटिफायर उन्मूलन का उपयोग करके तय किया जा सकता है। यह [[अल्फ्रेड टार्स्की]] के कारण है।) जोड़ के साथ प्राकृतिक संख्याओं का पहला क्रम सिद्धांत ( लेकिन गुणा नहीं), जिसे प्रेस्बर्गर अंकगणित कहा जाता है, भी निर्णय योग्य है। चूँकि स्थिरांकों द्वारा गुणन को नेस्टेड परिवर्धन के रूप में कार्यान्वित किया जा सकता है, कई कंप्यूटर प्रोग्रामों में अंकगणित को प्रेसबर्गर अंकगणित का उपयोग करके व्यक्त किया जा सकता है, जिसके परिणामस्वरूप निर्णायक सूत्र प्राप्त होते हैं।
-वास्तविक पर अनिर्णीत अंकगणितीय सिद्धांतों से सिद्धांत परमाणुओं के बूलियन संयोजनों को संबोधित करने वाले एसएमटी सॉल्वर के उदाहरण एबीएसॉल्वर हैं,<ref>{{Citation
+वास्तविकताओं पर अनिर्णीत अंकगणितीय सिद्धांतों से सिद्धांत परमाणुओं के बूलियन संयोजनों को संबोधित करने वाले SMT सॉल्वर के उदाहरण एबीएसॉल्वर हैं,<ref>{{Citation
    | first1 = A.
    | last1 = Bauer
@@ Line 67: / Line 66: @@
    | citeseerx = 10.1.1.323.6807
    | s2cid = 9159847
-  }}</ref> जो एक गैर-रैखिक अनुकूलन पैकेट के साथ एक शास्त्रीय डीपीएलएल (टी) आर्किटेक्चर को (आवश्यक रूप से अपूर्ण) अधीनस्थ सिद्धांत सॉल्वर के रूप में नियोजित करता है, और [http://isat.gforge.avacs.org/ iSAT], डीपीएलएल एसएटी-सॉल्विंग और इंटरवल अंकगणित#इंटरवल अंकगणित के एकीकरण पर आधारित है जिसे आईएसएटी एल्गोरिदम कहा जाता है।<ref>{{Citation
+  }}</ref> जो एक गैर-रेखीय अनुकूलन पैकेट के साथ एक शास्त्रीय डीपीएलएल (टी) आर्किटेक्चर को (आवश्यक रूप से अपूर्ण) अधीनस्थ सिद्धांत सॉल्वर और आईएसएटी के रूप में नियोजित करता है। , डीपीएलएल SAT-समाधान और अंतराल बाधा प्रसार के एकीकरण पर निर्माण, जिसे आईएसएटी एल्गोरिदम कहा जाता है।<ref>{{Citation
      | first1 = M.
      | last1 = Fränzle
@@ Line 85: / Line 84: @@
      | year = 2007 }}</ref>
+==सॉल्वर{{anchor|SMT solvers}}==
-==समाधानकर्ता{{anchor|SMT solvers}}==
+नीचे दी गई तालिका कई उपलब्ध SMT सॉल्वरों की कुछ विशेषताओं का सारांश प्रस्तुत करती है। कॉलम "SMT-LIB" SMT-LIB लैंग्वेज के साथ अनुकूलता दर्शाता है; 'हाँ' चिह्नित कई प्रणालियाँ केवल SMT-LIB के पुराने संस्करणों का समर्थन कर सकती हैं, या लैंग्वेज के लिए केवल आंशिक समर्थन प्रदान कर सकती हैं। कॉलम "CVC" CVC लैंग्वेज के लिए समर्थन दर्शाता है। कॉलम "DIMACS" DIMACS प्रारूप के लिए समर्थन दर्शाता है।
-नीचे दी गई तालिका कई उपलब्ध एसएमटी सॉल्वरों की कुछ विशेषताओं का सारांश प्रस्तुत करती है। कॉलम SMT-LIB, SMT-LIB भाषा के साथ अनुकूलता दर्शाता है; 'हाँ' चिह्नित कई प्रणालियाँ केवल SMT-LIB के पुराने संस्करणों का समर्थन कर सकती हैं, या भाषा के लिए केवल आंशिक समर्थन प्रदान कर सकती हैं। कॉलम सीवीसी इसके लिए समर्थन दर्शाता है {{abbr|CVC|Cooperating Validity Checker}} भाषा। कॉलम [[DIMACS]] DIMACS [http://www.satcompetition.org/2009/format-benchmarks2009.html प्रारूप] के लिए समर्थन दर्शाता है।
 परियोजनाएं न केवल सुविधाओं और प्रदर्शन में भिन्न होती हैं, बल्कि आसपास के समुदाय की व्यवहार्यता, परियोजना में इसकी चल रही रुचि और दस्तावेज़ीकरण, सुधार, परीक्षण और संवर्द्धन में योगदान करने की क्षमता में भी भिन्न होती हैं।
+=== मानकीकरण और SMT-COMP सॉल्वर प्रतियोगिता ===
 {| class="wikitable"
 |-
-! colspan="3" | Platform
+! colspan="3" | प्लेटफ़ॉर्म
-! colspan="6" | Features
+! colspan="6" | विशेषताएँ
-! colspan="1" | Notes
+! colspan="1" | टिप्पणियाँ
 |-
-! style="background:#ffdead;" | Name
+! style="background:#ffdead;" | नाम
-! style="background:#ffdead;" | OS
+! style="background:#ffdead;" | ओएस
-! style="background:#ffdead;" | License
+! style="background:#ffdead;" | लाइसेंस
 ! style="background:#ffdead;" | SMT-LIB
 ! style="background:#ffdead;" | CVC
-! style="background:#ffdead;" | DIMACS
+! style="background:#ffdead;" | डायमैक
-! style="background:#ffdead;" | Built-in theories
+! style="background:#ffdead;" | अंतर्निर्मित सिद्धांत
-! style="background:#ffdead;" | API
+! style="background:#ffdead;" | एपीआई
-! style="background:#ffdead;" | SMT-COMP [http://www.smtcomp.org/]
+! style="background:#ffdead;" | SMT-कॉम्प[http://www.smtcomp.org/]
 !
 |-
 | ABsolver
-| [[Linux]]
+| लिनक्स
 | [[Common Public License|CPL]]
 | {{yes|v1.2}}
 | {{no}}
 | {{yes}}
-| linear arithmetic, non-linear arithmetic
+| रैखिक अंकगणित, अरेखीय अंकगणित
 | [[C++]]
 | no
-| DPLL-based
+| डीपीएलएल-बेस्ड
 |-
 | [[Alt-Ergo]]
-| [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]]
+| लिनक्स , मैक ओएस , विंडोज़
 | [[CeCILL-C]] (roughly equivalent to [[LGPL]])
 | {{yes|partial v1.2 and v2.0}}
 | {{no}}
 | {{no}}
-| [[empty theory]], linear integer and rational arithmetic, non-linear arithmetic, [[polymorphic array]]s, [[enumerated datatype]]s, [[AC symbol]]s, [[bitvector]]s, [[record datatype]]s, [[Quantifier (logic)|quantifier]]s
+| रिक्त सिद्धांत , रैखिक पूर्णांक और तर्कसंगत अंकगणित, गैर-रेखीय अंकगणित, बहुरूपी ऐरे , प्रगणित डेटा प्रकार , एसी प्रतीक , बिटवेक्टर , रिकॉर्ड डेटा प्रकार , क्वांटिफायर
 | [[OCaml]]
 | 2008
-| Polymorphic first-order input language à la ML, SAT-solver based, combines Shostak-like and Nelson-Oppen like approaches for reasoning modulo theories
+|बहुरूपी प्रथम-क्रम इनपुट लैंग्वेज à la ML, SAT-सॉल्वर बेस्ड, तर्क मॉड्यूल सिद्धांतों के लिए शोस्ताक-जैसे और नेल्सन-ओपेन जैसे दृष्टिकोणों को जोड़ती है
 |-
 | Barcelogic
-| [[Linux]]
+| लिनक्स
 | Proprietary
 | {{yes|v1.2}}
 |
 |
-| [[empty theory]], [[difference logic]]
+| खोखला सिद्धांत , अंतर तर्क
 | [[C++]]
 | 2009
-| DPLL-based, [[congruence closure]]
+| डीपीएलएल-बेस्ड, सर्वांगसमता समापन
 |-
 | Beaver
-| [[Linux]], [[Microsoft Windows|Windows]]
+| लिनक्स , विंडोज़
 | [[BSD licenses|BSD]]
 | {{yes|v1.2}}
 | {{no}}
 | {{no}}
-| bitvectors
+| बिटवेक्टर
 | [[OCaml]]
 | 2009
-| SAT-solver based
+| SAT-सॉल्वर बेस्ड
 |-
 | Boolector
-| [[Linux]]
+| लिनक्स
 | [[MIT License|MIT]]
 | {{yes|v1.2}}
 | {{no}}
 | {{no}}
-| [[bitvector]]s, arrays
+| बिटवेक्टर , ऐरे
 | [[C (programming language)|C]]
 | 2009
-| SAT-solver based
+| SAT-सॉल्वर बेस्ड
 |-
 | CVC3
-| [[Linux]]
+| लिनक्स
 | [[BSD licenses|BSD]]
 | {{yes|v1.2}}
 | {{yes}}
 |
-| [[empty theory]], linear arithmetic, arrays, tuples, types, records, bitvectors, [[Quantifier (logic)|quantifier]]s
+| रिक्त सिद्धांत , रैखिक अंकगणित, ऐरे, टुपल्स, प्रकार, रिकॉर्ड, बिटवेक्टर, क्वांटिफायर
 | [[C (programming language)|C]]/[[C++]]
 | 2010
-| proof output to [[Higher-order logic|HOL]]
+| HOL को प्रूफ़ आउटपुट
 |-
 | CVC4
-| [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]], [[FreeBSD]]
+| लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी
 | [[BSD licenses|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
+| संस्करण 1.8 मई 2021 में जारी किया गया
 |-
-| cvc5
+| CVC5
-| [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]]
+| लिनक्स , मैक ओएस , विंडोज़
 | [[BSD licenses|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
+| संस्करण 1.0 अप्रैल 2022 में जारी किया गया
 |-
-| Decision Procedure Toolkit (DPT)
+|Decision Procedure Toolkit (DPT)
-| [[Linux]]
+| लिनक्स
 | [[Apache license|Apache]]
 | {{no}}
@@ Line 205: / Line 203: @@
 | [[OCaml]]
 | no
-| DPLL-based
+| डीपीएलएल-बेस्ड
 |-
 | iSAT
-| [[Linux]]
+| लिनक्स
 | Proprietary
 | {{no}}
 |
 |
-| non-linear arithmetic
+| अरेखीय अंकगणित
 |
 | no
-| DPLL-based
+| डीपीएलएल-बेस्ड
 |-
 | MathSAT
-| [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]]
+| लिनक्स , मैक ओएस , विंडोज़
 | Proprietary
 | {{yes}}
 |
 | {{yes}}
-| [[empty theory]], linear arithmetic, nonlinear arithmetic, bitvectors, arrays
+| रिक्त सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, ऐरे
 | [[C (programming language)|C]]/[[C++]], [[Python (programming language)|Python]], [[Java (programming language)|Java]]
 | 2010
-| DPLL-based
+| डीपीएलएल-बेस्ड
 |-
 | MiniSmt
-| [[Linux]]
+| लिनक्स
 | [[LGPL]]
 | {{yes|partial v2.0}}
 |
 |
-| non-linear arithmetic
+| अरेखीय अंकगणित
 |[[OCaml]]
 | 2010
-| SAT-solver based, Yices-based
+| SAT-सॉल्वर बेस्ड, Yices-बेस्ड
 |-
 | Norn
@@ Line 249: / Line 247: @@
 |
 |
-| SMT solver for string constraints
+| स्ट्रिंग बाधाओं के लिए SMT सॉल्वर
 |-
+|
+|लिनक्स
 |-
 | [[OpenCog]]
-| [[Linux]]
+| लिनक्स
 | [[Affero General Public License|AGPL]]
 | {{no}}
 | {{no}}
 | {{no}}
-| [[probabilistic logic]], arithmetic. [[relational model]]s
+| संभाव्य तर्क , अंकगणित। संबंधपरक मॉडल
 | [[C++]], [[Scheme (programming language)|Scheme]], [[Python (programming language)|Python]]
 | no
-| subgraph isomorphism
+| सबग्राफ समरूपता
 |-
 | OpenSMT
-| [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]]
+| लिनक्स , मैक ओएस , विंडोज़
 | [[GPLv3]]
 | {{yes|partial v2.0}}
 |
 | {{yes}}
-| [[empty theory]], differences, linear arithmetic, bitvectors
+| रिक्त सिद्धांत , अंतर, रैखिक अंकगणित, बिटवेक्टर
 | [[C++]]
 | 2011
-| lazy SMT Solver
+| लेजी SMT सॉल्वर
 |-
 |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
@@ Line 291: / Line 291: @@
 |
 |
-| linear arithmetic, difference logic
+| रैखिक अंकगणित, अंतर तर्क
 | none
 | 2009
@@ Line 297: / Line 297: @@
 |-
 | SMTInterpol
-| [[Linux]], [[Mac OS]], [[Windows]]
+| लिनक्स , मैक ओएस , विंडोज़
 | [[LGPLv3]]
 | {{yes|v2.5|align=|style=|color=}}
 |
 |
-| uninterpreted functions, linear real arithmetic, and linear integer arithmetic
+| अव्याख्यायित फलन, रैखिक वास्तविक अंकगणित, और रैखिक पूर्णांक अंकगणित
 | [[Java (programming language)|Java]]
 | 2012
-| Focuses on generating high quality, compact interpolants.
+| उच्च गुणवत्ता, कॉम्पैक्ट इंटरपोलेंट उत्पन्न करने पर ध्यान केंद्रित करता है।
 |-
 | SMCHR
-| [[Linux]], [[Mac OS]], [[Windows]]
+| लिनक्स , मैक ओएस , विंडोज़
 | [[GPLv3]]
 | {{no}}
 | {{no}}
 | {{no}}
-| linear arithmetic, nonlinear arithmetic, heaps
+| रैखिक अंकगणित, अरेखीय अंकगणित, हीप
 | [[C (programming language)|C]]
 | no
-| Can implement new theories using [[Constraint Handling Rules]].
+| बाधा प्रबंधन नियमों का उपयोग करके नए सिद्धांतों को लागू कर सकते हैं ।
 |-
 | SMT-RAT
-| [[Linux]], [[Mac OS]]
+| लिनक्स , मैक ओएस
 | [[MIT License|MIT]]
 | {{yes|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.
+| रणनीतिक और समानांतर SMT समाधान के लिए टूलबॉक्स जिसमें SMT अनुरूप कार्यान्वयन का संग्रह सम्मिलित है।
 |-
 | SONOLAR
-| [[Linux]], [[Microsoft Windows|Windows]]
+| लिनक्स , विंडोज़
 | Proprietary
 | {{yes|partial v2.0}}
 |
 |
-| bitvectors
+| बिटवेक्टर
 | [[C (programming language)|C]]
 | 2010
-| SAT-solver based
+| SAT-सॉल्वर बेस्ड
 |-
 | Spear
-| [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]]
+| लिनक्स , मैक ओएस , विंडोज़
 | Proprietary
 | {{yes|v1.2}}
 |
 |
-| bitvectors
+| बिटवेक्टर
 |
 | 2008
@@ Line 352: / Line 352: @@
 |-
 | STP
-| [[Linux]], [[OpenBSD]], [[Microsoft Windows|Windows]], [[Mac OS]]
+| लिनक्स , ओपनबीएसडी , विंडोज , मैक ओएस
 | [[MIT License|MIT]]
 | {{yes|partial v2.0}}
 | {{yes}}
 | {{no}}
-| bitvectors, arrays
+| बिटवेक्टर, ऐरे
 | [[C (programming language)|C]], [[C++]], [[Python (programming language)|Python]], [[OCaml]], [[Java (programming language)|Java]]
 | 2011
-| SAT-solver based
+| SAT-सॉल्वर बेस्ड
 |-
 | SWORD
-| [[Linux]]
+| लिनक्स
 | Proprietary
 | {{yes|v1.2}}
 |
 |
-| bitvectors
+| बिटवेक्टर
 |
 | 2009
@@ Line 374: / Line 374: @@
 |-
 | UCLID
-| [[Linux]]
+| लिनक्स
 | [[BSD licenses|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!
+| SAT-सॉल्वर बेस्ड, मॉस्को एमएल में लिखा गया । इनपुट लैंग्वेज एसएमवी मॉडल चेकर है। अच्छी तरह से प्रलेखित!
 |-
 | veriT
-| [[Linux]], [[OS X]]
+| लिनक्स , ओएस एक्स
 | [[BSD licenses|BSD]]
 | {{yes|partial v2.0}}
 |
 |
-| [[empty theory]], rational and integer linear arithmetics, quantifiers, and equality over uninterpreted function symbols
+| रिक्त सिद्धांत , तर्कसंगत और पूर्णांक रैखिक अंकगणित, परिमाणक, और अबाधित फ़ंक्शन प्रतीकों पर समानता
 | [[C (programming language)|C]]/[[C++]]
 | 2010
-| SAT-solver based, can produce proofs
+| SAT-सॉल्वर बेस्ड, प्रमाण प्रस्तुत कर सकते हैं
 |-
 | {{Visible anchor|Yices}}
-| [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]], [[FreeBSD]]
+| लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी
 | [[GPLv3]]
 | {{yes| v2.0}}
 | {{no}}
 | {{yes}}
-| rational and integer linear arithmetic, bitvectors, arrays, and equality over uninterpreted function symbols
+| तर्कसंगत और पूर्णांक रैखिक अंकगणित, बिटवेक्टर, ऐरे, और अबाधित फ़ंक्शन प्रतीकों पर समानता
 | [[C (programming language)|C]]
 | 2014
-| Source code is available online
+| सोर्स कोड ऑनलाइन उपलब्ध है
 |-
 | [[Z3 Theorem Prover]]
-| [[Linux]], [[Mac OS]], [[Microsoft Windows|Windows]], [[FreeBSD]]
+| लिनक्स , मैक ओएस , विंडोज , फ्रीबीएसडी
 | [[MIT License|MIT]]
 | {{yes| v2.0}}
 |
 | {{yes}}
-| [[empty theory]], linear arithmetic, nonlinear arithmetic, bitvectors, arrays, datatypes, [[Quantifier (logic)|quantifier]]s, strings
+| रिक्त सिद्धांत , रैखिक अंकगणित, अरेखीय अंकगणित, बिटवेक्टर, ऐरे, डेटाटाइप, क्वांटिफायर , स्ट्रिंग्स
 | [[C (programming language)|C]]/[[C++]], [[.NET Framework|.NET]], [[OCaml]], [[Python (programming language)|Python]], [[Java (programming language)|Java]], [[Haskell (programming language)|Haskell]]
 | 2011
-| Source code is available online
+| सोर्स कोड ऑनलाइन उपलब्ध है
 |}
 === मानकीकरण और SMT-COMP सॉल्वर प्रतियोगिता ===
-एसएमटी सॉल्वरों के लिए एक मानकीकृत इंटरफ़ेस का वर्णन करने के लिए कई प्रयास किए गए हैं (और स्वचालित प्रमेय साबित करना, एक शब्द जिसे अक्सर समानार्थक रूप से उपयोग किया जाता है)। सबसे प्रमुख है SMT-LIB मानक,{{citation needed|reason=Provide a source for the standard definition; similar for other standards.|date=October 2020}} जो [[ एस-अभिव्यक्ति ]] पर आधारित भाषा प्रदान करता है। आमतौर पर समर्थित अन्य मानकीकृत प्रारूप DIMACS प्रारूप हैं{{citation needed|date=October 2020}} कई बूलियन सैट सॉल्वर और सीवीसी प्रारूप द्वारा समर्थित{{citation needed|date=October 2020}} सीवीसी स्वचालित प्रमेय कहावत द्वारा उपयोग किया जाता है।
+SMT सॉल्वरों (और स्वचालित प्रमेय प्रोवर्स, एक शब्द जिसे प्रायः समानार्थक रूप से उपयोग किया जाता है) के लिए एक मानकीकृत इंटरफ़ेस का वर्णन करने के कई प्रयास किए गए हैं। सबसे प्रमुख SMT-LIB मानक है, जो S-अभिव्यक्ति पर बेस्ड लैंग्वेज प्रदान करता है। सामान्यतः समर्थित अन्य मानकीकृत प्रारूप कई बूलियन SAT सॉल्वरों द्वारा समर्थित डीआईएमएसीएस प्रारूप हैं, और CVC प्रारूप CVC स्वचालित प्रमेय प्रोवर द्वारा उपयोग किया जाता है।
-SMT-LIB प्रारूप कई मानकीकृत बेंचमार्क के साथ आता है और इसने SMT-COMP नामक SMT सॉल्वरों के बीच एक वार्षिक प्रतिस्पर्धा को सक्षम किया है। प्रारंभ में, प्रतियोगिता कंप्यूटर एडेड सत्यापन सम्मेलन (सीएवी) के दौरान हुई थी।<ref>{{Cite book|last1=Barrett|first1=Clark|last2=de Moura|first2=Leonardo|last3=Stump|first3=Aaron|date=2005|editor-last=Etessami|editor-first=Kousha|editor2-last=Rajamani|editor2-first=Sriram K.|chapter=SMT-COMP: Satisfiability Modulo Theories Competition|url=https://link.springer.com/chapter/10.1007%2F11513988_4|title=कंप्यूटर सहायता प्राप्त सत्यापन|series=Lecture Notes in Computer Science|volume=3576|publisher=Springer|pages=20–23|doi=10.1007/11513988_4|isbn=978-3-540-31686-2}}</ref><ref>{{Cite book|last1=Barrett|first1=Clark|last2=de Moura|first2=Leonardo|last3=Ranise|first3=Silvio|last4=Stump|first4=Aaron|last5=Tinelli|first5=Cesare|date=2011|editor-last=Barner|editor-first=Sharon|editor2-last=Harris|editor2-first=Ian|editor3-last=Kroening|editor3-first=Daniel|editor4-last=Raz|editor4-first=Orna|chapter=The SMT-LIB Initiative and the Rise of SMT|title=Hardware and Software: Verification and Testing|series=Lecture Notes in Computer Science|volume=6504|publisher=Springer|pages=3|doi=10.1007/978-3-642-19583-9_2|bibcode=2011LNCS.6504....3B|isbn=978-3-642-19583-9|doi-access=free}}</ref> लेकिन 2020 तक प्रतियोगिता को एसएमटी कार्यशाला के हिस्से के रूप में आयोजित किया गया है, जो स्वचालित तर्क (आईजेसीएआर) पर अंतर्राष्ट्रीय संयुक्त सम्मेलन से संबद्ध है।<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-->===
-कंप्यूटर-सहायता प्राप्त औपचारिक सत्यापन अक्सर एसएमटी सॉल्वर का उपयोग करता है। यह निर्धारित करने के लिए कि क्या सभी गुण धारण कर सकते हैं, एक सामान्य तकनीक पूर्व शर्त, पोस्टकंडिशन, लूप स्थिति और एसएमटी सूत्रों में दावे का अनुवाद करना है।
+कंप्यूटर प्रोग्रामों का कंप्यूटर समर्थित सत्यापन प्रायः SMT सॉल्वर का उपयोग करता है। यह निर्धारित करने के लिए कि क्या सभी गुण धारण किए जा सकते हैं, एक सामान्य तकनीक पूर्व शर्त, पोस्टकंडिशन, लूप स्थिति और SMT सूत्रों में दावे का अनुवाद करना है।
-Z3 प्रमेय नीति के शीर्ष पर कई सत्यापनकर्ता बनाए गए हैं। [http://research.microsoft.com/en-us/projects/boogie/ बूगी] एक मध्यवर्ती सत्यापन भाषा है जो सरल अनिवार्य कार्यक्रमों को स्वचालित रूप से जांचने के लिए Z3 का उपयोग करती है। समवर्ती सी के लिए [https://www.microsoft.com/en-us/research/project/vcc-a-verifier-for-concurrent-c/ VCC] सत्यापनकर्ता बूगी का उपयोग करता है, साथ ही अनिवार्य वस्तु-आधारित कार्यक्रमों के लिए [http://research.microsoft.com/en-us/projects/dafny/ Dafny], समवर्ती कार्यक्रमों के लिए [http://research.microsoft.com/en-us/projects/chalice/ चालिस] का उपयोग करता है। , और C# के लिए [http://research.microsoft.com/en-us/projects/specsharp/ Spec#]। [http://research.microsoft.com/en-us/projects/fstar/ F*] एक आश्रित रूप से टाइप की जाने वाली भाषा है जो प्रमाण खोजने के लिए Z3 का उपयोग करती है; कंपाइलर इन सबूतों को प्रूफ-ले जाने वाले बाइटकोड का उत्पादन करने के लिए ले जाता है। [http://viper.ethz.ch वाइपर सत्यापन अवसंरचना] सत्यापन शर्तों को Z3 में एन्कोड करता है। [https://hackage.haskell.org/package/sbv sbv] लाइब्रेरी हास्केल कार्यक्रमों का एसएमटी-आधारित सत्यापन प्रदान करती है, और उपयोगकर्ता को Z3, ABC, Boolector, cvc5, MathSAT और Yices जैसे कई सॉल्वरों में से चुनने देती है।
+Z3 SMT सॉल्वर के शीर्ष पर कई सत्यापनकर्ता बनाए गए हैं। बूगी एक मध्यवर्ती सत्यापन लैंग्वेज है जो सरल अनिवार्य कार्यक्रमों की स्वचालित रूप से जाँच करने के लिए Z3 का उपयोग करती है। समवर्ती सी के लिए वीसीसी सत्यापनकर्ता बूगी का उपयोग करता है, साथ ही अनिवार्य वस्तु-बेस्ड कार्यक्रमों के लिए डैफनी, समवर्ती कार्यक्रमों के लिए चालिस और सी# के लिए स्पेक# का उपयोग करता है। F* एक निर्भरता से टाइप की जाने वाली लैंग्वेज है जो प्रमाण खोजने के लिए Z3 का उपयोग करती है; कंपाइलर इन सबूतों को प्रूफ-ले जाने वाले बाइटकोड का उत्पादन करने के लिए ले जाता है। वाइपर सत्यापन अवसंरचना सत्यापन शर्तों को Z3 में एनकोड करती है। एसबीवी लाइब्रेरी हास्केल कार्यक्रमों का SMT-बेस्ड सत्यापन प्रदान करती है, और उपयोगकर्ता को Z3, एबीसी, बूलेक्टर, CVC5, मैथसैट और येस जैसे कई सॉल्वरों में से चुनने की सुविधा देती है।
-[http://alt-ergo.ocamlpro.com/ Alt-Ergo] SMT सॉल्वर के शीर्ष पर कई सत्यापनकर्ता भी बनाए गए हैं। यहां परिपक्व अनुप्रयोगों की एक सूची दी गई है:
+* ऑल्ट-एर्गो SMT सॉल्वर के ऊपर कई सत्यापनकर्ता भी बनाए गए हैं। यहां परिपक्व आवेदनों की सूची दी गई है:
-* [http://why3.lri.fr/When3], डिडक्टिव प्रोग्राम सत्यापन के लिए एक मंच, Alt-Ergo को अपने मुख्य कहावत के रूप में उपयोग करता है;
+* व्हाय3, डिडक्टिव प्रोग्राम सत्यापन के लिए एक मंच, ऑल्ट-एर्गो को अपने मुख्य कहावत के रूप में उपयोग करता है;
-* कैविएट, सीईए द्वारा विकसित और एयरबस द्वारा उपयोग किया जाने वाला एक सी-सत्यापनकर्ता; Alt-Ergo को इसके हालिया विमानों में से एक की योग्यता DO-178C में शामिल किया गया था;
+* कैविएट, सीईए द्वारा विकसित और एयरबस द्वारा उपयोग किया जाने वाला एक सी-सत्यापनकर्ता; ऑल्ट-एर्गो को इसके हालिया विमानों में से एक की योग्यता DO-178C में सम्मिलित किया गया था;
-* [[Frama-C]], C-कोड का विश्लेषण करने के लिए एक ढांचा, जेसी और WP प्लगइन्स (डिडक्टिव प्रोग्राम वेरिफिकेशन के लिए समर्पित) में Alt-Ergo का उपयोग करता है;
+* फ्रैमा-सी, सी-कोड का विश्लेषण करने के लिए एक ढांचा, जेसी और डब्ल्यूपी प्लगइन्स ("डिडक्टिव प्रोग्राम वेरिफिकेशन" के लिए समर्पित) में ऑल्ट-एर्गो का उपयोग करता है;
-* SPARK (प्रोग्रामिंग भाषा) SPARK 2014 में कुछ दावों के सत्यापन को स्वचालित करने के लिए CVC4 और Alt-Ergo (GNATprove के पीछे) का उपयोग करता है;
+* स्पार्क 2014 में कुछ दावों के सत्यापन को स्वचालित करने के लिए स्पार्क CVC4 और ऑल्ट-एर्गो (GNATprove के पीछे) का उपयोग करता है;
-* [[ बी-विधि ]]|एटेलियर-बी अपने मुख्य प्रोवर के बजाय Alt-Ergo का उपयोग कर सकता है ([http://alt-ergo.lri.fr/documents/ABZ-2014.pdf ANR Bware प्रोजेक्ट बेंचमार्क] पर सफलता 84% से बढ़कर 98% हो गई है);
+* एटेलियर-बी अपने मुख्य प्रोवर के बजाय ऑल्ट-एर्गो का उपयोग कर सकता है (एएनआर बीवेयर प्रोजेक्ट बेंचमार्क पर सफलता 84% से बढ़कर 98% हो गई है);
-* [[रॉडिन उपकरण]], सिस्टरेल द्वारा विकसित एक बी-मेथड फ्रेमवर्क, ऑल्ट-एर्गो को बैक-एंड के रूप में उपयोग कर सकता है;
+* रॉडिन, सिस्टरेल द्वारा विकसित एक बी-मेथड फ्रेमवर्क, ऑल्ट-एर्गो को बैक-एंड के रूप में उपयोग कर सकता है;
-* [http://cubicle.lri.fr/ क्यूबिकल], सरणी-आधारित संक्रमण प्रणालियों के सुरक्षा गुणों को सत्यापित करने के लिए एक खुला स्रोत मॉडल चेकर।
+* क्यूबिकल, सरणी-बेस्ड संक्रमण प्रणालियों की सुरक्षा गुणों की पुष्टि के लिए एक खुला सोर्स मॉडल चेकर।
-* [https://www.easycrypt.info/ EasyCrypt], प्रतिकूल कोड के साथ संभाव्य संगणनाओं के संबंधपरक गुणों के बारे में तर्क करने के लिए एक टूलसेट।
+* ईज़ीक्रिप्ट, प्रतिकूल कोड के साथ संभाव्य संगणनाओं के संबंधपरक गुणों के बारे में तर्क करने के लिए एक टूलसेट।
-कई एसएमटी सॉल्वर एक सामान्य इंटरफ़ेस प्रारूप लागू करते हैं जिसे [http://smt-lib.org/ SMTLIB2] कहा जाता है (ऐसी फ़ाइलों में आमतौर पर एक्सटेंशन होता है<code>.smt2</code>). [https://ucsd-progsys.github.io/liquidhaskell-blog/ LiquidHaskell]
+कई SMT सॉल्वर SMTLIB2 नामक एक सामान्य इंटरफ़ेस प्रारूप लागू करते हैं (ऐसी फ़ाइलों में सामान्यतः एक्सटेंशन "<code>.smt2</code>" होता है)।  लिक्विडहास्केल उपकरण हास्केल के लिए एक परिशोधन प्रकार-बेस्ड सत्यापनकर्ता लागू करता है जो किसी भी SMTLIB2 अनुरूप सॉल्वर का उपयोग कर सकता है, जैसे cvc5, MathSat, या Z3।
-टूल हास्केल के लिए एक शोधन प्रकार आधारित सत्यापनकर्ता लागू करता है जो किसी भी SMTLIB2 अनुरूप सॉल्वर का उपयोग कर सकता है, उदाहरण के लिए cvc5, MathSat, या Z3।
-===प्रतीकात्मक-निष्पादन आधारित विश्लेषण और परीक्षण===
+===सांकेतिक-निष्पादन बेस्ड विश्लेषण एवं परीक्षण===
+SMT सॉल्वरों का एक महत्वपूर्ण एप्लीकेशन प्रोग्राम के विश्लेषण और परीक्षण के लिए प्रतीकात्मक निष्पादन है (उदाहरण के लिए, कॉन्कोलिक परीक्षण), जिसका उद्देश्य विशेष रूप से सुरक्षा कमजोरियों का पता लगाना है। इस श्रेणी के उदाहरण टूल में [[माइक्रोसॉफ्ट रिसर्च]] से [http://research.microsoft.com/en-us/um/people/pg/public_psfiles/ndss2008.pdf SAGE], [https://klee.github.io/ KLEE], [http://s2e.epfl.ch/ S2E] और [https://triton.quarkslab.com ट्राइटन]शामिल हैं। SMT सॉल्वर जिनका उपयोग प्रतीकात्मक-निष्पादन अनुप्रयोगों के लिए किया गया है, उनमें [https://github.com/Z3Prover/z3 Z3], [https://sites.google.com/site/stpfastprover/ एसटीपी] आर्काइव्ड 2015-04-06 वेबैक मशीन, सॉल्वर का Z3str समहू और बूलेक्टर सम्मिलित हैं।
-एसएमटी सॉल्वरों का एक महत्वपूर्ण अनुप्रयोग कार्यक्रमों के विश्लेषण और परीक्षण के लिए प्रतीकात्मक निष्पादन है (उदाहरण के लिए, कॉन्कोलिक परीक्षण), जिसका उद्देश्य विशेष रूप से सुरक्षा कमजोरियों का पता लगाना है।{{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 सॉल्वर
-* बूलियन संतुष्टि समस्या#SAT को हल करने के लिए एल्गोरिदम
+* फर्स्ट-आर्डर लॉजिक
-* प्रथम-क्रम तर्क
+* थ्योरी ऑफ़ पुरे इक्वलिटी
-*[[शुद्ध समानता का सिद्धांत]]
 ==टिप्पणियाँ==
@@ Line 480: / Line 474: @@
 {{refend}}
 {{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: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:संतुष्टि की समस्या]]

Anonymous

Search

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

Latest revision as of 13:58, 14 August 2023

मूल शब्दावली

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

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

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

सॉल्वर

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

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

अनुप्रयोग

सत्यापन

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

यह भी देखें

टिप्पणियाँ

संदर्भ

Navigation

Wiki tools

Page tools

Other projects

Categories