DPLL

DPLL ( Davis-Putnam-Logeman-Loveland algorithm ) je kompletní backtrackingový algoritmus pro řešení problému CNF-SAT  - určování splnitelnosti booleovských vzorců zapsaných v konjunktivní normální formě .

Publikoval v roce 1962 Martin Davis , Hilary Putnam , George Logeman a Donald Loveland jako vylepšení dřívějšího Davis-Putnamova algoritmu založeného na pravidle rozlišení .

Jedná se o vysoce účinný algoritmus, který zůstává relevantní i po půl století a používá se ve většině SAT řešitelů a systémů automatického důkazu pro fragmenty logiky prvního řádu [1] .

Implementace a aplikace

Problém splnitelnosti booleovských vzorců je důležitý z teoretického i praktického hlediska. V teorii složitosti je to první problém, pro který bylo prokázáno členství ve třídě NP-úplných problémů . Může se také objevit v široké řadě praktických aplikací, jako je kontrola modelu , plánování a diagnostika.

Tato oblast byla a stále je rostoucí oblastí výzkumu, každoročně se konají soutěže mezi různými řešiteli SAT [2] ; moderní implementace algoritmu DPLL, jako je Chaff , zChaff [3] [4] , GRASP a Minisat [5] , zaujímají první místo v takových soutěžích.

Dalším typem aplikace, ve které se DPLL často používá, jsou systémy pro dokazování teorémů .

Popis algoritmu

Základní algoritmus zpětného sledování začíná výběrem proměnné, jejím nastavením na hodnotu true, zjednodušením vzorce a poté rekurzivním testováním zjednodušeného vzorce na proveditelnost; pokud je to proveditelné, pak je proveditelný i původní vzorec; jinak se postup opakuje, ale vybraná proměnná je nastavena na hodnotu false. Tento přístup se nazývá „pravidlo rozdělení“, protože rozděluje úlohu do dvou jednodušších dílčích úloh. Krok zjednodušení spočívá v odstranění všech klauzulí ze vzorce, které se stanou pravdivými po přiřazení hodnoty "true" vybrané proměnné, a odstranění všech výskytů této proměnné, které se stanou nepravdivými, ze zbývajících klauzulí.

Algoritmus DPLL vylepšuje základní algoritmus zpětného sledování pomocí následujících pravidel v každém kroku:

Variabilní šíření pokud klauzule obsahuje právě jednu proměnnou, které ještě nebyla přiřazena hodnota, může se tato klauzule stát pravdivou pouze tehdy, je-li proměnné přiřazena hodnota, která ji činí pravdivou (pravda, pokud je proměnná v klauzuli bez negace, a nepravda, pokud proměnná je negativní). V tomto kroku tedy není třeba provádět výběr. V praxi na to navazuje kaskáda přiřazení k proměnným, čímž se výrazně snižuje počet možností iterace. Vyloučení "čistých" proměnných pokud nějaká proměnná vstupuje do vzorce pouze s jednou "polaritou" (tedy buď pouze bez negací, nebo pouze s negacemi), nazývá se čistá . "Čisté" proměnné mohou mít vždy takovou hodnotu, že všechny klauzule, které je obsahují, se stanou pravdivými. Tyto doložky tedy neovlivní prostor variant a lze je odstranit.

Nesplnitelnost pro dané konkrétní hodnoty proměnných je definována, když se jedna z klauzulí stane „prázdnou“, to znamená, že všem jejím proměnným jsou dány hodnoty takovým způsobem, že jejich výskyty (s nebo bez negace) se stanou nepravdivé. Splnitelnost vzorce je uvedena buď tehdy, když jsou všechny proměnné nastaveny na hodnoty, takže neexistují žádné "prázdné" klauzule, nebo v moderních implementacích, pokud jsou všechny klauzule pravdivé. Nesplnitelnost celého vzorce lze konstatovat až po skončení vyčerpávajícího výčtu.

Algoritmus DPLL lze vyjádřit pomocí následujícího pseudokódu, kde Φ označuje vzorec v konjunktivní normální formě:

