صدق‌پذیری در پیمانه نظریات: تفاوت میان نسخه‌ها

محتوای حذف‌شده محتوای افزوده‌شده

درخط

نسخهٔ ‏۱۱ مهٔ ۲۰۲۱، ساعت ۱۱:۱۵

یک مسئله صدق‌پذیری در پیمانه نظریات (به انگلیسی: satisfiability modulo theories) با کوته‌نوشت 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$ داشته باشد.

بیشتر حل کننده های مسئله SAT فقط از قسمت های فاقد سور از منطق‌شان پشتیبانی می‌کنند.

قدرت بیان

یک نمونه مسئله SMT یک تعمیم برای نمونه مسئله SAT دودویی است، که در آن مجموعه های متنوعی از متغیرها با گزاره هایی از انواع متنوعی از نظریه‌های بنیادین جایگزین شده اند. فرمول‌های SMT قدرت مدل‌سازی بیشتری نسبت به فرمول‌های دودویی SAT دارند. برای مثال، یک فرمول SMT به ما امکان مدل‌سازی عملیات دیتاپت (مسیرداده) برای یک ریزپردازنده را در سطح کلمه (و نه سطح بیت) می دهد.

برای مقایسه، برنامه‌نویسی مجموعه جواب نیز براساس گزاره‌ها است (به صورت دقیق‌تر، یک جمله اتمی است که از فرمول‌های اتمی ساخته شده است). برخلاف SMT، برنامه‌های مجموعه جواب، سور ندارند، و نمی توانند محدودیت هایی مثل حساب خطی یا منطق تفاوت را به سادگی بیان کنند- ASP به عنوان بهترین راه‌حل برای مسائل دودویی هستند که به نظریه آزاد توابع تفسیرنشده کاهش یافته اند. پیاده سازی اعداد صحیح 32 بیتی به عنوان آرایه‌بیتی در ASP از مسائل مشابهی رنج می برند که حل کننده های اولیه SMT ها با آن مواجه بودند: برابری های «بدیهی» مثل x+y=y+x به سختی قابل استنتاج هستند.

برنامه‌نویسی منطقی محدودیت از محدودیت های حسابی خطی پشتیبانی می کنند، اما آن‌ها در چارچوب نظری کاملا متفاوتی قرار دارند. حل‌کننده های SMT برای حل فرمول‌هایی در منطق مرتبه بالاتر گسترش یافته اند.^[۱]

دیدگاه‌های حل‌کننده

تلاش‌های اولیه برای حل نمونه‌های مسئله SMT شامل ترجمه آن‌ها به نمونه مسائل SAT دودویی بود (مثلا یک متغیر صحیح 32 بیتی توسط 32 عدد متغیر تک بیتی با وزن‌های مناسب و عملیات سطح کلمه مثل «جمع» با عملیات منطقی سطح پایینی روی بیت ها جایگزین می شدند) سپس این فرمول به حل کننده SAT دودویی تحویل می شد. به این دیدگاه، دیدگاه حریصانه هم می گویند، و دارای مزیت‌هایی هم هست: با پیش‌پردازش یم فرمول SMT به یک فرمول SAT دودویی معادل، حل‌کننده های SAT دودویی موجود را می توان به صورتی که هست استفاده کرد، مزیت هایش از نظر کارایی و ظرفیت در طی زمان بیشتر می شود. از جهت دیگر، فقدان وجود معناشناسی سطح بالا برای نظریه‌های بنیادین، یعنی حل‌کننده دودویی SAT باید خیلی بیشتر از آنچه برای برای کشف واقعیت‌های «بدیهی» لازم است، کار کند (مثلا $x+y=y+x$ برای جمع اعداد صحیح). این مشاهده منجر به ایجاد تعدادی از حل کننده های SMT شد که به شدت استنتاج دودویی یک جستجوی با سبک DPLL را به حل‌کننده‌های خاص نظریه (T-solvers) که به عطف‌های(ANDs) از گزاره‌ها از یک نظریه معین رسیدگی می کند، یکپارچه‌سازی می‌کرد. به این دیدگاه، دیدگاه کندرو هم گفته می شود.

