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

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

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

मूल शब्दावली

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

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

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

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

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

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

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

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

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

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

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

${\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} }.$

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

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

सॉल्वर

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

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

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

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

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

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

अनुप्रयोग

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

सत्यापन

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

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

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

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

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

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

यह भी देखें

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

संदर्भ

• 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