صدق‌پذیری در پیمانه نظریات

یک مسئله صدق‌پذیری در پیمانه نظریات  با کوته‌نوشت SMT در علوم رایانه و منطق ریاضیاتی، یک «مسئله تصمیم» برای فرمول‌های منطقی در ارتباط با ترکیبی از نظریات پیش‌زمینه‌ای که به صورت منطق مرتبه اول کلاسیک دارای تساوی بیان شده‌اند، است. مثال‌هایی از این نظریات که معمولاً در علوم رایانه استفاده می‌شوند از این قرار است: نظریه اعداد حقیقی، نظریه اعداد صحیح، و نظریات ساختمان داده‌های متنوع مثل لیست، آرایه، بردار بیتی، و غیره. مسئله SMT را می‌توان نوعی مسئله ارضای محدودیت در نظر گرفت، و از این رو یک دیدگاه صوری‌شده معین به برنامه‌نویسی محدودیت است.

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

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

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

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

برنامه‌نویسی منطقی محدودیت از محدودیت‌های حسابی خطی پشتیبانی می‌کنند، اما آن‌ها در چارچوب نظری کاملاً متفاوتی قرار دارند. حل‌کننده‌های SMT برای حل فرمول‌هایی در منطق مرتبه بالاتر گسترش یافته‌اند.Barbosa, Haniel, et al. "Extending SMT solvers to higher-order logic." International Conference on Automated Deduction. Springer, Cham, 2019.

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

DPLL(T) دوبل (دوتایی) که این معماری یک «مسئولیت استنتاج بولی» به «حل‌کننده SAT مبتنی بر DPLL» می داد، که به نوبه خود با یک حل‌کننده برای نظریه T از طریق یک واسط خوش‌تعریف تعامل دارد. حل‌کننده نظریه فقط باید در مورد بررسی امکان عطف‌دهی به گزاره‌های نظریه ارسال‌شده به آن، از حل‌کننده SAT و در هنگام کاوش فضای جستجوی دودویی فرمول نگران باشد. برای آنکه این یکپارچه‌سازی به خوبی کار کند، حل‌کننده نظریه باید بتواند در تحلیل انتشار و تضاد مشارکت کند، یعنی باید بتواند واقعیت‌های جدیدی را از واقعیت‌های پیش از این بناشده، استنتاج کند، همچنین از «توضیحات مختصری از غیرممکن بودن» در موقع بروز تعارض‌های نظری پشتیبانی کند. به زبان دیگر، حل‌کننده نظریه باید افزایشی و پس‌گردی باشد.

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



که در آن:



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

مثال‌هایی از حل کننده‌های SMT که می‌خواهند ترکیبات دودویی «اتم نظریه» از نظریات حسابی تصمیم‌ناپذیر روی اعداد حقیقی رسیدگی کنند، ABsolver نام دارند، که از یک معماری کلاسیک DPLL(T) با یک بسته بهینه‌سازی غیرخطی به عنوان حل‌کننده نظریه فرعی (به صورت لازم غیرکامل) استفاده می‌کنند، و iSAT  که روی یک اتحاد حل‌کننده DPLL SAT و انتشار محدودیت بازه‌ای ساخته شده‌اند، که الگوریتم iSAT نامیده می‌شود.

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