DPLL(T) دوبل (دوتایی)^[۲] که این معماری مسئولیت استنتاج دودویی به حل کننده SAT مبتنی بر DPLL داده می شود، که به نوبه خود با یک حل کننده برای نظریه T از طریق یک واسط خوش‌تعریف تعامل دارد. حل کننده نظریه فقط باید در مورد بررسی امکان عطف‌دهی به گزاره‌های نظریه ارسال شده به آن، از حل‌کننده 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 که می خواهند ترکیبات دودویی اتم نظریه از نظریات حسابی تصمیم‌ناپذیر روی اعداد حقیقی رسیدگی کنند، ABsolver^[۳] نام دارند، که از یک معماری کلاسیک DPLL(T) با یک بسته بهینه‌سازی غیرخطی به عنوان حل‌کننده نظریه فرعی (به صورت لازم غیرکامل) استفاده می کنند، و iSAT که روی یک اتحاد حل‌کننده DPLL SAT و انتشار محدودیت بازه‌ای ساخته شده اند، که الگوریتم iSAT نامیده می شود.^[۴]

حل‌کننده‌ها

جدول زیر بعضی از ویژگی‌های چند تا از حل کننده های SMT موجود را خلاصه‌بندی نموده است. ستون «SMT-LIB» نشان‌دهنده سازگاری با زبان SMT-LIB است؛ بیشتر سامانه‌هایی را که با 'yes' نشان‌گذاری کرده ایم، فقط از نسخه های قدیمی SMT-LIB پشتیبانی می کنند، یا اینکه فقط پشتیبانی جزئی از زبان دارند. ستون «CVC» نشان‌دهنده پشتیبانی از زبان CVC است. ستون «DIMACS» نشان‌دهنده پشتیبانی از قالب DIMACS است.

این پروژه ها نه فقط از نظر ویژگی و کارایی با هم فرق دارند، بلکه از نظر زیست‌پذیری انجمن اطراف شان، علاقه پیشرونده به پروژه و توانمندی مشارکت مستندات، تعمیرها، تست‌ها و ارتقا با هم تفاوت دارند.

استانداردسازی و مسابقه حل‌کننده SMT-COMP

تلاش های زیادی برای توصیف یک واسط استاندارد شده برای حل کننده SMT (و اثبات‌گر قضیه خودکار، که یک اصطلاح هم‌معنی است) وجود دارد. برجسته‌ترین آن‌ها استاندارد SMT-LIB است که یک زبان بر اساس عبارات S تهیه دیده است. دیگر قالب‌های استاندارد شده که معمولا پشتیبانی می شوند شامل قالب DIMACS است که توسط خیلی از حل‌کننده‌های SAT بولی پشتیبانی می شود، و قالب CVC که توسط اثبات‌گر قضیه خودکار CVC استفاده می شود.

قالب SMT-LIB همراه با تعدادی از محک‌زنی (benchmark) استاندارد آمده است، و این موضوع یک مسابقه سالانه بین حل‌کننده های SMT را امکان‌پذیر نموده است که به آن SMT-COMP گفته می شود. در ابتدا، مسابقه در همایش درستی‌سنجی به کمک رایانه (CAV)^[۵]^[۶] قرار داشت، اما از سال 2020 مسابقه به عنوان بخشی از کارگاه SMT قرار گرفت، که به همایش ترکیبی بین‌المللی روی استنتاج خودکار (IJCAR) وابسته بود.^[۷]

کاربردها

حل‌کننده های SMT هم برای درستی‌سنجی، اثبات درستی برنامه‌ها، آزمون نرم‌افزار براساس اجرای نمادین، و نیز برای ترکیب، تولید قطعه های برنامه با جستجو روی فضای برنامه‌های ممکن مفید است. در خارج از حیطه درستی‌سنجی نرم‌افزار، از حل‌کننده SMT برای استنتاج نوع،^[۸]^[۹] و نیز برای مدل‌سازی سناریوهای نظری، شامل مدل‌سازی اعتقادات کنشگر در کنترل نیروی هسته‌ای استفاده شده است.^[۱۰]

درستی‌سنجی

درستی‌سنجی برنامه‌های رایانه‌ای به کمک رایانه معمولا از حل کننده SMT استفاده می کنند. یک روش معمول ترجمه پیش‌شرط، پس‌شرط، شرط حلقه، و ادعاها به فرمول‌های SMT است، که هدف آن است که تعیین شود، آیا همه ویژگی ها برقرار است یا نه.