Vstupní data: Soubor klauzulí vzorce Φ. Výstup: Pravdivá hodnota funkce DPLL(Φ) , pokud Φ je množina spustitelných klauzulí , vrátí hodnotu true; pokud Φ obsahuje prázdnou klauzuli, pak vrátí false; pro každou klauzuli z jedné proměnné l až Φ Φ šíření jednotek ( l , Φ); pro každou proměnnou l , která se vyskytuje v čisté formě v Φ Φ čistý-doslovný-přiřadit ( l , Φ); l zvolit-literál (Φ); návrat DPLL (Φ&l) nebo DPLL (Φ¬(l));

V tomto pseudokódu unit-propagate(l, Φ)a pure-literal-assign(l, Φ) jsou funkce, které vracejí výsledek použití na proměnnou la vzorec šíření proměnné Φa pravidlo vyloučení "čisté proměnné". Jinými slovy nahrazují každý výskyt proměnné hodnotou ltrue a každý výskyt negované proměnné hodnotou not lfalse ve vzorci Φa výsledný vzorec pak zjednodušují. Výše uvedený pseudokód vrací pouze odpověď - zda poslední z přiřazených sad hodnot splňuje vzorec. V moderních implementacích se s úspěchem vracejí i dílčí exekuční sady.

Algoritmus závisí na volbě "větvené proměnné", tj. proměnné, která je vybrána v dalším kroku algoritmu s návratem. přiřadit mu konkrétní hodnotu. Nejedná se tedy o jeden algoritmus, ale o celou rodinu algoritmů, jeden pro každý možný způsob výběru „větvených proměnných“. Účinnost algoritmu silně závisí na této volbě: existují příklady problémů, u kterých může být doba běhu algoritmu konstantní nebo může exponenciálně růst v závislosti na volbě „větvených proměnných“. Metody výběru jsou heuristické techniky a nazývají se také „heuristiky větvení“ [6] .

Současný výzkum

Současný výzkum zaměřený na zlepšení algoritmu se provádí ve třech směrech: definování různých optimalizačních metod pro výběr "větvené proměnné"; vývoj nových datových struktur pro urychlení algoritmu, zejména pro variabilní šíření; a vývoj různých variant základního backtrackingového algoritmu. Posledním směrem je „nechronologický backtracking“ a vzpomínání na špatné případy . Tato vylepšení lze popsat jako metodu návratu po dosažení nepravdivé klauzule, ve které je zapamatováno, které konkrétní přiřazení hodnoty proměnné způsobilo tento výsledek, aby se předešlo přesně stejné posloupnosti výpočtů v budoucnu, čímž se sníží pracovní doba.

Od roku 1990 je znám novější algoritmus, metoda Stalmark. Také od roku 1986 se k řešení problému SAT používají rozhodovací diagramy.

Algoritmus CDCL založený na algoritmu DPLL byl vytvořen v polovině 90. let a stal se široce používaným .

Poznámky

  1. ↑ Nieuwenhuis, Robert; Oliveras, Albert & Tinelly, Cesar (2004), Abstract DPLL and Abstract DPLL Modulo Theories , Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, Proceedings : 36–50 , < http://www.lsi.upc.edu /~roberto/papers/lpar04.pdf > Archivováno 17. listopadu 2011 na Wayback Machine 
  2. ↑ Mezinárodní webová stránka soutěží SAT , so! live , < http://www.satcompetition.org/ > Archivováno 12. února 2005 na Wayback Machine 
  3. ↑ Web zChaff , < http://www.princeton.edu/~chaff/zchaff.html > Archivováno 19. dubna 2017 na Wayback Machine 
  4. ↑ Web Chaff , < http://www.princeton.edu/~chaff/ > Archivováno 23. února 2020 na Wayback Machine 
  5. ↑ Web Minisat . Archivováno z originálu 20. dubna 2012.
  6. ↑ Marques-silva, Joao. Vliv větvené heuristiky v algoritmech propositional satisfiability algorithms  (anglicky)  // In 9th Portuguese Conference on Artificial Intelligence (EPIA) : journal. - 1999. - doi : 10.1.1.111.9184 . Archivováno z originálu 14. dubna 2012.

Literatura