موضوع مقاله: الگوریتم DPLL | مخاطب: عمومی | لحن: دانشنامه‌ای | ساختار: عنوان، مقدمه، 3 بخش، جمع‌بندی | مقاله: | # الگوریتم DPLL | مقدمه: این الگوریتم در سال ۱۹۶۱ توسط مارتین دیویس، جرج لاگِمن، و دونالد لاولند معرفی گردید، که یک روش اصلاحی برای الگوریتم پیشین دیویس-پاتنام بود. | ## بخش 1: الگوریتم DPLL | بخصوص در نشریات قدیمی، به الگوریتم دیویس-پاتانم-لاولند، «روش دیویس-پاتنام» یا «الگوریتم DP» گفته می‌شد. بعد از حدود ۵۰ سال، هنوز هم فرایند DPLL مبنایی برای موثرترین حل‌کننده‌های کامل SAT می‌باشد. این الگوریتم، امروزه، این الگوریتم، در زمینه اثبات قضیه خودکار برای قطعه‌هایی از منطق مرتبه اول، به روش الگوریتم DPLL(T) گسترش داده شده‌است. در نظریه پیچیدگی، این الگوریتم، اولین مسئله‌ای بود که ثابت شد که ان‌پی کامل است. مسئله SAT در موارد متنوع و گسترده‌ای مثل «وارسی مدل»، «زمان‌بندی و برنامه‌ریزی خودکار» و «تشخیص در هوش مصنوعی» کاربرد دارد. از این رو، این الگوریتم سال‌ها مورد پژوهش‌های فراوان بوده‌است، و به صورت منظم صحنه رقابت‌های زیادی بین حل‌کننده‌های SAT بوده‌است. یک کاربرد دیگر که DPLL را درگیر نموده‌است، اثبات قضیه خودکار، یا رضایت به پیمانه نظریات (SMT) است. SMT یک نظریه SAT است که در آن متغیرهای گزاره‌ای توسط فرمول‌های دیگر نظریهٔ ریاضیاتی جایگزین شده‌اند. الگوریتم الگوریتم پس‌گرد اصلی توسط انتخاب یک لیترال، انتساب یک مقدار درستی به آن، ساده‌سازی فرمول، و سپس بررسی بازگشتی این موضوع رخ می‌دهد که آیا فرمول ساده‌سازی شده صدق‌پذیر هست یا نه؛ اگر صدق‌پذیر بود، یعنی فرمول اصلی صدق‌پذیر است، در غیر این صورت، با فرض مقدار درستی معکوس، بررسی بازگشتی مشابهی باید انجام شود. به این موضوع «قاعده جداسازی» گفته می‌شود، زیرا مسئله را به دو زیرمسئله ساده‌تر جداسازی می‌کند. گام ساده‌سازی به صورت اساسی این است که همه بندهایی که تحت انتساب از فرمول، «درست» می‌شوند، و همه لیترال‌هایی که از بندهای باقیمانده «نادرست» می‌شوند، را حذف می‌کند. با استفاده حریصانه این قواعد در هر گام، الگوریتم DPLL روی الگوریتم پسگرد، افزایش می‌یابد: انتشار واحد اگر بند یک «بند واحد» باشد، یعنی فقط شامل یک «لیترال انتساب نیافته و منفرد» باشد، این بند فقط با انتساب مقدار لازم برای درست ساختن این لیترال، صدق‌پذیر می‌شود. | ## بخش 2: الگوریتم DPLL | انتشار واحد شامل حذف هر بندی است که شامل لیترال بند واحد است و نیز شامل حذف مکمل لیترال بند واحد از هر بندی است که شامل آن مکمل است. در عمل این کار معمولاً منجر به فروریختن قطعی واحدها می‌شود، از این رو از قسمت بزرگی از فضای جستجوی اولیه جلوگیری می‌شود. حذف لیترال خالص یک لیترال موقعی «خالص» است که در فرمول فقط یک جهت قطبیت داشته باشد. یک لیترال خالص را همیشه می‌توان به صورتی انتساب داد که همه بندهای شامل کننده اش را درست کند. از این رو اگر به این شیوه انتساب داده شود، این بندها دیگر جستجو را محدودسازی نمی‌کنند، و قابل حذف می‌شوند. یک انتساب جزئی داده شده موقعی صدق‌ناپذیری اش تشخیص داده می‌شود که یکی از بندها «خالی» شود، یعنی همه متغیرهایش به شیوه ای منتسب شوند که لیترال‌های متناظر را نادرست کنند. صدق‌پذیری فرمول در دو حالت تشخیص داده می شود: یا موقعی که همه متغیرها را انتساب دهیم اما بند خالی تولید نشود، یا در پیاده‌سازی‌های نوین، اگر همه بندها صادق شوند. به زبان دیگر، این توابع در فرمول Φ هر رخداد l را به «درست» و هر رخداد not l را با «نادرست» جایگزین می‌کنند، و سپس فرمول نتیجه‌شده را ساده‌سازی می‌کنند. این الگوریتم در یکی از این دو حالت خاتمه می‌یابد: یا اینکه فرمول CNF ای با نام Φ پیدا می‌شود که شامل مجموعه سازگاری از لیترال‌ها باشد، یعنی هیچ l و ¬l ای برای لیترال l در فرمول موجود نباشد. اگر این موضوع رخ دهد، متغیرها را به صورت بدیهی با تنظیم آن‌ها به قطبیت متناظر لیترال شامل‌شونده در ارزیابی صادق می‌کنیم. در غیر این صورت، موقعی که فرمول شامل یک بند خالی باشد، این بند به صورت پوچ «نادرست» است، زیرا یک فصل حتماً نیاز دارد تا حداقل یک عضوش درست باشد تا مجموعه کلی درست شود. در این حالت، وجود چنین بندی به معنی آن است که فرمول (که به صورت عطف همه بندها ارزیابی می‌شود) را نمی‌توان «درست» ارزیابی کرد، و فرمول باید صدق‌ناپذیر باشد. | ## بخش 3: الگوریتم DPLL | شبه‌کد تابع DPLL فقط این موضوع را برمی‌گرداند که آیا انتساب نهایی برای فرمول، صدق‌پذیر هست یا نه. در یک پیاده‌سازی واقعی، یک انتساب نیمه‌صادق نیز معمولاً موفقیت را برمی‌گرداند؛ این موضوع از مجموعه سازگار لیترال‌های بیانیه if اول در تابع، قابل دستیابی است. الگوریتم دیویس-لاگمن-لاولند به گزینه «لیترال انتشعابی» بستگی دارد، که همان لیترالی است که در گام پسگرد درنظرگرفته شده‌است. و این موضوع، یعنی الگوریتم DPLL یک الگوریتم دقیق نیست، بلکه «خانواده‌ای از الگوریتم‌ها» است، که هر عضو آن خانواده یک روش ممکن برای انتخاب لیترال انشعاب دارد. «کارایی» الگوریتم به شدت از نحوه انتخاب گزینه لیترال انشعاب تأثیر می‌پذیرد: نمونه‌هایی وجود دارد که در آن زمان اجرایی ثابت است، و همچنین در نمونه‌هایی زمان‌اجرا نمایی است، این موضوع بستگی به نحوه انتخاب لیترال‌های انشعابی دارد. یک مثال با تصور مرتبط با آن از یک الگوریتم DPLL که پسگرد زمانی دارد: کارهای جدید روی الگوریتم در سال‌های دهه ۲۰۱۰، کار روی بهبود الگوریتم در سه جهت انجام شد: تعریف سیاست‌های متنوع برای انتخاب لیترال انتشعاب. تعریف ساختمان داده‌های جدید برای سریع‌سازی الگوریتم، که مخصوصاً مرتبط با بخش انتشار واحد بود. که این جهت آخر شامل «پسگردهای غیرزمانی» (که به آن پس‌پرش گفته می‌شود) و یادگیری بند است. این اصلاحات توصیف‌کننده یک روش پسگرد بعد از رسیدن به یک بند متعارض است، که یعنی بند ریشه‌ای (انتساب به متغیرها) موجود در تعارض را با هدف جلوگیری از رسیدن به تعارض‌های مشابه در آینده «یادمی‌گیرد». حل‌کننده‌های SAT نتیجه‌شده، که حالت یادگیری بند مبتنی بر تعارض دارند، موضوع پژوهش‌های جدید و زیادی در سال ۲۰۱۴ بوده‌اند. از این رو از سال ۱۹۸۶، از نمودارهای تصمیم دودویی (با مرتبه پایین) برای حل SAT استفاده شده‌است. | ## جمع‌بندی | ارتباط با دیگر مفاهیم اجرای الگوریتم‌های مبتنی بر DPLL روی نمونه‌های صدق‌ناپذیر با «اثبات‌های انکار وجود رزلوشن درختی» متناظر است.