Az informatikában a konfliktusvezérelt klóztanulás (CDCL) a logikai kielégítési probléma (SAT) megoldására szolgáló algoritmus. Adott egy logikai képlet, a SAT-probléma változók hozzárendelését kéri, hogy a teljes képlet igaz legyen. A CDCL SAT megoldók belső működését a DPLL megoldók ihlették. A fő különbség a CDCL és a DPLL között az, hogy a CDCL visszaugrása nem kronologikus.
A konfliktusvezérelt klózok tanulását Marques-Silva és Sakallah (1996, 1999), valamint Bayardo és Schrag (1997) javasolta.
Háttér
Logikai kielégítési probléma
A kielégítési probléma abban áll, hogy egy adott képlethez megfelelő hozzárendelést találunk konjunktív normál formában (CNF).
( ( nem A ) vagy ( nem C ) ) és ( B vagy C ),
vagy egy általános jelöléssel:In the pictures below, "" is used to denote "or", multiplication to denote "and", and a postfix "" to denote "not".
ahol A, B, C logikai változók, , , , és litárlok, és és klózok.
mivel igazzá teszi az első klózt (hiszen igaz), valamint a másodikat (mivel igaz).
Ez a példa három változót használ ( A, B, C ), és mindegyikhez két lehetséges hozzárendelés (igaz és hamis) van. Tehát az egyiknek van lehetősége. Ebben a kis példában a brute-force keresést használhatjuk az összes lehetséges hozzárendelés kipróbálásához, és ellenőrizhetjük, hogy megfelelnek-e a képletnek.
De realisztikus alkalmazásokban, amelyekben milliónyi változó és klóz található, a brute force keresés nem praktikus. A SAT-megoldó feladata, hogy hatékonyan és gyorsan megtalálja a kielégítő feladatot összetett CNF-képletek különböző heurisztikáinak alkalmazásával.
Unit klóz szabály (unit propagáció vagy egységterjesztés) Ha egy nem kielégítő klóznak egy kivételével minden literálja vagy változója Hamis értékkel van kiértékelve, akkor a szabad literálnak igaznak kell lennie ahhoz, hogy a klóz igaz legyen. Például, ha az alábbi nem kielégítő klózt a következővel értékeljük ki és nekünk kell hogy legyen a klóz érdekében hogy igaz legyen.
A unit klóz szabály iterált alkalmazását unit propagációnak vagy Boole-kényszer-propagációnak (BCP) nevezik.
Rezolúció Vegyünk két kitételt és . A klóz , amelyet a két klóz egyesítésével és mindkettő eltávolításával kapunk és , a két klóz oldójának nevezzük.
Algoritmus A konfliktus-vezérelt klózok tanulása a következőképpen működik.
Válasszon ki egy változót, és rendelje hozzá az igaz vagy hamis értéket. Ezt döntési állapotnak nevezik. Emlékezzen a feladatra. Alkalmazza a logikai kényszer propagációt (unit propagáció). Építsd meg az implikációs gráfot. Ha bármilyen konfliktus van Keresse meg az implikációs grafikonon azt a vágást, amely az ütközéshez vezetett Hozz létre egy új klózt, amely a konfliktushoz vezető hozzárendelések tagadása Nem kronologikusan visszalépni ("visszaugrás") a megfelelő döntési szintre, ahol az elsőként hozzárendelt, a konfliktusban érintett változót hozzárendelték Ellenkező esetben folytassa az 1. lépéstől, amíg az összes változóértéket hozzá nem rendeli.
Példa A CDCL algoritmus vizuális példája:In the pictures below, "" is used to denote "or", multiplication to denote "and", and a postfix "" to denote "not".
Teljesség A DPLL egy megbízható és teljes algoritmus a SAT számára. A CDCL SAT megoldói megvalósítják a DPLL-t, de megtanulhatnak új klózokat, és nem kronologikusan léphetnek vissza. A konfliktuselemzéssel végzett klóztanulás nem befolyásolja sem a megalapozottságot, sem a teljességet. Az új klózokat feloldási művelettel azonosítja az ütközéselemzés. ezért minden egyes tanult klóz kikövetkeztethető az eredeti klózból és a többi tanult klózból a feloldási szekvencia sorozatával. Ha cN az új tanult klóz, akkor ϕ akkor és csak akkor teljesíthető, ha ϕ ∪ {cN} is kielégíthető. Ezen túlmenően a módosított backtrack lépés sem befolyásolja a megbízhatóságot vagy a teljességet, mivel a visszalépési információkat minden új tanult klózból kapjuk.
Alkalmazások A CDCL algoritmus fő alkalmazása a különböző SAT-megoldókban található, beleértve:
MiniSAT Zchaff SAT Z3 Glükóz ManySAT stb.
A CDCL algoritmus annyira erőssé tette a SAT-megoldókat, hogy számos alkalmazási területen alkalmazzák hatékonyan a gyakorlatban, mint például a mesterséges intelligencia tervezése, bioinformatika, szoftverteszt-minta generálása, szoftvercsomag-függőségek, hardver- és szoftvermodell-ellenőrzés és kriptográfia.
Kapcsolódó algoritmusok A CDCL-hez kapcsolódó algoritmusok a Davis–Putnam-algoritmus és a DPLL algoritmus. A DP algoritmus rezolúció cáfolatokat használ, és lehetséges memóriaelérési problémája van. Míg a DPLL algoritmus megfelelő a véletlenszerűen generált példányokhoz, rossz a gyakorlati alkalmazásokban generált példányokhoz. A CDCL hatékonyabb megoldás az ilyen problémák megoldására, mivel a CDCL alkalmazása kevesebb állapottér-keresést biztosít a DPLL-hez képest.
Jegyzetek
Fordítás
Források
Presentation – "SAT-Solving: From Davis-Putnam to Zchaff and Beyond" by Lintao Zhang. (Several pictures are taken from his presentation)
Kategória:Algoritmusok Kategória:NP-teljes problémák