مسئله صدق‌پذیری دودویی

در علوم رایانه، صدق‌پذیری (در زبان انگلیسی به طور خلاصه SAT) مسئله‌ایست که تعیین می‌کند آیا متغیرهای یک فرمول دودویی را می‎توان به صورتی مشخص کرد که فرمول همواره درست باشد یا نه. همچنین مشخص می‎‌کند که اگر نتوان به هیچ طریقی آن متغیرها را معین کرد، پس قطعا این فرمول همواره نادرست خواهد بود و می‌گوییم که این فرمول صدق‌ناپذیر است، در غیر این صورت صدق‌پذیر خواهد بود. به طور مثال، فرمول a AND b صدق‌پذیر است، چون اگر a و b هر دو همواره درست باشند، این فرمول هم همواره درست خواهد بود. برای تاکید بر دودویی بودن ماهیت این مسئله، معمولا به آن مسئله‌ی دودویی گفته می‌شود.

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

تعاریف اساسی، واژگان و کاربردها

در نظریه پیچیدگی محاسباتی مسئله‌ی صدق‌پذیری یک مسئله‌ی تصمیم است که نمونه‌ی آن یک عبارت بولی می‌باشد که فقط با AND، OR، NOT، متغیرها و پرانتز نوشته شده است. سوال این است که: آیا می‌توان به متغیرها مقادیر "درست" و "نادرست" داد تا عبارت موردنظر همواره درست باشد؟ یک فرمول از منطق گزاره‌ای صدق‌پذیر است اگر به متغیرهای آن بتوان مقادیر منطقی داد تا فرمول همواره درست باشد. مسئله‌ی صدق‌پذیری دودویی یک ان‌پی کامل است. مسئله‌ی صدق‌پذیری گزاره‌ای (PSAT)، که مشخص می‌کند آیا یک فرمول گزاره‌ای صدق‌پذیر هست یا نه، مهمترین مسئله در حوزه‌های مختلف علوم رایانه است؛ نظیر علوم نظری رایانه، الگوریتم‌ها، هوش مصنوعی، طراحی پردازنده، اتوماسیون طراحی الکترونیکی و تایید.

