Дејвис–Патнам–Логман–Ловеланд (ДПЛЛ) алгоритам

ДПЛЛ алгоритам је техника за решавање проблема задовољивости булових формула, који покушава да утврди да ли постоји комбинација „тачно“ или „нетачно“ за променљиве која задовољава формулу у конјунктивној нормалној форми (ЦНФ). Овај проблем је важан у рачунарству, јер је основа за многе логичке и рачунске проблеме.

Историјат

Овај алгоритам је развијен 1961. године од стране Мартина Дејвиса, Џорџа Логемана и Доналда В. Ловеланда, као унапређење ранијег Дејвис-Путнам алгоритма, који је развио Дејвис са Хилари Путнамом 1960. године. Алгоритам ДПЛЛ је често називан и "Дејвис-Путнам методом" или "ДП алгоритмом", а у неким случајевима се користи и скраћеница ДЛЛ.

Имплементација и примене

САТ проблем је веома важан у рачунарским наукама јер се користи за проверу да ли је нека логичка формула могућа (задовољива). Он је први проблем који је доказано НП-комплетан, што значи да је веома тешко решити га за велике примере.

САТ проблем има много примена, као што су:

Модел-чековања: Проверава да ли неки рачунарски модел ради исправно.
Аутоматизовано планирање: Креирање планова који испуњавају одређене циљеве.
Дијагноза у вештачкој интелигенцији: Проналажење проблема у сложеним системима.

За решавање САТ проблема, користе се алгоритми као што је ДПЛЛ, који је веома популаран у истраживањима и такмичењима. У међународним такмичењима,софтвери као што је Minisat^[1] који користе ДПЛЛ, освајали су прва места.

Алгоритам

Избор променљиве и додела вредности: Алгоритам бира једну променљиву (нпр. x) и додељује јој вредност „тачно“ или „нетачно“. Затим проверава да ли формула постаје тачна или нетачна са том доделом. Ако се формула задовољи, завршавамо – нашли смо решење. Ако не, алгоритам ће касније испробати другу вредност (користећи тзв. backtracking).
Јединичне клаузе (unit propagation): Ако у формули постоји клауза са само једним литералом (нпр. само x или само ¬x), тај литерал мора бити тачан да би клауза била испуњена. Овим кораком, алгоритам уклања много могућих додела вредности, јер зна да јединичне клаузе морају бити испуњене. Пример: ако у формули постоји само x, онда алгоритам поставља x на „тачно“.
Чисте променљиве : Ако се нека променљива појављује само као позитиван (само x) или само као негативан литерал (само ¬x), може јој се доделити вредност која задовољава све клаузе у којима се појављује. На пример, ако имамо x који се јавља само у позитивном облику, поставићемо га на „тачно“, што уклања све клаузе које садрже x, јер су већ задовољене.
Враћање уназад (backtracking): Ако ниједна од додела не води ка решењу, алгоритам се враћа корак уназад (backtrack) и испробава другу вредност за променљиву. Ово омогућава алгоритму да испроба све комбинације вредности ако је потребно, али користећи предности јединичних клаузи и чистих променљивих да брже елиминише лоше комбинације.
Заустављање: Алгоритам се зауставља ако:

Нађе доделу која чини формулу тачном, што значи да је задовољива.
Ако не може да задовољи формулу јер је свака могућа додела испробана и ниједна не ради, онда закључује да формула није задовољива.

ПЛЛ алгоритам се може резимирати у следећем псеудокоду, где је Φ је КНФ формула:

  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 Φ
      Φ ← unit-propagate(l, Φ);
   for every literal l that occurs pure in Φ
      Φ ← pure-literal-assign(l, Φ);
   l ← choose-literal(Φ);
   return DPLL(Φ ∧ l) or DPLL(Φ ∧ not(l));

У овом псеудокоду, unit-propagate(l, Φ) и pure-literal-assign(l, Φ) су функције које враћају резултат примене правила unit propagation и the pure literal, до литерала l и формуле Φ. Другим речима, оне замењују свако појављивање l са "тачно" и свако појављивање not l са "нетачно" у формули Φ, и поједностављује резултујућу формулу. or у return исказ је оператор кратког споја. Φ ∧ l означава поједностављен резултат замене "тачно" за l у Φ.

Псеудокод ДПЛЛ функција враћа само да ли је крајња додела задовољава формулу или не.

Дејвис-Логман-Ловеланд алгоритам зависи од избора литерала гранања, који је литерал размотрен у бектрекинг кораку. Као резултат тога, ово није баш алгоритам, већ фамилија алгоритама. Ефикасност је јако погођена избором литерала гранања: постоје инстанце за које је време извршавања константно или експоненцијално у зависности од избора литерала гранања. Такве функције се такође зову хеуристичке функције или хеуристике гранања.

ДПЛЛ алгоритам је веома важан јер је основ за већину модерних САТ софтвера, а такође је повезан и са многим другим техникама у области логике и вештачке интелигенције.

Референце

↑ „Minisat website“.

[1] „Minisat website“.

[1]