DPLL

A DPLL ( Davis-Putnam- Logeman -Loveland algoritmus ) egy komplett visszakövető algoritmus a CNF-SAT probléma megoldására - konjunktív normál formában  írt Boole-képletek kielégíthetőségének meghatározására .

1962 -ben tette közzé Martin Davis , Hilary Putnam , George Logeman [ és Donald Loveland a korábbi Davis-Putnam algoritmus továbbfejlesztéseként, amely a felbontási szabályon alapul .

Ez egy rendkívül hatékony algoritmus, és fél évszázad után is releváns marad, és a legtöbb SAT -megoldóban és az elsőrendű logika töredékeinek automatikus ellenőrző rendszerében használják [1] .

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

A Boole-képletek kielégíthetőségének problémája elméleti és gyakorlati szempontból egyaránt fontos. A komplexitáselméletben ez az első olyan probléma, amelynél az NP-teljes problémák osztályába való tartozás bizonyított . Számos gyakorlati alkalmazásban is megjelenhet, például modellellenőrzésben , ütemezésben és diagnosztikában.

Ez a terület a kutatások egyre növekvő területe volt és továbbra is az, évente versenyeket rendeznek a különböző SAT-megoldók között [2] ; a DPLL algoritmus modern implementációi, mint például a Chaff [ , zChaff [3] [4] , GRASP és Minisat [5] , első helyezést értek el az ilyen versenyeken.

Egy másik alkalmazástípus, amelyben a DPLL-t gyakran használják, a tételbizonyító rendszerek .

Az algoritmus leírása

Az alapvető visszakövetési algoritmus a változó kiválasztásával, igaz értékre állításával, a képlet egyszerűsítésével, majd az egyszerűsített képlet megvalósíthatóságának rekurzív tesztelésével kezdődik; ha megvalósítható, akkor az eredeti képlet is megvalósítható; ellenkező esetben az eljárás megismétlődik, de a kiválasztott változó false értékre van állítva. Ezt a megközelítést "felosztási szabálynak" nevezik, mert két egyszerűbb részfeladatra bontja a feladatot. Az egyszerűsítés lépése abból áll, hogy eltávolítjuk a képletből az összes olyan tagmondatot, amely igazzá válik, miután a kiválasztott változóhoz „true” értéket rendeltünk, és eltávolítjuk a többi tagmondatból a változó hamissá váló összes előfordulását.

A DPLL algoritmus minden lépésben a következő szabályokat alkalmazva javítja az alapvető visszakövetési algoritmust:

Változó terjedés ha egy tagmondat pontosan egy olyan változót tartalmaz, amelyhez még nem rendeltek értéket, akkor ez a záradék csak akkor válhat igazzá, ha a változóhoz olyan értéket rendelünk, amely igazzá teszi (igaz, ha a változó tagadás nélkül szerepel a klózban, és hamis, ha a változó negatív). Így ebben a lépésben nem kell választani. A gyakorlatban ezt a változókhoz való hozzárendelések kaszkádja követi, így jelentősen csökken az iterációs lehetőségek száma. A "tiszta" változók kizárása ha valamilyen változó csak egy "polaritással" lép be a képletbe (vagyis vagy csak tagadások nélkül, vagy csak tagadással), akkor tiszta . A "tiszta" változóknak mindig olyan értéket adhatunk, hogy minden, azokat tartalmazó tagmondat igaz legyen. Így ezek a záradékok nem befolyásolják a változatok terét, és eltávolíthatók.

Adott változóértékek ki nem elégíthetőségét akkor határozzuk meg, amikor az egyik záradék „üres” lesz, vagyis minden változója értéket kap úgy, hogy előfordulása (tagsággal vagy anélkül) hamis lesz. A képlet kielégíthetősége akkor van megadva, ha minden változó értékre van állítva, hogy ne legyenek "üres" záradékok, vagy a modern megvalósításokban, ha minden kitétel igaz. A teljes képlet kielégíthetetlensége csak a kimerítő felsorolás befejezése után állapítható meg.

A DPLL algoritmus a következő pszeudokóddal fejezhető ki, ahol Φ egy konjunktív normál formában lévő képletet jelöl:

Bemenő adatok: Φ képletű tagmondatok halmaza. Kimenet: Igazságérték függvény DPLL(Φ) , ha Φ a végrehajtható tagmondatok halmaza, akkor igazat ad vissza ; ha Φ üres záradékot tartalmaz, akkor a false értéket adja vissza ; minden tagmondatnál egy l változótól Φ-ig Φ egység-szaporodás ( l , Φ); minden l változóra , amely tiszta formában fordul elő Φ-ben Φ tiszta-literal-hozzárendelés ( l , Φ); l select-literal (Φ); visszaküldi a DPLL-t (Φ&l) vagy DPLL-t (Φ¬(l));

Ebben a pszeudokódban unit-propagate(l, Φ), és pure-literal-assign(l, Φ) olyan függvények, amelyek egy változóra való alkalmazás eredményét adják vissza, lilletve egy változóterjesztési képlet Φ, illetve egy „tiszta változó” kizárási szabály. Más szóval, a képletben egy változó lminden előfordulását igazra, a negált változó minden előfordulását not lhamisra cserélik Φ, majd egyszerűsítik a kapott formulát. A fenti pszeudokód csak választ ad vissza - hogy a hozzárendelt értékkészletek közül az utolsó teljesíti-e a képletet. A modern megvalósításokban a részleges végrehajtási készletek is megtérülnek a sikeren.

Az algoritmus egy "ági változó" megválasztásától függ, vagyis egy olyan változótól, amely az algoritmus következő lépésében kerül kiválasztásra, visszatéréssel. hogy konkrét értéket rendeljünk hozzá. Így nem egy algoritmusról van szó, hanem egy egész algoritmus-családról, egyet-egyet az „ágváltozók” kiválasztásának minden lehetséges módjához. Az algoritmus hatékonysága erősen függ ettől a választástól: vannak példák olyan problémákra, amelyeknél az algoritmus futási ideje állandó, vagy exponenciálisan nőhet, attól függően, hogy melyik „ágváltozót” választjuk. A kiválasztási módszerek heurisztikus technikák, és "elágazási heurisztikának" is nevezik [6] .

Kortárs kutatás

Az algoritmus fejlesztését célzó jelenlegi kutatások három irányban zajlanak: különféle optimalizálási módszerek meghatározása az „elágazási változó” kiválasztásához; új adatstruktúrák fejlesztése az algoritmus felgyorsítása érdekében, különösen változó terjedés esetén; és az alapvető visszakövetési algoritmus különféle változatainak fejlesztése. Az utolsó irány a "nem kronologikus visszalépés" és a rossz esetekre való emlékezés . Ezeket a fejlesztéseket úgy írhatjuk le, mint egy hamis záradék elérése utáni visszatérési módszert, amelyben megjegyezzük, hogy egy adott változóhoz adott érték hozzárendelése okozta ezt az eredményt, hogy elkerüljük a pontosan ugyanazt a számítási sorozatot a jövőben, ezáltal csökkentve munkaidő.

1990 óta ismert egy újabb algoritmus, a Stalmark-módszer. Szintén 1986 óta használnak döntési diagramokat a SAT probléma megoldására.

A DPLL-algoritmuson alapuló CDCL- algoritmust az 1990-es évek közepén hozták létre, és széles körben elterjedt .

Jegyzetek

  1. ↑ Nieuwenhuis, Robert; Oliveras, Albert és 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 > Archiválva : 2011. november 17. a Wayback Machine -nél 
  2. ↑ A nemzetközi SAT Competitions weboldal , szo! élő , < http://www.satcompetition.org/ > Archiválva 2005. február 12-én a Wayback Machine -nél 
  3. ↑ zChaff webhely , < http://www.princeton.edu/~chaff/zchaff.html > Archiválva : 2017. április 19. a Wayback Machine -nél 
  4. ↑ Chaff webhely , < http://www.princeton.edu/~chaff/ > Archivált : 2020. február 23. a Wayback Machine -nél 
  5. ↑ Minisat webhely . Az eredetiből archiválva: 2012. április 20.
  6. ↑ Marques-silva, Joao. Az elágazó heurisztikák hatása a propozíciós kielégítési algoritmusokban  (angol)  // In 9th Portuguese Conference on Artificial Intelligence (EPIA) : folyóirat. - 1999. - doi : 10.1.1.111.9184 . Archiválva az eredetiből 2012. április 14-én.

Irodalom