این پروژه‌ها نه فقط از نظر ویژگی و کارایی با هم فرق دارند، بلکه از نظر زیست‌پذیری انجمن اطراف شان، علاقه پیشرونده به پروژه و توانمندی مشارکت مستندات، تعمیرها، تست‌ها و ارتقا با هم تفاوت دارند.
 بن‌سازه ویژگی‌ها یادداشت‌ها Name OS License SMT-LIB CVC DIMACS Built-in theories API SMT-COMP  ABsolver Linux CPL    linear arithmetic, non-linear arithmetic C++ no DPLL-based Alt-Ergo Linux,  Mac OS , Windows CeCILL-C (roughly equivalent to LGPL)    empty theory, linear integer and rational arithmetic, non-linear arithmetic, polymorphic arrays, enumerated datatypes, AC symbols, bitvectors, record datatypes, quantifiers OCaml ۲۰۰۸ 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  empty theory, difference logic C++ ۲۰۰۹ DPLL-based, congruence closure Beaver Linux, Windows BSD    bitvectors OCaml ۲۰۰۹ SAT-solver based Boolector Linux MIT    bitvectors, arrays C ۲۰۰۹ SAT-solver based CVC3 Linux BSD   empty theory, linear arithmetic, arrays, tuples, types, records, bitvectors, quantifiers C/C++ ۲۰۱۰ proof output to HOL CVC4 Linux,  Mac OS , Windows, FreeBSD BSD   rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bitvectors, strings, and equality over uninterpreted function symbols C++ ۲۰۱۰ version 1.5 released July 2017 Decision Procedure Toolkit (DPT) Linux Apache  OCaml no DPLL-based iSAT Linux Proprietary  non-linear arithmetic no DPLL-based MathSAT Linux,  Mac OS , Windows Proprietary   empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays C/C++, Python, Java ۲۰۱۰ DPLL-based MiniSmt Linux LGPL  non-linear arithmetic ۲۰۱۰ SAT-solver based, Yices-based Norn SMT solver for string constraints OpenCog Linux AGPL    probabilistic logic, arithmetic. relational models C++, Scheme, Python no subgraph isomorphism OpenSMT Linux,  Mac OS , Windows GPLv3   empty theory, differences, linear arithmetic, bitvectors C++ ۲۰۱۱ lazy SMT SolverraSATLinuxGPLv3v2.0real and integer nonlinear arithmetic۲۰۱۴، ۲۰۱۵extension of the Interval Constraint Propagation with Testing and the Intermediate Value Theorem SatEEn ? Proprietary  linear arithmetic, difference logic none ۲۰۰۹ SMTInterpol Linux,  Mac OS , Windows  LGPLv3   uninterpreted functions, linear real arithmetic, and linear integer arithmetic Java ۲۰۱۲ Focuses on generating high quality, compact interpolants. SMCHR Linux,  Mac OS , Windows GPLv3    linear arithmetic, nonlinear arithmetic, heaps C no Can implement new theories using Constraint Handling Rules. SMT-RAT Linux,  Mac OS  MIT    linear arithmetic, nonlinear arithmetic C++ ۲۰۱۵ Toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations. SONOLAR Linux, Windows Proprietary  bitvectors C ۲۰۱۰ SAT-solver based Spear Linux,  Mac OS , Windows Proprietary  bitvectors ۲۰۰۸ STP Linux, OpenBSD, Windows,  Mac OS  MIT    bitvectors, arrays C, C++, Python, OCaml, Java ۲۰۱۱ SAT-solver based SWORD Linux Proprietary  bitvectors ۲۰۰۹ UCLID Linux BSD    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  empty theory, rational and integer linear arithmetics, quantifiers, and equality over uninterpreted function symbols C/C++ ۲۰۱۰ SAT-solver based  Linux,  Mac OS , Windows, FreeBSD GPLv3    rational and integer linear arithmetic, bitvectors, arrays, and equality over uninterpreted function symbols C ۲۰۱۴ Source code is available online Z3 Theorem Prover Linux,  Mac OS , Windows, FreeBSD MIT   empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays, datatypes, quantifiers, strings C/C++, .NET, OCaml, Python, Java, Haskell ۲۰۱۱ Source code is available online

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

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

 کاربردها 
حل‌کننده‌های SMT هم برای صحت، اثبات درستی برنامه‌ها، آزمون نرم‌افزار براساس اجرای نمادین، و نیز برای ترکیب، تولید قطعه‌های برنامه با جستجو روی فضای برنامه‌های ممکن مفید است. در خارج از حیطه درستی‌سنجی نرم‌افزار، از حل‌کننده SMT برای استنتاج نوع،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. و نیز برای مدل‌سازی سناریوهای نظری، که شامل مدل‌سازی اعتقادات کنشگر در کنترل نیروی هسته‌ای است، استفاده شده‌است.

 درستی‌سنجی 
درستی‌یابی برنامه‌های رایانه‌ای به کمک رایانه معمولاً از حل کننده 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 به جای اثبات‌گر اصلی اش استفاده کند (این کار موجب افزایش موفقیت از ۸۴٪ به ۹۸٪ در محک‌زنی‌های پروژه ANR Bware می‌شود)؛
 Rodin، یک چارچوب روش-B است که توسط Systertel توسعه یافته‌است و می‌تواند از Alt-Ergo به عنوان یک back-end استفاده کند.
 Cubicle یک بررسی‌کننده مدل متن‌باز است که از آن برای درستی‌سنجی ویژگی‌های امنیتی برای سامانه‌های تبدیل مبتنی بر آرایه استفاده می‌شود.
 EasyCrypt، یک جعبه ابزار برای استنتاج دربارهٔ ویژگی‌های رابطه‌ای در محاسبات احتمالی است، که کد خصومتی دارد.

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

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

 پانویس 

 منابع 

رده:برنامه‌نویسی ارضای محدودیت
رده:حل‌کننده‌های مسئله SMT
رده:خودکارسازی طراحی الکترونیکی
رده:روش‌های صوری
رده:مسائل صدق‌پذیری
رده:مسئله‌های ان‌پی کامل
رده:منطق در علوم کامپیوتر