DPLL алгоритм

Якщо диз'юнкта містить рівно одну змінну, якій ще не задали значення, ця диз'юнкта може прийняти значення «істина» тільки в разі присвоєння змінній значення, яке зробить її істинною («істина», якщо змінна входить в диз'юнкт без заперечення та «брехня», якщо змінна з запереченням). Таким чином, не потрібно робити вибір на даному етапі. На практиці за цим слідує багато присвоєнь змінним значень, та через це істотно скорочується кількість варіантів перебору.

Якщо деяка змінна входить в формулу тільки з однієї «полярністю», тобто без заперечень, або тільки з запереченнями, вона називається чистою. «Чистим» змінним завжди можна задати значення так, що всі утримуючи її диз'юнкти стануть істинними. Таким чином, ці диз'юнкти не впливатимуть на простір варіантів та їх можна буде видалити.

Нездійсненність, при даних конкретних значеннях змінних, визначається коли одна з диз'юнкт стає «порожня», тобто всім її змінним задаються значення таким чином, що їх входження стають помилковими. Здійснимість формули констатується або коли всім змінним задані значення так, що не виникає «порожніх» диз'юнкт, або (в сучасних реалізація) кожна диз'юнкта дорівнює істини. Нездійсненність формули може бути встановлена тільки після закінчення перебору. Алгоритм DPLL може бути виражений за допомогою наступного псевдокоду, де знаком Φ позначена формула в кон'юнктивній нормальній формі (КНФ):

Алгоритм DPLL
        Вхідні дані: Набір диз'юнкт формули Φ.
        Вихідні дані: Значення істинності

Псевдокод:

function DPLL(Φ)
   if Φ - набір виконуваних диз'юнкт
       then return true;
   if Φ містить порожню диз'юнкту
       then return false;
    for each диз'юнкти з однією змінною l in Φ
      Φ  ←  unit-propagate(l, Φ);
   for each l яка зустрічається в "чистому" вигляді in Φ
      Φ   ←   pure-literal-assign(l, Φ);
   l ←  choose-literal(Φ);
   return DPLL(Φ&l) or DPLL(Φ&not(l));

У цьому псевдокоді unit-propagate(l, Φ) й pure-literal-assign(l, Φ) — це функції, які повертають результат застосовуваний до змінної l в формулі Φ — поширення змінної та правила виключення «чистої змінної». Іншими словами, вони замінють кожне входження змінної lзначенням «істина» та кожне входження змінної з запереченням not l значенням «брехня» у формулі Φ, а потім спрощують результативну формулу. Наведений псевдокод повертає тільки відповідь — чи виконує формулу останній з присвоєних наборів значень чи ні. У сучасних реалізаціях, часткові виконувані набори, теж повертаються у разі успіху.

Алгоритм залежить від вибору «змінної розгалуження», тобто змінної, яка вибирається на черговому кроці алгоритму з поверненням присвоєння їй певного значення. Таким чином, це не один алгоритм, а ціле сімейство алгоритмів, по одному на кожен можливий спосіб вибору «змінних розгалуження». Ефективність алгоритму сильно залежить від цього вибору. Час роботи алгоритму (для яких може бути ${\displaystyle const}$ або рости експоненціально) в залежності від вибору «змінних розгалуження». Методи вибору — евристичні техніки, які називаються також «евристиками для розгалуження» (branching heuristics).

Девіс, Логемана, Лавленд (1962) розробили цей алгоритм. Деякі властивості алгоритму:

• Він засновується для пошуку.
• Він є основою для багатьох сучасних вирішувачів SAT.
• Він не використовує джерела введено в 1996 році.

Приклад з візуалізацією алгоритму DPLL, що має хронологічні джерела:

• 
  Всі можливі випадки КНФ формул.
• 
  Вибираємо змінну.
• 
  Приймаємо рішення, змінна а = False (0), таким чином, зелені положення стають True.
• 
  Після кількох рішень, ми знаходимо імплікаційний граф, який призводить до конфлікту.
• 
  Тепер повертаємося назад та надаємо значення змінній.
• 
  Рішення все ще приводить до іншого конфлікту.
• 
  Повертаємося на попередній рівень.
• 
  Зробили нове рішення але це призводить до конфлікту також.
• 
  Зробили ще одне зміщення але знову це призводить до конфлікту.
• 
  Повертаємося на попередній рівень.
• 
  Продовжуємо таким же чином до остаточного імплікаційного графу.