درستی‌سنج‌های زیادی روی حل کننده Z3 SMT ساخته شده است. Boogie یک زبان درستی‌سنجی سطح میانی است که از Z3 استفاده می کند تا به صورت خودکار برنامه‌های دستوری ساده را بررسی کند. درستی‌سنج VCC برای C همزمان از Boogie، و نیز از Dafny برای برنامه‌های مبتنی بر شیء دستوری استفاده می کند و از Chalice برای برنامه های همزمان استفاده می کند، و از Spec# برای C# استفاده می کند. زبان F* یک زبان نوع دار وابسته است که از Z3 برای یافتن اثبات استفاده می کند؛ کامپایلر این اثبات‌ها را حمل می کند تا بایت‌کد حامل اثبات را تولید کند. زیرساخت درستی‌سنجی Viper شرایط درستی‌سنجی را به Z3 کدبندی می کند. کتابخانه sbv درستی‌سنجی مبتنی بر SMT را برای برنامه‌های زبان Haskell تهیه می بیند، و به کاربر کمک می کند تا از بین تعدادی از حل‌کننده ها مثل Z3، ABC، Boolector، CVC4، MathSat، و Yices انتخاب انجام دهد.

درستی‌سنج‌های زیادی روی حل‌کننده SMT با نام Alt-Ergo ساخته شده اند. در ادامه فهرستی از کاربردهای به بلوغ رسیده آمده است:

Why3: یک بن‌سازه برای درستی‌سنجی برنامه به صورت استقرایی، که از Alt-Ergo به عنوان اثبات کننده اصلی استفاده می کند.

CAVEAT، یک درستی‌سنج C که توسط CEA توسعه یافته است، و توسط شرکت Airbus استفاده می شود؛ Alt-Ergo در یکی از صلاحیت سنجی DO-178C از یکی از هواپیماهای جدیدش قرار گرفته است.

Frama-C، یک چارچوب برای تحلیل کد C است، از Alt-Ergo در افزونه های Jessie و WP استفاده می کند (که اختصاص به «درستی‌سنجی برنامه استقرایی» دارد)؛

SPARK، از CVC4 و Alt-Ergo (که پشت GNATprove قرار دارد) استفاده می کند تا درستی‌سنجی بعضی از ادعا ها را در SPARK 2014 خودکارسازی کند؛

Atelier-B می تواند از Alt-Ergo به جای اثبات‌گر اصلی اش استفاده کند (این کار موجب افزایش موفقیت از 84% به 98% در محک‌زنی‌های پروژه ANR Bware می شود)؛

Rodin، یک چارچوب روش-B است که توسط Systertel توسعه یافته است و می تواند از Alt-Ergo به عنوان یک back-end استفاده کند.

Cubicle یک بررسی‌کننده مدل متن‌باز است که از آن برای درستی‌سنجی ویژگی‌های امنیتی برای سامانه‌های تبدیل مبتنی بر آرایه‌ استفاده می شود.

EasyCrypt، یک جعبه ابزار برای استنتاج درباره ویژگی‌های رابطه‌ای در محاسبات احتمالی است، که کد خصومتی دارد.

بسیاری از حل‌کننده های SMT یک قالب واسط معمول که SMTLIB نامیده می شود را پیاده‌سازی می کنند (این فایل‌ها معمولا پسوند ".smt2" دارند). ابزار LiquidHaskell یک درستی‌سنج مبتنی بر نوع اصلاحی برای Haskell را پیاده سازی می کند، که می تواند از هر حل‌کننده سازگار با SMTLIB2 (مثل CVC4، MathSat یا Z3) استفاده کند.

تحلیل و آزمون مبتنی بر اجرای نمادین

یک کاربرد مهم برای حل‌کننده SMT، اجرای نمادین برای تحلیل و آزمون برنامه‌ها است (مثل تست کلونیک)، که مخصوصا در پیدا کردن آسیب‌پذیری‌های امنیتی کمک کننده است. ابزارهای مهمی که به صورت فعال نگهداری می شوند در این زمینه شامل SAGE، از تحقیق مایکروسافت، KLEE، S2E و Triton است. حل‌کننده های SMT که مخصوصا در کاربردهای اجرای نمادین مفید است شامل Z3، STP، Z3str2، و Boolector است.

پانویس

