DPLL algoritmus

 

DPLL
5 eredménytelen (piros) kísérlet után az a=1, b=1 változó-hozzárendelés kiválasztása, az unitpropagáció után (alul)(zöld) ): a bal felső CNF képlet kielégíthető.
Kategória	Boolean satisfiability problem
Adatstruktúra	Bináris fa
Legrosszabb időbonyolultság	$O(2^{n})$
Legjobb időbonyolultság	$O(1)$ (állandó)
Legrosszabb tár bonyolultság	$O(n)$ (alap algoritmus)

A logikában és az informatikában a Davis–Putnam–Logemann–Loveland (DPLL)-algoritmus egy teljes, visszalépésen (backtrack) alapuló keresőalgoritmus az ítéletlogikai formulák konjunktív normál formában való kielégíthetőségének eldöntésére, azaz a CNF-SAT probléma megoldására.

Ezt az algoritmust Martin Davis, George Logemann és Donald W. Loveland vezette be 1961-ben, a korábbi Davis-Putnam-algoritmust fejlesztették; a Davis és Hilary Putnam által 1960-ban kifejlesztett rezolúció alapú eljárás volt. Különösen a régebbi publikációkban a Davis–Logemann–Loveland-algoritmust gyakran „Davis–Putnam-módszernek” vagy „DP-algoritmusnak” nevezték. Egyéb gyakori nevek, amik segítik a megkülönböztetést a DLL és a DPLL.

Megvalósítások és alkalmazások

A SAT probléma egyaránt fontos mind elméleti, mind megvalósítási szempontból. A komplexitáselméletben ez volt az első probléma, amely NP-teljesnek bizonyult, és számos alkalmazásban megjelenhet, mint például a modellellenőrzés, az automatizált tervezés és ütemezés, valamint a mesterséges intelligencia diagnosztikája.

A hatékony SAT-megoldók írása évek óta kutatási téma. A GRASP (1996-1999) a DPLL algoritmust használó korai megvalósítója volt. A nemzetközi SAT versenyeken 2004-ben és 2005-ben a DPLL-re épülő implementációk, például a ZChaff és a MiniSat voltak az első helyezettek a versenyeken.

Egy másik alkalmazás, amely gyakran magában foglalja a DPLL-t, az automatizált tételbizonyítási vagy más néven a SAT modulo elméletek (SMT). Ez egy olyan SAT probléma, ahol a logikai változókat egy másik matematikai elmélet képleteivel helyettesítik.

Az algoritmus

Az alapvető visszalépési (backtrack) algoritmus úgy fut le, hogy kiválaszt egy literált, amihez hozzárendel egy valós értéket, leegyszerűsíti ezáltal a képletet, majd rekurzívan ellenőrzi azt, hogy az egyszerűsített képlet kielégítő-e; ha megfelelő a helyzet, akkor az eredeti képlet kielégítő; ellenkező esetben ugyanazt a rekurzív ellenőrzést végezzük el az ellenkező valós értéket feltételezve.

Ezt felosztási szabálynak nevezik, mivel a problémát két egyszerűbb részproblémára bontja. Az egyszerűsítési lépés lényegében eltávolítja a képletből az összes olyan tagmondatot, amely igazzá válik a hozzárendelés során, és minden olyan literált, amely hamissá válik a többi tagmondatból.

A DPLL algoritmus javítja a visszalépési algoritmust azáltal, hogy minden lépésben a következő szabályokat használja:

Unit propagáció (egységterjesztés más fordításban)

Ha egy tagmondat unitklóz, azaz csak egyetlen hozzá nem rendelt literált tartalmaz, akkor ez a klóz csak úgy teljesíthető, ha a literál igazzá tételéhez szükséges értéket rendeljük hozzá. Így nincs szükség választásra. Az unit propagáció abból áll, hogy eltávolítunk minden tagmondatot, amely tartalmazza az unitklóz literálját, és eldobjuk az unitklóz literáljának komplementerét minden, ezt a kiegészítést tartalmazó tagmondattól. A gyakorlatban ez gyakran az unitok determinisztikus kaszkádjához vezet, így elkerülhető a naiv keresési tér nagy része.

Tiszta literál elimináció

