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

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

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

मूल शब्दावली

औपचारिक रूप से कहें तो, एक एसएमटी उदाहरण प्रथम-क्रम तर्क में एक सूत्र है, जहां कुछ फ़ंक्शन और विधेय प्रतीकों की अतिरिक्त व्याख्याएं होती हैं, और एसएमटी यह निर्धारित करने की समस्या है कि क्या ऐसा सूत्र संतोषजनक है। दूसरे शब्दों में, बूलियन संतुष्टि समस्या (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} }.$

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

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

समाधानकर्ता

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

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

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

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

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

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

अनुप्रयोग

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

सत्यापन

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

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

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

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

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

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

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

यह भी देखें

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