الگوریتم DPLL

الگوریتم DPLL (کوته‌نوشت Davis–Putnam–Logemann–Loveland) در منطق و علوم رایانه، یک الگوریتم جستجوی کامل و مبتنی بر پس‌گرد برای تصمیم‌گیری برای صدق‌پذیری فرمول‌های منطق گزاره‌ای در حالت نرمال عطفی است، به عبارت دیگر الگوریتم DPLL دارد مساله CNF-SAT را حل می کند.

این الگوریتم در سال 1961 توسط مارتین دیویس، جرج لاگِمن، و دونالد لاولند معرفی گردید، که یک روش اصلاحی برای الگوریتم پیشین دیویس-پاتنام بود، که این الگوریتم یک فرایند مبتنی بر رزلوشن بود که توسط دیویس و هیلاری پاتنم در سال 1960 توسعه داده شد. بخصوص در نشریات قدیمی، به الگوریتم دیویس-پاتانم-لاولند، «روش دیویس-پاتنام» یا «الگوریتم DP» گفته می شد. نام‌های معمول‌تر دیگری که این تفاوت را حفظ نموده اند، DLL و DPLL می باشند.

بعد از حدود 50 سال، هنوز هم فرایند DPLL مبنایی برای موثرترین حل‌کننده‌های کامل SAT می باشد. این الگوریتم، به تازگی برای اثبات قضیه خودکار برای قطعه‌هایی از منطق مرتبه اول به روش الگوریتم DPLL(T) گسترش داده شده است.

پیاده‌سازی و کاربردها

مسئله SAT هم از دیدگاه نظری و هم عملی مهم می باشد. در نظریه پیچیدگی، اولین مساله ای بود که ثابت شد که ان‌پی کامل است. این مساله در موارد متنوع و گسترده‌ای مثل «وارسی مدل»، «زمان‌بندی و برنامه‌ریزی خودکار» و «تشخیص در هوش مصنوعی» کاربرد دارد.

از این رو، این الگوریتم سال ها یک عنوان با پژوهش فراوان بوده است، و به صورت منظم صحنه رقابت‌های زیادی بین حل‌کننده‌های SAT بوده است. در سال‌های اخیر، پیاده‌سازی های نوین DPLL مثل چاف و زدچاف، GRASP یا MiniSat در مقام اول این رقابت‌ها بوده اند.

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

الگوریتم

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

با استفاده حریصانه این قواعد در هر گام، الگوریتم DPLL روی الگوریتم پسگرد، افزایش می یابد:

انتشار واحد

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

حذف لیترال خالص

یک لیترال موقعی خالص است که در فرمول فقط یک جهت قطبیت داشته باشد. یک لیترال خالص را همیشه می توان به صورتی انتساب داد که همه بندهای شامل کننده اش را «درست» کند. از این رو اگر به این شیوه انتساب داده شود، این بندها دیگر جستجو را محدودسازی نمی کنند، و قابل حذف می شوند.

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

الگوریتم DPLL را می توان در شبه کد زیر خلاصه کرد، که در آن Φ همان فرمول CNF است:

Algorithm DPLL
    Input: A set of clauses Φ.
    Output: A Truth Value.

function DPLL(Φ)
    if Φ is a consistent set of literals then
        return true;
    if Φ contains an empty clause then
        return false;
    for every unit clause {l} in Φ do
        Φ ← unit-propagate(l, Φ);
    for every literal l that occurs pure in Φ do
        Φ ← pure-literal-assign(l, Φ);
    l ← choose-literal(Φ);
    return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {not(l)});

• "←" denotes assignment. For instance, "largest ← item" means that the value of largest changes to the value of item.
• "return" terminates the algorithm and outputs the following value.

در این شبه‌کدunit-propagate(l, Φ) و pure-literal-assign(l, Φ) توابعی هستند که نتیجه اعمال انتشار واحد و قاعده لیترال خالص را برای لیترال l و فرمول Φ به ترتیب برمی گردانند. به زبان دیگر، این توابع در فرمول Φ هر رخداد l را به «درست» و هر رخداد not l را با «نادرست» جایگزین می کنند، و سپس فرمول نتیجه شده را ساده‌سازی می کنند. or موجود در عبارت return یک عملگر اتصال کوتاه است. Φ ∧ {l} نشان دهنده نتیجه ساده‌سازی شده جایگزینی «درست» برای l در Φ است.

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

شبه‌کد تابع DPLL فقط این موضوع را برمی گرداند که آیا انتساب نهایی برای فرمول برآورده می کند یا نه. در یک پیاده‌سازی واقعی، یک انتساب نیمه صادق نیز معمولا موفقیت را برمی گرداند؛ این موضوع از مجموعه سازگار لیترال های بیانیه if اول در تابع قابل مشتق کردن است.

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

نحوه تصور

در سال 1961 دیویس، لاگمن، لاومن این الگوریتم را ایجاد کردند. بعضی از ویژگی های این الگوریتم از این قرار است:

• بر اساس جستجو می باشد.
• مبنای تقریبا همه حل‌کننده های SAT نوین است.
• از پسگردهایی که یادگیرنده اند یا غیرزمانی اند استفاده نمی کند.

یک مثال با تصور یک الگوریتم DPLL که پسگرد زمانی دارد:

• 
  All clauses making a CNF formula
• 
  Pick a variable
• 
  Make a decision, variable a = False (0), thus green clauses becomes True
• 
  After making several decisions, we find an implication graph that leads to a conflict.
• 
  Now backtrack to immediate level and by force assign opposite value to that variable
• 
  But a forced decision still leads to another conflict
• 
  Backtrack to previous level and make a forced decision
• 
  Make a new decision, but it leads to a conflict
• 
  Make a forced decision, but again it leads to a conflict
• 
  Backtrack to previous level
• 
  Continue in this way and the final implication graph

کارهای جدید روی الگوریتم

در سال‌های دهه 2010، کار روی بهبود الگوریتم در سه جهت انجام شد:

1. تعریف سیاست‌های متنوع برای انتخاب لیترال انتشعاب.
2. تعریف ساختمان داده های جدید برای سریع‌سازی الگوریتم، مخصوصا بخش مرتبط با انتشار واحد.
3. تعریف انواع الگوریتم پسگرد اصلی. که در این جهت آخر شامل «پسگردهای غیرزمانی» (که به آن پس‌پرش گفته می شود) و یادگیری بند است. این اصلاحات توصیف کننده یک روش پسگرد بعد از رسیدن به یک بند متعارض است که بند ریشه ای (انتساب به متغیرها) در تعارض را با هدف جلوگیری از رسیدن به تعارض مشابه به صورت مجدد، «یاد می گیرد». حل‌کننده های نتیجه شده SAT که حالت یادگیری بند مبتنی بر تعارض دارند، موضوع پژوهش های تازه زیادی در سال 2014 بوده است.

یک الگوریتم جدیدتر از سال 1990، روش استالمارک است. از این رو از سال 1986 نمودارهای تصمیم دودویی (با مرتبه پایین) برای حل SAT استفاده شده است.

ارتباط با دیگر مفاهیم

اجرای الگوریتم‌های مبتنی بر DPLL روی نمونه‌های صدق‌ناپذیر متناظر است با اثبات های انکار وجود رزلوشن درختی.

منابع

مشارکت‌کنندگان ویکی‌پدیا. «DPLL algorithm». در دانشنامهٔ ویکی‌پدیای انگلیسی، بازبینی‌شده در ۴ مهٔ ۲۰۲۱.