به پرسشهایی که به دنبالِ پاسخدادن به «آیا میتوان ارزشدهیای به متغیرهای بولی یافت که گزارهای دارای ارزش درست شود» SAT که کوتاهشدهٔ Satisfiability است میگویند. برای نمونه پرسشِ زیر.
نمونه: آیا انتخابی برای دو متغیرِ بولیِ $A$ و $B$ وجود دارد که $(A\vee B)\wedge(\neg B)$ درست باشد؟
که البته پاسخ بلی است که اصطلاحا میگویند عبارتِ $(A\vee B)\wedge(\neg B)$ «شدنی» SAT است. و یک ارزشدهی که آن را شدنی میکند برابر با $A=\text{درست}$ و $B=\text{نادرست}$ است. اگر عبارت به ازای تمام ارزشدهیها نادرست باشد، آنگاه میگوئیم «ناشدنی» UNSAT است.
اکنون اگر به غیر از متغیرهای بولی و عملگرهای منطقی، اجازهداشته باشیم از تئوری دیگری استفاده کنیم، به جای SAT به پرسشمان SMT که کوتاه شدهٔ Satisfiability Modulo Theory است میگوئيم. برای نمونه اگر متغیرهای حقیقی مقدار و نامساویهای چندجملهای داشته باشیم. در زیر یک نمونه میبینیم.
نمونه: آیا عدد حقیقیای مانندِ $a$ وجود دارد که عبارتِ $x^2>a$ برای هر مقدارِ حقیقی به جای $x$ برقرار باشد؟
این یک پرسشِ SMT است که SAT است یعنی شدنی است و یک ارزشدهیِ مناسب برایش $a=-1$ است.
گاهی تعداد متغیرها یا اندازهٔ عبارت بزرگ است و نمیتوان پرسش را دستی حل کرد. در این حالت مجبور به استفاده از نرمافزار هستیم. یکی از ابزارهای رایگان که این گونه پرسشها را حل میکند Z3 (زی سه) نام دارد. این ابزار بوسیلهٔ چند فرد در شرکت مایکروسافت توسعه یافته است. میتوانید آن را در پایتون به کار ببرید، اما برای صداکردنِ آن در پایتون به روشی که بستههای دیگر را به کار میبردید باید ابتدا آن را نصب و به پایتون معرفی کنید که متأسفانه با روشِ متداولِ pip install انجام نمیشود. اگر میخواهید بدانید که چگونه آن را نصب کنید میتوانید ویدئوی زیر را نگاه کنید که در انتهایش چند نمونه از به کار بردن این ابزار برای حل پرسشهای به شکل بالا هم آورده شدهاست.
اگر یک راهنمای تقریبا جامع برای شیوهٔ استفاده از این ابزار و همین طور اینکه چه دسته از پرسشها را میتواند حل کند میخواهید، راهنمای آمده در پیوند زیر که بوسیلهٔ چند نفر از توسعهدهندههایش نوشته شده است و در دانشگاه استنفورد آمریکا تدریس شدهاست را میتوانید نگاه کنید.
https://theory.stanford.edu/~nikolaj/programmingz3.html