Ha egy logikai változó csak egy polaritással fordul elő a képletben, akkor tisztának nevezzük. A tiszta literál mindig hozzárendelhető oly módon, hogy az azt tartalmazó kitétel igaz legyen. Így, ha ilyen módon van hozzárendelve, ezek a klózok már nem korlátozzák a keresést, és törölhetők.

Egy adott hozzárendelés részleges ki nem elégíthetősége akkor észlelhető, ha egy klóz üres lesz, azaz ha az összes változóját úgy rendelték hozzá, hogy a megfelelő literálok hamisak legyenek. A képlet kielégíthetősége akkor észlelhető, ha az összes változót üres klóz generálása nélkül hozzárendeljük, vagy a modern megvalósításokban, ha minden klóz teljesül. A teljes képlet kielégíthetetlensége csak kimerítő keresés után deríthető ki.

A DPLL algoritmus a következő pszeudokódban foglalható össze, ahol Φ a CNF (konjunktív normálforma) képlet:

   

DPLL Algoritmus
     Input: Φ tagmondatok halmaza.
     Output: A valós érték amely jelzi, hogy Φ teljesíthető-e.

 függvény DPLL(Φ)
     // unit propagáció:
      while van egy {l} unit klóz a Φ do-ban
          Φ ← unit-propagácó(l, Φ);
      // tiszta literál elimináció:
      amíg van tiszta literál l, amely tisztán fordul elő Φ 'do
          Φ ← tiszta-literális-hozzárendelés(l, Φ);
      // leállási feltételek:
      'ha' Φ üres 'akkor
          return igaz;
      'if' Φ egy üres klózt tartalmaz 'akkor'
          return false;
      // DPLL eljárás:
      l ← elágazó literál választása(Φ);
      return DPLL(Φ ∧ {l}) vagy DPLL(Φ ∧ {¬l} );
      
     // A „←” hozzárendelést jelöl. Például a "legnagyobb ← elem" azt jelenti, hogy a legnagyobb értéke megváltozik az elem értékéhez képest.
     // A "return" leállítja az algoritmust, és a következő értéket adja ki.

Ebben a pszeudokódban unit-propagáció(l, Φ) és tiszta literál hozzárendelés(l, Φ) olyan függvények, amelyek az unit propagáció és a tiszta literális szabály alkalmazásának eredményét adják vissza az l literálra és a Φ képletre. Más szóval, a Φ képletben l minden előfordulását "igaz"-ra, not l minden előfordulását "hamis"-ra cserélik, és egyszerűsítik a kapott formulát. A vagy a return utasításban egy rövidzárlati operátor. Φ ∧ {l} azt az egyszerűsített eredményt jelöli, amikor l "igaz"-val helyettesítünk Φ -ben.

Az algoritmus két eset közül az egyikben véget ér. Vagy a Φ CNF képlet üres, azaz nem tartalmaz klózt. Ekkor minden hozzárendelést kielégít, mivel minden tagmondata kimondottan igaz. Ellenkező esetben, ha a képlet üres tagmondatot tartalmaz, a klóz egyértelműen hamis, mivel a diszjunkcióhoz legalább egy olyan tagra van szükség, amely igaz ahhoz, hogy a teljes halmaz igaz legyen. Ebben az esetben egy ilyen klóz megléte azt jelenti, hogy a formula (az összes tagmondat kötőszójaként értékelve) nem értékelhető igazra, és nem teljesíthető.

A pszeudokód DPLL függvény csak akkor ad vissza, ha a végső hozzárendelés megfelel a képletnek, vagy sem. Valós megvalósításban a részleges kielégítő feladat is jellemzően sikerrel jár vissza; ez az elágazó literálok és az unit propagáció és a tiszta literális elimináció során végzett literál-hozzárendelések nyomon követésével származtatható.

A Davis–Logemann–Loveland-algoritmus az elágazó literál megválasztásától függ, amely a visszalépési (backtrack) lépésben figyelembe vett literál. Ennek eredményeként ez nem pontosan egy algoritmus, hanem egy algoritmuscsalád, amely az elágazó literál kiválasztásának minden lehetséges módjához tartozik. A hatékonyságot erősen befolyásolja az elágazó literál megválasztása: vannak olyan esetek, amelyeknél a futási idő állandó vagy exponenciális az elágazó literálok megválasztásától függően. Az ilyen választási függvényeket heurisztikus függvényeknek vagy elágazó heurisztikának is nevezik.

Szemléltetés

