A CDCL ( konfliktusvezérelt záradéktanulás ) algoritmus a DPLL-algoritmuson alapuló Boole-képletek (SAT-megoldó) kielégítési problémáinak hatékony ( NP-teljes ) megoldása. A CDCL-megoldók fő adatszerkezete egy implikációs gráf, amely rögzíti a változókhoz való hozzárendeléseket, és egy másik funkció a nem kronologikus visszakövetés és a konfliktuselemzés során történő emlékezés használata.
Az algoritmust João Marques -Silva és Karem A. Sakallah javasolta 1996-ban [ 1] és egymástól függetlenül Roberto J. Bayardo és Robert Schrag . Robert C. Schrag ) 1997-ben [2] [3] .
A CDCL-algoritmus alapjául szolgáló DPLL-algoritmus konjunktív normálformákon visszakövetést használ , amelynek minden lépésében kiválasztunk egy változót, és hozzárendelünk egy értéket (0 vagy 1) a következő elágazáshoz, ami abból áll, hogy egy változóhoz értéket rendelünk, majd egy egyszerűsített. A képlet megvalósíthatóságát rekurzívan tesztelik. Abban az esetben, ha ütközés történik , vagyis a kapott képlet nem megvalósítható, aktiválódik a visszatérési mechanizmus (visszalépés), amelyben törlődnek azok az ágak, amelyekben mindkét értéket megpróbálták a változóhoz. Ha a keresés visszatér egy első szintű elágazáshoz, akkor a teljes képlet nem teljesíthető . Az ilyen, a DPLL algoritmusban rejlő visszatérést kronologikusnak nevezzük [3] .
Az algoritmusban használt diszjunktokat elégedettre (kielégültre) osztjuk, ha a diszjunktban szereplő értékek között 1 van, elégedetlen (elégedetlen) - minden érték nulla, egyetlen (egység) - minden nulla, kivéve egy változó, amelyhez még nem rendeltek értéket, és feloldatlan - a többi. A SAT-megoldók egyik legfontosabb összetevője a single disjunkt rule , amelyben a változó kiválasztása és értéke egyértelmű. (Emlékeztetni kell arra, hogy a diszjunkt mind a változókat, mind a tagadásaikat tartalmazza . ) Az egységterjedési eljárást ( a modern CDCL-megoldókban szinte mindig az egyszeri diszjunkt szabályon alapszik) az elágazás után hajtjuk végre, hogy kiszámítsuk a választott választás logikai következményeit [ 3] .
A DPLL-n és annak visszakövetési mechanizmusán kívül a CDCL más trükköket is alkalmaz [3] :
Számos segédérték van társítva minden olyan változóhoz, amelyet a CDCL-algoritmusban ellenőriznek a képlet megvalósíthatósága szempontjából [3] :
Sematikusan egy tipikus CDCL-algoritmus a következőképpen ábrázolható [3] :
Algoritmus CDCL(φ, ν) bemenet: φ - képlet (CNF) ν - a változók értékeinek megjelenítése párok formájában kijárat: SAT (kielégíthető képlet) vagy UNSAT (nem kielégíthető) if UnitPropagationConflict(φ, ν) akkor UNSAT visszatérés L := 0 -- döntési szint while NotAllVariablesAssigned(φ, ν) (x, v) := PickBranchingVariable(φ, ν) -- döntéshozatal L := L + 1 ν := ν ∪ {(x, v)} if UnitPropagationConflict(φ, ν) -- kimeneti következmények akkor β := ConflictAnalysis(φ, ν) -- konfliktusdiagnosztika ha β < 0 akkor UNSAT visszatérés másképp Visszalépés(φ, ν, β) -- visszatérés (visszalépés) L := β SAT visszatérésEz az algoritmus több szubrutint használ, amelyek az értékek visszaadása mellett megváltoztathatják a nekik hivatkozással átadott φ, ν [3] változókat is :
A konfliktuselemzési eljárás központi szerepet játszik a CDCL algoritmusban.
A CDCL-megoldókban használt fő adatstruktúra egy implikációs gráf , amely a változókhoz való hozzárendeléseket rögzíti (mind a döntések eredményeként, mind a single disjunkt szabály alkalmazásával), amelyben a csúcsok a formulaliteráloknak, az ívek pedig az implikációk szerkezetét rögzítik [4 ] [5] .
A konfliktuselemzési eljárást (lásd az algoritmus diagramot) akkor hívjuk meg, ha az egytagmondat szabály szerint ütközést észlelünk, és ennek alapján pótoljuk a memorizált tagmondatokat. Az eljárás az implikációs gráf azon csomópontjától kezdődik, ahol az ütközést találták, és az alacsonyabb számokkal rendelkező döntési szinteken megy keresztül, visszafelé haladva az implikációkon, amíg nem találkozik a legutóbb hozzárendelt (a döntés eredményeként) változóval [3] . A memorizált tagmondatokat nem kronologikus visszakövetésben használják , ami egy másik, a CDCL -megoldókra jellemző technika [6] .
Összehasonlításképp:
DPLL : nincs tagmondat memorizálása, kronologikus visszatérés.
CDCL: záradékmemorizálás konfliktuselemzés és nem kronologikus visszalépés eredményeként
A konfliktushoz vezető implikációs struktúra használatának ötlete az UIP ( Eng. Unit Impplication Points – „egyszeri implikációs pontok”) használatára irányult. Az UIP az implikációs gráf domináns , amely lineáris időben számítható ki az ilyen típusú gráfokhoz. Az UIP egy alternatív változó-hozzárendelés, és az első ilyen ponton tárolt záradék garantáltan a legkisebb méretű lesz, és a legnagyobb megoldási szint csökkenést biztosítja. A hatékony lusta adatstruktúrák használatának köszönhetően számos SAT-megoldó szerzője, például Chaff, az első UIP-módszert alkalmazza a tagmondatok memorizálására ( első UIP-tagmondat tanulás ) [3] .
A DPLL -hez hasonlóan a CDCL algoritmus is egy helyes és teljes SAT-megoldó. Így a tagmondatok memorizálása nem befolyásolja a teljességet és a helyességet, hiszen a feloldási módszerrel minden betanult tagmondat levezethető a kezdeti tagmondatból és a többi memorizált tagmondatból . A megváltozott visszaküldési mechanizmus sem befolyásolja a teljességet és a helyességet, mivel a visszaküldésre vonatkozó információk a memorizált záradékban tárolódnak [3] .
Algoritmusművelet illusztráció:
Elágazási változó kiválasztása: x1 . A sárga kör önkényes döntést jelent.
A szinguláris záradékszabály szerint x4 - nek 1-nek kell lennie. A szürke kör kényszerített hozzárendelés. Az eredményül kapott gráf az implikációs gráf.
Egy másik változó tetszőleges választása, x3 .
Az egységzáradék-szabály alkalmazása és új implikációs gráf keresése.
Az x8 és x12 változók logikailag 0 és 1 értéket vesznek fel.
Elágazási változó kiválasztása ismét: x2 .
Implikációs gráf felépítése.
Egy másik változó: x7 .
Implikációs gráf felépítése.
Új implikációs grafikon. Kapott egy konfliktus .
A konfliktushoz vezető grafikon metszésének és a konfliktuszáradéknak a megkeresése .
Disjunkt keresése tagadással: ha a-ból b következik , akkor nem-b- ből nem -a következik
Emlékezés a disjunkcióra.
Nem kronologikus visszatérés a megfelelő döntési szintre.
Megfelelő beállítási értékek.
A CDCL algoritmuson alapuló SAT-megoldók alkalmazást találnak automatikus tételbizonyításban , kriptográfiában , hardver- és szoftvermodell- ellenőrzésben és -tesztelésben, bioinformatikában , függőségek meghatározásában a csomagkezelő rendszerekben stb. [3]