↑ Barbosa, Haniel, et al. "Extending SMT solvers to higher-order logic." International Conference on Automated Deduction. Springer, Cham, 2019.
↑ Nieuwenhuis, R.; Oliveras, A.; Tinelli, C. (2006), "Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)", Journal of the ACM (PDF), vol. 53, pp. 937–977
↑ 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", JSAT Special Issue on SAT/CP Integration (PDF), vol. 1, pp. 209–236
↑ Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). Etessami, Kousha; Rajamani, Sriram K. (eds.). "SMT-COMP: Satisfiability Modulo Theories Competition". Computer Aided Verification. Lecture Notes in Computer Science (به انگلیسی). Berlin, Heidelberg: Springer: 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). Barner, Sharon; Harris, Ian; Kroening, Daniel; Raz, Orna (eds.). "The SMT-LIB Initiative and the Rise of SMT". Hardware and Software: Verification and Testing. Lecture Notes in Computer Science (به انگلیسی). Berlin, Heidelberg: Springer: 3–3. doi:10.1007/978-3-642-19583-9_2. ISBN 978-3-642-19583-9.
↑ "SMT-COMP 2020". SMT-COMP (به انگلیسی). Retrieved 2020-10-19.
↑ Hassan, Mostafa, et al. "Maxsmt-based type inference for python 3." International Conference on Computer Aided Verification. Springer, Cham, 2018.
↑ 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 (به انگلیسی). Cham: Springer International Publishing: 521–540. doi:10.1007/978-3-319-24174-6_27. ISBN 978-3-319-24174-6.

منابع

مشارکت‌کنندگان ویکی‌پدیا. «Satisfiability modulo theories». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۱۱ مهٔ ۲۰۲۱.

[1] Barbosa, Haniel, et al. "Extending SMT solvers to higher-order logic." International Conference on Automated Deduction. Springer, Cham, 2019.

[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)", Journal of the ACM (PDF), vol. 53, pp. 937–977

[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", JSAT Special Issue on SAT/CP Integration (PDF), vol. 1, pp. 209–236

[5] Barrett, Clark; de Moura, Leonardo; Stump, Aaron (2005). Etessami, Kousha; Rajamani, Sriram K. (eds.). "SMT-COMP: Satisfiability Modulo Theories Competition". Computer Aided Verification. Lecture Notes in Computer Science (به انگلیسی). Berlin, Heidelberg: Springer: 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). Barner, Sharon; Harris, Ian; Kroening, Daniel; Raz, Orna (eds.). "The SMT-LIB Initiative and the Rise of SMT". Hardware and Software: Verification and Testing. Lecture Notes in Computer Science (به انگلیسی). Berlin, Heidelberg: Springer: 3–3. doi:10.1007/978-3-642-19583-9_2. ISBN 978-3-642-19583-9.

[7] "SMT-COMP 2020". SMT-COMP (به انگلیسی). Retrieved 2020-10-19.

[8] Hassan, Mostafa, et al. "Maxsmt-based type inference for python 3." International Conference on Computer Aided Verification. Springer, Cham, 2018.