یک متغیر یا خود آن متغیر و یا نقیضش است. به طور مثال x_۱ یک متغیر مثبت و (not(x_۲ یک متغیر منفی است.

یک عبارت فصلی منطقی از متغیرهاست. به طور مثال (x_۱ V not(x_۲ یک عبارت است.

در بعضی حالت‌های مسئله صدق‌پذیری دودویی، نیاز است که فرمول عطف منطقی چند عبارت باشد. حالتی که صدق‌پذیری یک فرمول به شکل عطف معمولی را بررسی می‌کنیم که هر عبارت حداکثر دارای سه متغیر باشد، ان‌پی کامل است؛ این مسئله "۳SAT" یا "۳CNFSAT" یا "۳-صدق‌پذیری" نامیده می‌شود. حالتی که فرمول موردبررسی دارای عبارت‌هایی با حداکثر دو متغیر باشد، ان‌ال کامل است؛ این مسئله "۲SAT" نامیده می‌شود. حالتی که فرمول موردبررسی دارای عبارت‌های هورن (که حداکثر یک متغیر مثبت دارند.) باشد، پی کامل است؛ این مسئله صدق‌پذیری هورن نامیده می‌شود.

قضیه کوک لوین عنوان می‌کند که مسئله دودویی صدق‌پذیری یک ان‌پی کامل است، در واقع این اولین مسئله‌ایست که اثبات شده ان‌پی کامل است.

پیچیدگی و نسخه‌های محدود

ان‌پی کامل

همانطور که استفن کوک در سال ۱۹۷۱ اثبات کرد، مسئله‌ی SAT اولین مسئله‌ی ان‌پی کامل شناخته شد. (اثبات را در قضیه کوک لوین ببینید.) تا آن زمان مفهومی به نام ان‌پی کامل وجود نداشت. این مسئله ان‌پی کامل باقی می‎ماند هرچند که همه‌ی عبارات به صورت عطفی معمولی با سه متغیر در هر عبارت (۳-CNF) باشند؛ یعنی عبارت به شکل زیر است:

(x₁₁ OR x₁₂ OR x₁₃) AND

(x₂₁ OR x₂₂ OR x₂₃) AND

(x₃₁ OR x₃₂ OR x₃₃) AND ...

در اینجا هر x یک "متغیر" است و هر متغیر می‌تواند چندبار در عبارت تکرار شوند.

یک ویژگی مهم اختصار کوک آن است که تعداد جواب‌های درست را نگه می‌دارد. به طور مثال اگر یک گراف 17 رنگ‌آمیزی سه‌گانه معتبر داشته باشد، قاعده‌ی SAT دارای 17 واگذاری ارضاپذیر است.

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

مسئله‌ی SAT آسانتر است اگر فرمول‌ها به صورت فصلی معمولی باشند، یعنی بین عبارات OR و در هر عبارت بین متغیرها AND قرار گرفته باشد. این فرمول‌ها صدق‌پذیر هستند اگر و تنها اگر حداقل یکی از عبارات آن صدق‌پذیر باشند، و یک عبارت صدق‌پذیر است اگر و تنها اگر به ازای هر متغیر x هم خودش و هم NOT آن را دربرنداشته باشد. این موضوع می‌تواند در زمان چندجمله‌ای بررسی شود.

2-صدق‌پذیری

همچنین مسئله‌ی SAT آسانتر است اگر تعداد متغیرهای یک عبارت به 2 محدود شده باشد، که در این حالت مسئله 2SAT نامیده می‌شود. این مسئله نیز می‌تواند در زمان چندجمله‌ای حل شود و در واقع برای رده‌ی ان‎ال کامل است. به طور مشابه اگر تعداد متغیرهای هر عبارت را به 2 محدود کرده و اعمال AND را به XOR تغییر دهیم، نتیجه یک 2-صدق‌پذیری XOR است که یک مسئله‌ی کامل برای SL = L می‌باشد.

یکی از مهمترین محدودیت‌های SAT، مسئله‌ی HORNSAT می‌باشد که فرمول، یک عطف از چند عبارت هورن باشد. این مسئله با الگوریتم ارضاپذیری هورن با زمان چندجمله‌ای قابل حل است، و در اصل پی-کامل می‌باشد. می‌تواند به صورت نسخه‌ای از رده‌ی پی برای مسئله‌ی صدق‌پذیری دودویی دیده شود.

در صورتی که رده‌های پیچیدگی پی و ان‎پی یکسان نباشند، برخلاف SAT هیچ‌کدام از این محدودیت‌ها ان‌پی کامل نیستند. این فرضیه که پی و ان‌پی یکسان نیستند هنوز اثبات نشده‌است.

3-صدق‌پذیری

3-صدق‌پذیری یک حالت خاص از k-SAT یا به طور ساده‌شده SAT است که هر عبارت دقیقا k = 3 متغیر را شامل می‌شود. این یکی از 21 مسئله ان‌پی-کامل کارپ است.

در اینجا یک مثال می‌زنیم: (¬ نشان‌دهنده‌ی نقیض است.)

$E = (x_1 \vee \neg x_2 \vee \neg x_3) \wedge (x_1 \vee x_2 \vee x_4)$

E دارای دو عبارت (که با پرانتز مشخص شده‌اند)، چهار متغیر (x₁, x₂, x₃, x₄) و k = 3 (سه متغیر در هر عبارت) می‌باشد.

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

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

بر اساس نظر شونینگ (1990) یک الگوریتم ساده‌ی تصادفی وجود دارد که در زمان $(4/3)^n$ اجرا می‌شود (n تعداد عبارات). این الگوریتم به احتمال قوی موفق می‌شود تا درباره‌ی 3-SAT درست تصمیم بگیرد. فرضیه‌ی نمایی زمان آن است که هیچ الگوریتمی نمی‌تواند 3-SAT را در زمان $\exp(o(n))$ حل کند.

صدق‌پذیری هورن

یک عبارت هورن است اگر حداکثر یک متغیر مثبت داشته باشد. این‌گونه عبار‌ت‌ها موردتوجه هستند چون می‌توانند استلزام یک متغیر از مجموعه‌ای از متغیرها را بیان کنند. در واقع یک عبارت مانند $\neg x_1 \vee \cdots \vee \neg x_n \vee y$ می‌تواند به شکل $x_1 \wedge \cdots \wedge x_n \rightarrow y$ بازنویسی شود، یعنی اگر $x_1,\ldots,x_n$ همه "درست" باشند، y هم باید "درست" باشد.

مسئله‌ی تصمیم‌گیری در مورد صدق‌پذیری عبارات هورن در پی (P) است. این مسئله نیز می‌تواند با یک مرحله از انتشار واحد حل شود که مدل کمینه‌ی واحد از مجموعه‌ای از عبارات هورن ایجاد می‌کند.

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

صدق‌پذیری XOR

یک حالت خاص دیگر مسائلی هستند که در آنها هر عبارت فقط اعمال XOR را شامل می‌شود. چون عمل XOR معادل جمع در زمینه‌ی گالویس از اندازه‌ی 2 است، عبارات می‌توانند مانند یک دستگاه معادلات خطی دیده شوند و از روش‌های متناظر مانند حذف گاوسی می‌توان برای یافتن راه‌حل آنها استفاده کرد.

قضیه‌ی دوگانگی شافر

محدودیت‌های بالا (CNF، 2CNF، 3CNF، هورن) فرمول موردبررسی را به عطفی بودن زیرفرمول محدود می‌کنند؛ هر محدودیت یک شکل خاص برای همه‌ی زیرفرمول‌ها مشخص می‌کند: به طور مثال، فقط عبارات دودویی می‌توانند یک زیرفرمول در 2CNF باشند.

قضیه‌ی دوگانگی شافر عنوان می‌کند که برای هر محدودیتی بر اعمال بولی که می‌توانند این زیرفرمول‌ها را شکل دهند، مسئله‌ی صدق‌پذیری متناظر یک پی یا ان‌پی کامل است. عضویت در پی (P) برای صدق‌پذیری 2CNF و فرمول هورن، حالت‌های خاصی از این قضیه هستند.

رفتار در زمان اجرا

همانطور که در بالا به طور خلاصه بیان شد، هرچند که مسئله، ان‌پی کامل است، مثال‌های عملی زیادی می‌توانند خیلی زود حل شوند. اکثر مسائل عملی در حقیقت "آسان" هستند، پس حل‌کننده‌ی SAT به آسانی می‌تواند یک راه‌حل بیابد یا اثبات کند که وجود ندارد؛ با وجود آنکه آن مورد هزاران متغیر و ده‌ها هزار محدودیت دارد. بقیه‌ی مسائل کوچک زمان‌های اجرایی را ارایه می‌دهند که به صورت نمایی باشند و به مرور غیرعملی شده‌اند. متاسفانه هیچ راه قابل اطمینانی وجود ندارد که سختی مسئله را بدون امتحان آن بیان کند. پس تقریبا همه‌ی حل‌کننده‌های SAT شامل زمان‌های اضافه می‌شوند، پس با آنکه هیچ راه‌حلی نیافته‌اند اما به پایان خواهند رسید. در نهایت حل‌کننده‌های SAT مختلفی موارد مختلف آسان و یا سخت را پیدا خواهند کرد و بعضی از آنها در اثبات صدق‌ناپذیری و دیگران در یافتن راه‌حل برترند. همه‌ی آن رفتارها در مسابقه‌های حل SAT دیده می‌‎شوند.

قابلیت کاهش دادن خود

از یک الگوریتم که به درستی می‌گوید یک مثال از SAT قابل‌حل است یا نه، می‌توان برای یافتن واگذاری صدق‌پذیر استفاده کرد. در ابتدا سوال از فرمول $\phi$ پرسیده می‌شود. اگر جواب "خیر" باشد، فرمول صدق‌ناپذیر است. در غیر این صورت سوال از $\phi_{x_1 = 0}$ پرسیده می‌شود، یعنی اولین متغیر 0 در نظر گرفته می‌شود. اگر جواب "خیر" باشد، فرض می‌کنیم $x_1 = 1$. به همین ترتیب مقادیر بقیه‌ی متغیرها به دست می‌آیند.

این ویژگی در تئوری‌های مختلفی از قضیه‌ی پیچیدگی استفاده می‌شود:

$\mathsf{NP} \subseteq \mathsf{P/poly} \implies \mathsf{PH} = \Sigma_2$ (قضیه‌ی کارپ-لیپتون)

$\mathsf{NP} \subseteq \mathsf{BPP} \implies \mathsf{NP} = \mathsf{RP}$

$\mathsf{P} = \mathsf{NP} \implies \mathsf{FP} = \mathsf{FNP}$

الگوریتم‌های حل‌کننده‌ی SAT

دو رده از الگوریتم‌های با کارایی بالا برای حل مسائل SAT وجود دارد: الگوریتم تضاد-رانده‌ی شناختن عبارت، که می‌توان به عنوان نوعی دیگر از الگوریتم‌های DPLL به آن نگاه کرد، و همچنین الگوریتم‌های اتفاقی جست‌وجوی محلی مانند WalkSAT.

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

حل‌کننده‌های SAT نوین (که در 10 سال گذشته ایجاد شدند) در دو نوع بیان می‌شوند: "تضاد-رانده" و "پیش‌بین". حل‌کننده‌های تضاد-رانده الگوریتم جست‌وجوی DPLL اصلی را با تحلیل تضاد کارآمد، شناختن عبارت، بازگشت بدون ترتیب زمانی (الگوریتم پس‌پرش)، و همچنین انتشار واحد "دو-متغیر-تماشا"، انشعاب انطباقی و راه‌اندازی مجدد تصادفی، افزایش می‌دهند. نشان داده شده است که این "الحاقات" اصولی جست‌وجو به صورت تجربی برای رسیدگی به موارد زیادی از SAT که در اتوماسیون طراحی الکترونیکی (EDA) به وجود می‌آیند ضروری هستند. حل‌کننده‌های پیش‌بین به خصوص کاهش‌ها (رفتن به ورای انتشار عبارت واحد) و کشف‌کننده‌ها را تشدید کردند و در کل در موارد پیچیده از حل‌کننده‌های تضاد-رانده قوی‌تر عمل می‌کنند.

حل‌کننده‌های SAT نوین تاثیرات مهمی بر زمینه‌های تایید نرم‌افزاری، حل‌کردن محدودیت‌های هوش مصنوعی و تحقیق در عملیات‌ دارند. حل‌کننده‌های قوی به آسانی به صورت نرم‌افزار آزاد و متن‌باز در دسترس هستند. به طور خاص نرم‌افزار تضاد-رانده‌ی MiniSAT که در مسابقه‌ی SAT در سال 2005 نسبتا موفق بود، فقط دارای حدود 600 خط برنامه است. یک مثال از حل‌کننده‌های پیش‌بین march_dl است که در مسا‌بقه‌ی SAT در سال 2007 برنده شد.

انواع خاصی از موارد بزرگ تصادفی صدق‌پذیر از SAT با انتشار نظرسنجی (SP) قابل حل هستند. به خصوص در طراحی پردازنده و برنامه‌های تایید، صدق‌پذیری و دیگر خواص منطقی از فرمول‌ گزاره‌ای داده‌شده بعضی اوقات بر پایه‌ی نمایشی از فرمول در نمودار تصمیم‌گیری دودویی (BDD) تصمیم‌گیری می‌شوند.

منابع برای مطالعه‌ی بیشتر

• هسته‌ی صدق‌ناپذیر
• قضایای صدق‌پذیری پیمانه‌ای
• Sharp-SAT

منابع

• Michael R. Garey and David S. Johnson (1979). Computers and Intractability: A Guide to the Theory of NP-Completeness. W.H. Freeman. ISBN 0-7167-1045-5.  A9.1: LO1 – LO7, pp. 259 – 260.
• R. E. Bryant, S. M. German, and M. N. Velev, Microprocessor Verification Using Efficient Decision Procedures for a Logic of Equality with Uninterpreted Functions, in Analytic Tableaux and Related Methods, pp. 1–13, 1999.
• Davis, M.; Putnam, H. (1960). "A Computing Procedure for Quantification Theory". Journal of the ACM 7: 201.
• Davis, M.; Logemann, G.; Loveland, D. (1962). "A machine program for theorem-proving". Communications of the ACM
• Cook, S. A. (1971). "The complexity of theorem-proving procedures". Proceedings of the 3rd Annual ACM Symposium on Theory of Computing: 151–158.
• Marques-Silva, J. P.; Sakallah, K. A. (1999). "GRASP: a search algorithm for propositional satisfiability". IEEE Transactions on Computers 48: 506.
• Marques-Silva, J.; Glass, T. (1999). Combinational equivalence checking using satisfiability and recursive learning. pp. 145.
• Schoning, T. (1999). A probabilistic algorithm for k-SAT and constraint satisfaction problems. pp. 410.
• Moskewicz, M. W.; Madigan, C. F.; Zhao, Y.; Zhang, L.; Malik, S. (2001). Chaff. pp. 530.
• Clarke, E.; Biere, A.; Raimi, R.; Zhu, Y. (2001). Formal Methods in System Design 19: 7.
• Gi-Joon Nam; Sakallah, K. A.; Rutenbar, R. A. (2002). "A new FPGA detailed routing approach via search-based Boolean satisfiability". IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 21: 674.
• Giunchiglia, E.; Tacchella, A. (2004). Giunchiglia, Enrico; Tacchella, Armando. eds. 2919.
• Babic, D.; Bingham, J.; Hu, A. J. (2006). "B-Cubing: New Possibilities for Efficient SAT-Solving". IEEE Transactions on Computers 55: 1315.
• Rodriguez, C.; Villagra, M.; Baran, B. (2007). Asynchronous team algorithms for Boolean Satisfiability. pp. 66.

مطالعه‌ی بیشتر

• Carla P. Gomes, Henry Kautz, Ashish Sabharwal, Bart Selman (2008). "Satisfiability Solvers". In Frank Van Harmelen, Vladimir Lifschitz, Bruce Porter. Handbook of knowledge representation. Foundations of Artificial Intelligence. 3. Elsevier. pp. 89–134. DOI:10.1016/S1574-6526(07)03002-7. ISBN 9780444522115. 

پیوند به بیرون

اطلاعات بیشتر در مورد SAT:

• SAT and MAX-SAT for the Lay-researcher

برنامه‌های SAT:

• WinSAT v2.04

حل‌کننده‌های SAT:

• Chaff
• HyperSAT
• Spear
• The MiniSAT Solver
• UBCSAT
• Sat4j
• RSat
• Fast SAT Solver - یک اجرای ساده اما سریع برای حل‌کننده‌ی مسئله‌ی صدق‌پذیری بر پایه‌ی الگوریتم ژنتیک
• PicoSAT
• CryptoMiniSat

کنفرانس بین‌المللی درباره‌ی قضیه و برنامه‌های آزمایش صدق‌پذیری:

• SAT 2011
• SAT 2010
• SAT 2009
• SAT 2008
• SAT 2007

انتشارات:

• Journal on Satisfiability, Boolean Modeling and Computation
• Survey Propagation

برنامه‌های محک:

• Forced Satisfiable SAT Benchmarks
• IBM Formal Verification SAT Benchmarks
• SATLIB
• Software Verification Benchmarks
• Fadi Aloul SAT Benchmarks

حل کردن SAT در حالت کلی:

• http://www.satlive.org
• http://www.satisfiability.org

ارزیابی حل‌کننده‌های SAT:

• Yearly evaluation of SAT solvers
• SAT solvers evaluation results for 2008

---

این مقاله شامل موادی از یک ستون در ACM SIGDA e-newsletter توسط Prof. Karem Sakallah می‌باشد.