مسئلهٔ SAT می‌پرسد آیا می‌توان به متغیرهای منطقی مقدار درست یا نادرست داد تا همهٔ شرط‌های یک فرمول برقرار شوند. DPLL این جست‌وجو را با عقب‌گرد و ساده‌سازیِ بندها انجام می‌دهد. در این صفحه، یک انتخابِ اولیه واقعاً به تناقض می‌رسد، عقب‌گرد ثبت می‌شود و انتخابِ جایگزین جواب می‌دهد؛ نتیجه را هم با جدول حقیقتِ مستقل کنترل می‌کنیم.
ورودیِ CNF چه قراردادی دارد؟
فرمولِ آموزشیِ اول سه بند دارد: (A∨B) و (¬A∨B) و (¬A∨¬B). درون هر بند، «یا» داریم و میان بندها «و»؛ پس همهٔ بندها باید درست شوند، اما در هر بند کافی است یکی از لفظ‌ها درست باشد. A با ¬A فرق دارد؛ دومی نقیض همان متغیر است، نه نام یک متغیر مستقل.
در فایل، A با عدد۱ و B با۲ نمایش داده می‌شود؛ علامت منفی نقیض است. بنابراین سه بند به [[۱،۲]،[−۱،۲]،[−۱،−۲]] تبدیل شده‌اند. این اعداد مقدار احتمال یا برچسبِ طبقه‌بندی نیستند. فایلِ کوچک، لفظ‌های صحیحِ غیرصفر با شمارهٔ حداکثر۸ را می‌پذیرد؛ متن طبیعی را به منطق ترجمه نمی‌کند.
چرا شاخهٔ A=درست رد می‌شود؟
در آغاز بندِ تک‌لفظی و نمادِ خالص نداریم. ترتیبِ جست‌وجو ثابت است: اول A و ابتدا مقدارِ درست. بندِ اول با A درست می‌شود، اما بندِ دوم B و بندِ سوم ¬B را لازم دارند. قاعدهٔ بندِ واحد، B را درست می‌گذارد؛ اکنون بندِ ¬B نادرست است و هیچ لفظِ نامعلوم در آن نمانده است. این یک شکستِ واقعیِ همان شاخه است.
برنامه رویدادِ conflict و سپس backtrack با متغیر و مقدارِ ردشده را ثبت می‌کند. شکستِ یک شاخه دلیلِ بی‌جواب‌بودنِ تمام فرمول نیست؛ شاخهٔ A=نادرست هنوز بررسی نشده است. از همین نقطه برمی‌گردیم، نه اینکه B را در همان شاخه بی‌اجازه عوض کنیم و علتِ شکست را گم کنیم.
شاخهٔ دوم جوابِ مشترک می‌دهد
با A=نادرست، بندِ اول B را لازم دارد و دو بندِ دیگر به‌واسطهٔ ¬A درست می‌شوند. قرار‌دادن B=درست هر سه بند را برقرار می‌کند. خروجی نهایی A=نادرست و B=درست است؛ کد تمامِ بندهای اصلی را با همین انتساب دوباره ارزیابی می‌کند.
| فرمول | خروجی DPLL | کنترل مستقل |
|---|---|---|
| سه بندِ اولیه | یک جواب: Aنادرست، Bدرست | چهار انتساب؛ فقط همین یک جواب |
| افزودنِ بندِ A∨¬B | بی‌جواب | چهار انتساب؛ هیچ جواب |
در مثالِ دوم، بندِ تازه تنها جوابِ قبلی را رد می‌کند. تابعِ DPLL هر دو شاخه را واقعاً می‌گردد و تابعِ مستقلِ جدول حقیقت نیز هر چهار ترکیبِ دو متغیر را می‌سنجد؛ نتیجهٔ «بی‌جواب» از حدس دربارهٔ متن نیامده است.
بندِ واحد، نمادِ خالص و پایان زودهنگام
اگر بندِ هنوز برقرار‌نشده فقط یک لفظِ نامعلوم داشته باشد، برای درست‌کردن فرمول همان لفظ باید درست شود. اگر متغیری در بندهای باقی‌مانده فقط با یک علامت ظاهر شود، می‌توان با همان علامت راضی‌اش کرد؛ کد این نمادِ خالص را در نمونهٔ جدا واقعاً اجرا می‌کند. همچنین وقتی همهٔ بندها از قبل درست‌اند، لازم نیست برای متغیرهای بی‌اثر شاخه‌سازی ادامه پیدا کند؛ نسخهٔ خروجی آن‌ها را طبق قرارداد نادرست کامل می‌کند.
دو حالتِ خالی را اشتباه نگیرید: فهرستِ بدون بند، یعنی هیچ شرطی برای نقض وجود ندارد و در این قرارداد درست است. وجودِ یک بندِ خالی یعنی «یا»یی بدون هیچ لفظِ درست‌پذیر و در نتیجه نادرست. هر دو حالت در فایل آزموده می‌شوند؛ یکی SAT و دیگری UNSAT است.
سازگاریِ محلی با جوابِ کامل فرق دارد
AC-3 و فیلترِ دامنه ممکن است بدون پیداکردنِ جوابِ مشترک تمام شود؛ اینجا جست‌وجو تا انتسابِ تأییدشده یا ردِ همهٔ شاخه‌ها ادامه دارد. البته این پیاده‌سازی حل‌کنندهٔ صنعتیِ SAT نیست؛ یادگیری بندِ تعارض، watched literals و اثباتِ قابل‌بررسیِ مستقل برای مسئلهٔ بزرگ تولید نمی‌کند. جدول حقیقتِ دو متغیر هم معیارِ سرعت یا مقیاس‌پذیری نیست.
در استفادهٔ واقعی، درستیِ تبدیلِ نیاز به فرمول به اندازهٔ حل فرمول مهم است. جوابِ منطقی برای قواعدِ ناقص، صحتِ تصمیمِ کسب‌وکار را ثابت نمی‌کند. در راهکارهای اپرا شرط‌های پاسخ و اختیارِ اقدام را با مثالِ پذیرش مشخص کنید؛ این تمرین ادعای استفادهٔ داخلی از DPLL در محصول ندارد.
فایل تمرین و منبع
کد کامل Python؛ محاسبه و کنترل‌های مستقل · ورودیِ ساخته‌شده، مراحل و خروجیِ اجرای واقعی
منابع در 2026-11-04 خوانده شدند؛ این تاریخ، تاریخ انتشار منبع نیست. مثال‌ها و فایل‌های این راهنما آموزشی و ساختهٔ تحریریه‌اند.