[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 (به انگلیسی). Cham: Springer International Publishing: 521–540. doi:10.1007/978-3-319-24174-6_27. ISBN 978-3-319-24174-6.

[۱]

[۲]

[۳]

[۴]

[۵]

[۶]

[۷]

[۸]

[۹]

[۱۰]

@@ خط ۱۱: / خط ۱۱: @@
 برای مقایسه، برنامه‌نویسی مجموعه جواب نیز براساس گزاره‌ها است (به صورت دقیق‌تر، یک جمله اتمی است که از فرمول‌های اتمی ساخته شده است). برخلاف SMT، برنامه‌های مجموعه جواب، سور ندارند، و نمی توانند محدودیت هایی مثل حساب خطی یا منطق تفاوت را به سادگی بیان کنند- ASP به عنوان بهترین راه‌حل برای مسائل دودویی هستند که به نظریه آزاد توابع تفسیرنشده کاهش یافته اند. پیاده سازی اعداد صحیح 32 بیتی به عنوان آرایه‌بیتی در ASP از مسائل مشابهی رنج می برند که حل کننده های اولیه SMT ها با آن مواجه بودند: برابری های «بدیهی» مثل ''x''+''y''=''y''+''x'' به سختی قابل استنتاج هستند.
-برنامه‌نویسی منطقی محدودیت از محدودیت های حسابی خطی پشتیبانی می کنند، اما آن‌ها در چارچوب نظری کاملا متفاوتی قرار دارند. حل‌کننده های SMT برای حل فرمول‌هایی در منطق مرتبه بالاتر گسترش یافته اند.
+برنامه‌نویسی منطقی محدودیت از محدودیت های حسابی خطی پشتیبانی می کنند، اما آن‌ها در چارچوب نظری کاملا متفاوتی قرار دارند. حل‌کننده های SMT برای حل فرمول‌هایی در منطق مرتبه بالاتر گسترش یافته اند.<ref>Barbosa, Haniel, et al. "[https://hal.archives-ouvertes.fr/hal-02300986/document Extending SMT solvers to higher-order logic]." International Conference on Automated Deduction. Springer, Cham, 2019.</ref>
 == دیدگاه‌های حل‌کننده ==
 تلاش‌های اولیه برای حل نمونه‌های مسئله SMT شامل ترجمه آن‌ها به نمونه مسائل SAT دودویی بود (مثلا یک متغیر صحیح 32 بیتی توسط 32 عدد متغیر تک بیتی با وزن‌های مناسب و عملیات سطح کلمه مثل «جمع» با عملیات منطقی سطح پایینی روی بیت ها جایگزین می شدند) سپس این فرمول به حل کننده SAT دودویی تحویل می شد. به این دیدگاه، دیدگاه حریصانه هم می گویند، و دارای مزیت‌هایی هم هست: با پیش‌پردازش یم فرمول SMT به یک فرمول SAT دودویی معادل، حل‌کننده های SAT دودویی موجود را می توان به صورتی که هست استفاده کرد، مزیت هایش از نظر کارایی و ظرفیت در طی زمان بیشتر می شود. از جهت دیگر، فقدان وجود معناشناسی سطح بالا برای نظریه‌های بنیادین، یعنی حل‌کننده دودویی SAT باید خیلی بیشتر از آنچه برای برای کشف واقعیت‌های «بدیهی» لازم است، کار کند (مثلا <math>x + y = y + x</math> برای جمع اعداد صحیح). این مشاهده منجر به ایجاد تعدادی از حل کننده های SMT شد که به شدت استنتاج دودویی یک جستجوی با سبک DPLL را به حل‌کننده‌های خاص نظریه (T-solvers) که به عطف‌های(ANDs) از گزاره‌ها از یک نظریه معین رسیدگی می کند، یکپارچه‌سازی می‌کرد. به این دیدگاه، دیدگاه کندرو هم گفته می شود.
-DPLL(T) دوبل (دوتایی) که این معماری مسئولیت استنتاج دودویی به حل کننده SAT مبتنی بر DPLL داده می شود، که به نوبه خود با یک حل کننده برای نظریه T از طریق یک واسط خوش‌تعریف تعامل دارد. حل کننده نظریه فقط باید در مورد بررسی امکان عطف‌دهی به گزاره‌های نظریه ارسال شده به آن، از حل‌کننده SAT و در هنگام کاوش فضای جستجوی دودویی فرمول نگران باشد. برای آنکه این یکپارچه‌سازی به خوبی کار کند، حل کننده نظریه باید بتواند در تحلیل انتشار و تضاد مشارکت کند، یعنی باید بتواند واقعیت های جدیدی را از واقعیت‌های پیش از این بناشده، استنتاج کند، همچنین از توضیحات مختصری از غیرممکن بودن در موقع بروز تعارض‌های نظری پشتیبانی کند. به زبان دیگر، حل‌کننده نظریه باید افزایشی و پس‌گردی باشد.
+DPLL(T) دوبل (دوتایی)<ref>{{Citation|first1=R.|last1=Nieuwenhuis|first2=A.|last2=Oliveras|first3=C.|last3=Tinelli|url=http://homepage.cs.uiowa.edu/~tinelli/papers/NieOT-JACM-06.pdf|contribution=Solving SAT and SAT Modulo Theories: From an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)|title=Journal of the ACM|volume=53|pages=937&ndash;977|year=2006|issue=6}}</ref> که این معماری مسئولیت استنتاج دودویی به حل کننده SAT مبتنی بر DPLL داده می شود، که به نوبه خود با یک حل کننده برای نظریه T از طریق یک واسط خوش‌تعریف تعامل دارد. حل کننده نظریه فقط باید در مورد بررسی امکان عطف‌دهی به گزاره‌های نظریه ارسال شده به آن، از حل‌کننده SAT و در هنگام کاوش فضای جستجوی دودویی فرمول نگران باشد. برای آنکه این یکپارچه‌سازی به خوبی کار کند، حل کننده نظریه باید بتواند در تحلیل انتشار و تضاد مشارکت کند، یعنی باید بتواند واقعیت های جدیدی را از واقعیت‌های پیش از این بناشده، استنتاج کند، همچنین از توضیحات مختصری از غیرممکن بودن در موقع بروز تعارض‌های نظری پشتیبانی کند. به زبان دیگر، حل‌کننده نظریه باید افزایشی و پس‌گردی باشد.
 == مسئله SMT برای نظریات تصمیم‌ناپذیر ==
@@ خط ۳۳: / خط ۳۳: @@
 صدق‌پذیر هست یا نه. سپس این مسائل به صورت کلی غیرقابل تصمیم می شوند. (نظریه زمینه‌های بسته حقیقی، و از این رو نظریه مرتبه اول از اعداد حقیقی، توسط حذف سور قابل تصمیم هستند. این موضوع را مدیون آلفرد تارسکی هستیم.) نظریه مرتبه اول اعداد طبیعی با جمع (اما بدون ضرب) حساب پرسبورگر نامیده می شود، که آن هم تصمیم‌پذیر است. به دلیل آنکه ضرب کردن با ثابت ها را می توان به صورت جمع‌های تودرتو پیاده‌سازی کرد، حساب در بسیاری از برنامه‌های رایانه‌ای قابل بیان به کمک حساب پرسبورگر است، که این موضوع منجر به فرمول‌های قابل تصمیم‌گیری می شود.
-مثال‌هایی از حل کننده های SMT که می خواهند ترکیبات دودویی اتم نظریه از نظریات حسابی تصمیم‌ناپذیر روی اعداد حقیقی رسیدگی کنند، ABsolver نام دارند، که از یک معماری کلاسیک DPLL(T) با یک بسته بهینه‌سازی غیرخطی به عنوان حل‌کننده نظریه فرعی (به صورت لازم غیرکامل) استفاده می کنند، و iSAT که روی یک اتحاد حل‌کننده DPLL SAT و انتشار محدودیت بازه‌ای ساخته شده اند، که الگوریتم iSAT نامیده می شود.
+مثال‌هایی از حل کننده های SMT که می خواهند ترکیبات دودویی اتم نظریه از نظریات حسابی تصمیم‌ناپذیر روی اعداد حقیقی رسیدگی کنند، ABsolver<ref>{{Citation|first1=A.|last1=Bauer|author-link=|first2=M.|last2=Pister|first3=M.|last3=Tautschnig|contribution=Tool-support for the analysis of hybrid systems and models|title=Proceedings of the 2007 Conference on Design, Automation and Test in Europe (DATE'07)|publisher=IEEE Computer Society|year=2007|doi=10.1109/DATE.2007.364411|page=1|isbn=978-3-9810801-2-4|citeseerx=10.1.1.323.6807|s2cid=9159847}}</ref> نام دارند، که از یک معماری کلاسیک DPLL(T) با یک بسته بهینه‌سازی غیرخطی به عنوان حل‌کننده نظریه فرعی (به صورت لازم غیرکامل) استفاده می کنند، و iSAT که روی یک اتحاد حل‌کننده DPLL SAT و انتشار محدودیت بازه‌ای ساخته شده اند، که الگوریتم iSAT نامیده می شود.<ref>{{Citation|first1=M.|last1=Fränzle|first2=C.|last2=Herde|first3=S.|last3=Ratschan|first4=T.|last4=Schubert|first5=T.|last5=Teige|url=http://jsat.ewi.tudelft.nl/content/volume1/JSAT1_11_Fraenzle.pdf|contribution=Efficient Solving of Large Non-linear Arithmetic Constraint Systems with Complex Boolean Structure|title=JSAT Special Issue on SAT/CP Integration|volume=1|pages=209&ndash;236|year=2007}}</ref>
 == حل‌کننده‌ها ==
@@ خط ۴۳: / خط ۴۳: @@
 تلاش های زیادی برای توصیف یک واسط استاندارد شده برای حل کننده SMT (و اثبات‌گر قضیه خودکار، که یک اصطلاح هم‌معنی است) وجود دارد. برجسته‌ترین آن‌ها استاندارد SMT-LIB است که یک زبان بر اساس عبارات S تهیه دیده است. دیگر قالب‌های استاندارد شده که معمولا پشتیبانی می شوند شامل قالب DIMACS است که توسط خیلی از حل‌کننده‌های SAT بولی پشتیبانی می شود، و قالب CVC که توسط اثبات‌گر قضیه خودکار CVC استفاده می شود.
-قالب SMT-LIB همراه با تعدادی از مح‌زنی (benchmark) استاندارد آمده است، و این موضوع یک مسابقه سالانه بین حل‌کننده های SMT را امکان‌پذیر نموده است که به آن SMT-COMP گفته می شود. در ابتدا، مسابقه در همایش درستی‌سنجی به کمک رایانه (CAV) قرار داشت، اما از سال 2020 مسابقه به عنوان بخشی از کارگاه SMT قرار گرفت، که به همایش ترکیبی بین‌المللی روی استنتاج خودکار (IJCAR) وابسته بود.
+قالب SMT-LIB همراه با تعدادی از محک‌زنی (benchmark) استاندارد آمده است، و این موضوع یک مسابقه سالانه بین حل‌کننده های SMT را امکان‌پذیر نموده است که به آن SMT-COMP گفته می شود. در ابتدا، مسابقه در همایش درستی‌سنجی به کمک رایانه (CAV)<ref>{{Cite journal|last=Barrett|first=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.|title=SMT-COMP: Satisfiability Modulo Theories Competition|url=https://link.springer.com/chapter/10.1007%2F11513988_4|journal=Computer Aided Verification|series=Lecture Notes in Computer Science|language=en|location=Berlin, Heidelberg|publisher=Springer|pages=20–23|doi=10.1007/11513988_4|isbn=978-3-540-31686-2}}</ref><ref>{{Cite journal|last=Barrett|first=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|title=The SMT-LIB Initiative and the Rise of SMT|url=https://link.springer.com/chapter/10.1007%2F978-3-642-19583-9_2|journal=Hardware and Software: Verification and Testing|series=Lecture Notes in Computer Science|language=en|location=Berlin, Heidelberg|publisher=Springer|pages=3–3|doi=10.1007/978-3-642-19583-9_2|isbn=978-3-642-19583-9|doi-access=free}}</ref> قرار داشت، اما از سال 2020 مسابقه به عنوان بخشی از کارگاه SMT قرار گرفت، که به همایش ترکیبی بین‌المللی روی استنتاج خودکار (IJCAR) وابسته بود.<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 هم برای درستی‌سنجی، اثبات درستی برنامه‌ها، آزمون نرم‌افزار براساس اجرای نمادین، و نیز برای ترکیب، تولید قطعه های برنامه با جستجو روی فضای برنامه‌های ممکن مفید است. در خارج از حیطه درستی‌سنجی نرم‌افزار، از حل‌کننده SMT برای استنتاج نوع، و نیز برای مدل‌سازی سناریوهای نظری، شامل مدل‌سازی اعتقادات کنشگر در کنترل نیروی هسته‌ای استفاده شده است.
+حل‌کننده های SMT هم برای درستی‌سنجی، اثبات درستی برنامه‌ها، آزمون نرم‌افزار براساس اجرای نمادین، و نیز برای ترکیب، تولید قطعه های برنامه با جستجو روی فضای برنامه‌های ممکن مفید است. در خارج از حیطه درستی‌سنجی نرم‌افزار، از حل‌کننده SMT برای استنتاج نوع،<ref>Hassan, Mostafa, et al. [https://link.springer.com/chapter/10.1007/978-3-319-96142-2_2 "Maxsmt-based type inference for python 3."] International Conference on Computer Aided Verification. Springer, Cham, 2018.</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|last=Beaumont|first=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|url=https://link.springer.com/chapter/10.1007%2F978-3-319-24174-6_27|journal=Computer Security -- ESORICS 2015|series=Lecture Notes in Computer Science|language=en|location=Cham|publisher=Springer International Publishing|pages=521–540|doi=10.1007/978-3-319-24174-6_27|isbn=978-3-319-24174-6|doi-access=free}}</ref>
 === درستی‌سنجی ===