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

С Википедије, слободне енциклопедије
Пређи на навигацију Пређи на претрагу

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

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

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

DPLL
Backtracking-no-backjumping.svg
КласаПроблем задовољивости
Најгора перформанца
Најгора просторна комплексност (базни алгоритам)

Имплементације и апликације[уреди | уреди извор]

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

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

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

Алгоритам[уреди | уреди извор]

Основни бектрекинг алгоритам се покреће избором литерала, преписујући му тачну вредност, поједностављивањем формуле потом и рекурзивне провере да лу је формула задовољива; ако је ово случај, оригинална формула је задовољива; у супротном, иста рекурзивна провера се обавља под претпоставком нетачне вредности. Ово је познато као 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, Φ);
   lchoose-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 израза у функцији.

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

Тренутни рад[уреди | уреди извор]

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

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

Однос са другим појмовима[уреди | уреди извор]

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

Референце[уреди | уреди извор]

General

Specific

Референце[уреди | уреди извор]

  1. ^ Nieuwenhuis, Robert; Oliveras, Albert; Tinelly, Cesar (2004), „Abstract DPLL and Abstract DPLL Modulo Theories” (PDF), Proceedings Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, стр. 36—50 
  2. ^ The international SAT Competitions web page, sat! live  Спољашња веза у |publisher= (помоћ)
  3. ^ zChaff website 
  4. ^ Chaff website 
  5. ^ „Minisat website”. 
  6. ^ doi:10.1007/3-540-48159-1_5
    This citation will be automatically completed in the next few minutes. You can jump the queue or expand by hand
  7. ^ 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. 

Литература[уреди | уреди извор]