Davis, Logemann, Loveland (1961) dolgozta ki ezt az algoritmust, amit DLL-nek neveztek el. Ennek az eredeti algoritmusnak néhány tulajdonsága:

• Keresésen alapul.
• Szinte minden modern SAT-megoldó alapja.
• Nem használ tanulást vagy nem kronologikus visszalépést (1996-ban vezették be).

Példa egy időrendi visszalépéssel rendelkező DPLL-algoritmus megjelenítésére:

• 
  Minden klóz, amely CNF formulát alkot.
• 
  Változó választása
• 
  Döntéshozatal, változó a = Hamis (0), így a zöld klózok igazak lesznek
• 
  Több döntés meghozatala után találunk egy implikációs gráfot, amely konfliktushoz vezet.
• 
  Visszalépés az azonnali szintre, és rákényszeríti hogy ellentétes értéket rendeljen a változóhoz
• 
  De a kényszerített döntés még mindig ütközéshez vezet
• 
  Backtrack egy korábbi szintre és döntés kényszerítés
• 
  Új döntés meghozása még mindig ütközéshez vezet
• 
  Kényszerített döntés, de ez is ütközéshez vezet
• 
  Backtrack (visszalépés) korábbi szintre
• 
  Folytassa így a végső implikációs grafikonig

Kapcsolódó algoritmusok

A SAT megoldására 1986 óta a (csökkenő sorrendben) a bináris döntési diagramokat is használják.

1989-1990-ben bemutatták és szabadalmaztatták Stålmarck képletellenőrzési módszerét, ami csak némi ipari alkalmazásokban lett felhasználva.

A DPLL algoritmust kibővítették az elsőrendű logika töredékeinek automatikus tételbizonyítására a DPLL(T) algoritmus segítségével.

A 2010–2019-es évtizedben az algoritmus javításán végzett munka során jobb házirendeket találtak az elágazó literálok kiválasztásához, és új adatstruktúrákat találtak az algoritmus gyorsabbá tétele érdekében, különösen az egységnyi propagációre vonatkozó részt. A fő fejlesztés azonban egy erősebb algoritmus, a Conflict-Driven Clause Learning (CDCL), amely hasonló a DPLL-hez, de az ütközés elérése után „megtanulja” a konfliktus kiváltó okait (változókhoz való hozzárendelését), és felhasználja ezt az információt. nem kronologikus visszalépés (backjumping ) végrehajtása annak érdekében, hogy ne érje el újra ugyanazt a konfliktust. A legtöbb legkorszerűbb SAT-megoldó 2019-től a CDCL-keretrendszeren alapul

Más fogalmakkal való kapcsolat

A DPLL-alapú algoritmusok nem kielégítő példányokon való futtatása megfelel a fafelbontású cáfolatbizonyításoknak.

Hivatkozások

Általános

• Davis (1960). „A Computing Procedure for Quantification Theory”. Journal of the ACM 7 (3), 201–215. o. DOI:10.1145/321033.321034. 
• Davis (1961). „A Machine Program for Theorem Proving”. Communications of the ACM 5 (7), 394–397. o. DOI:10.1145/368273.368557. 
• Ouyang (1998). „How Good Are Branching Rules in DPLL?”. Discrete Applied Mathematics 89 (1–3), 281–286. o. DOI:10.1016/S0166-218X(98)00045-6. 
• John Harrison. Handbook of practical logic and automated reasoning. Cambridge University Press, 79–90. o. (2009). ISBN 978-0-521-89957-4 

Fordítás

Ez a szócikk részben vagy egészben a DPLL algorithm című angol Wikipédia-szócikk ezen változatának fordításán alapul. Az eredeti cikk szerkesztőit annak laptörténete sorolja fel. Ez a jelzés csupán a megfogalmazás eredetét és a szerzői jogokat jelzi, nem szolgál a cikkben szereplő információk forrásmegjelöléseként.

További irodalom

• Malay Ganai. SAT-based scalable formal verification solutions. Springer, 23–32. o. (2007). ISBN 978-0-387-69166-4 
• Gomes, Carla P..szerk.: Van Harmelen: Satisfiability Solvers, Handbook of knowledge representation, Foundations of Artificial Intelligence. Elsevier, 89–134. o.. DOI: 10.1016/S1574-6526(07)03002-7 (2008). ISBN 978-0-444-52211-5