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

कंप्यूटर विज्ञान और गणितीय तर्क में, संतुष्टि मॉड्यूल सिद्धांत (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 सॉल्वरों को भी बढ़ाया गया है।

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

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

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

सॉल्वर

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

अनुप्रयोग

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

सत्यापन

कंप्यूटर प्रोग्रामों का कंप्यूटर समर्थित सत्यापन प्रायः 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 सॉल्वर
• फर्स्ट-आर्डर लॉजिक
• थ्योरी ऑफ़ पुरे इक्वलिटी

संदर्भ

• 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