ДПЛЛ алгоритам

У рачунарству, Дејвис–Патнам–Логман–Ловеланд (ДПЛЛ) алгоритам је комплетан, заснован на бектрекинг алгоритмом претраге за одлучивање задовољивости исказне логичке формуле у конјуктивној нормалној форми, т.ј. за решавање КНФ-САТ проблем.

Представљен је 1962. године од стране Мартина Дејвиса, Хилари Патнама, Џорџа Логмана и Доналда Ловеланда и он је усавршавање ранијег Дејвис–Патнам алгоритма, који је резолуцијски-базирана процедура развијена од стране Дејвиса и Патнама 1960. године. Специјално у старијим публикацијама, Дејвис-Логман-Ловеланд је често реферисан као “Дејвис-Патнам метод” или “ДП алгоритам”. Остала позната имена која одржавају одлику су ДЛЛ и ДПЛЛ.

После скоро 50 година ДПЛЛ процедура и даље формира основе за најефикасније комплетне SAT решаваче. Скоро је проширен за аутоматизовану теорему о доказивању за фрагменте логике првог реда.

DPLL

Класа	Проблем задовољивости
Најгора перформанца	$O(2^{n})$
Најгора просторна комплексност	$O(n)$ (базни алгоритам)

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

САТ проблем је важан са обе, теоријске и практичне, тачке гледишта. У комплексној теорији био је први доказан проблем да је НП-комплетан, и може да се појави у широком спектру апликација као што су провера модела, аутоматизовано планирање и распоређивање, и дијагноза у вештачкој интелигенцији.

Као такав, био је и још је популарна тема у истраживању већ дуги низ година, и такмичења између САТ решавача се редовно одржавају. DPLL-ове модерне имплементације као Chaff и zChaff, GRASP или Minisat су на првим местима у такмичењима последњих година.

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

Алгоритам

Основни бектрекинг алгоритам се покреће избором литерала, преписујући му тачну вредност, поједностављивањем формуле потом и рекурзивне провере да лу је формула задовољива; ако је ово случај, оригинална формула је задовољива; у супротном, иста рекурзивна провера се обавља под претпоставком нетачне вредности. Ово је познато као splitting rule, јер дели проблем на два једноставнија потпроблема. Корак поједностављивања у суштини брише све клаузе које су постале тачне по додели из формуле, и сви литерали који су постали нетачни из преосталих клауза.

ДПЛЛ алгоритам се побољшава преко бектрекинг алгоритма по жељеној употреби следећих правила у сваком кораку:

Unit propagation

Ако је клауза јединична клауза, т.ј. садржи само један недодељен литерал, ова клауза може бити једино задовољива додељивањем неопходне вредности да би овај литерал био тачан. Према томе, није потребан избор. У пракси, ово често води до детерминистичких каскада јединица, према томе избегава велики део наивне претраге простора.

Pure literal elimination

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

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

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

  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 у Φ.

Псеудокод ДПЛЛ функција враћа само да ли је крајња додела задовољава формулу или не. У реалној имплементацији, делимична задовољива формула обично такође враћа успех; ово се може извести из конзистентног скупа литерала првог if израза у функцији.

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

Тренутни рад

у 2010. години, рад на побољшању алгоритма је урађен у три правца:

1. Дефинисање различитих политика за избор литерала гранања
2. Дефинисање нове сатруктуре података да би алгоритам постао бржи, посебно за део unit propagation
3. Дефинисање варијанте базичног backtracking алгоритма. Други правац обухватају не хронолошки Бектрекинг (или backjumping) и учење клауза. Ова побољшања описују методу бектрекинг након постизања конфликт клаузе која "учи" основне узорке (задатке за променљиве) конфликта како би се избегло достизање истог конфликта поново. Добијени Conflict-Driven Clause Learning САТ решавачи су стање уметности у 2014. години.

Однос са другим појмовима

Рад на ДПЛЛ базираним алгоритмима на незадовољивим случајевима одговарају стаблу резолуције за побијање доказа.

Референце

General

• Davis, Martin; Putnam, Hilary (1960). „A Computing Procedure for Quantification Theory”. Journal of the ACM. 7 (3): 201—215. S2CID 31888376. doi:10.1145/321033.321034. 
• Davis, Martin; Logemann, George; Loveland, Donald (1962). „A Machine Program for Theorem Proving”. Communications of the ACM. 5 (7): 394—397. S2CID 15866917. doi:10.1145/368273.368557. hdl:2027/mdp.39015095248095. 
• Ouyang, Ming (1998). „How Good Are Branching Rules in DPLL?”. Discrete Applied Mathematics. 89 (1–3): 281—286. doi:10.1016/S0166-218X(98)00045-6. 
• Harrison, John (2009). Handbook of practical logic and automated reasoning. Cambridge University Press. стр. 79–90. ISBN 978-0-521-89957-4. 

Specific

Литература

• Marques-Silva, João (1999). „The Impact of Branching Heuristics in Propositional Satisfiability Algorithms”. Progress in Artificial Intelligence. Lecture Notes in Computer Science. 1695. стр. 62—74. ISBN 978-3-540-66548-9. doi:10.1007/3-540-48159-1_5. 
• Beek, Peter Van (2006). „Backtracking search algorithms”. Ур.: Francesca Rossi, Peter Van Beek, Toby Walsh. Handbook of constraint programming. Elsevier. стр. 122. ISBN 978-0-444-52726-4. CS1 одржавање: Вишеструка имена: списак уредника (веза)