Algoritmus CDCL ( conflic -driven clause learning ) je účinným řešitelem ( NP-complete ) problémů splnitelnosti pro booleovské vzorce (SAT solver) založený na algoritmu DPLL . Hlavní datovou strukturou v řešičích CDCL je implikační graf, který zachycuje přiřazení k proměnným, a další funkcí je použití nechronologického zpětného sledování a zapamatování si klauzulí během analýzy konfliktů.
Algoritmus navrhli João Marques - Silva a Karem A. Sakallah v roce 1996 [ 1] a nezávisle Roberto J. Bayardo a Robert Schrag ( Robert C. Schrag ) v roce 1997 [2] [3] .
Algoritmus DPLL, který je základem algoritmu CDCL, používá backtracking na konjunktivních normálních formách , v každém kroku je vybrána proměnná a je jí přiřazena hodnota (0 nebo 1) pro následné větvení, které spočívá v přiřazení hodnoty proměnné, po které následuje zjednodušený vzorec je rekurzivně testován na proveditelnost. V případě, že dojde ke konfliktu , to znamená, že výsledný vzorec není proveditelný, je aktivován návratový mechanismus (backtracking), ve kterém jsou zrušeny větve, ve kterých byly pro proměnnou vyzkoušeny obě hodnoty. Pokud se hledání vrátí do větve první úrovně, celý vzorec je prohlášen za nesplnitelný . Takový návrat, který je vlastní algoritmu DPLL, se nazývá chronologický [3] .
Disjunkty použité v algoritmu se dělí na splněné (spokojené), kdy mezi hodnotami zahrnutými v disjunktě je 1, nespokojené (nesplněné) - všechny hodnoty jsou nulové, jednoduché (jednotka) - všechny nuly, kromě jedné proměnná, které ještě nebyla přiřazena hodnota, a nevyřešená - vše ostatní. Jednou z nejdůležitějších součástí SAT řešitelů je jediné disjunktní pravidlo , ve kterém je volba proměnné a její hodnoty jednoznačná. (Je třeba připomenout, že disjunkt zahrnuje obě proměnné a jejich negace . ) Procedura šíření jednotek ( v moderních řešičích CDCL je téměř vždy založena na pravidle jediného disjunktu) se provádí po větvení, aby se vypočítaly logické důsledky provedené volby [ 3] .
Kromě DPLL a jeho backtracking mechanismu používá CDCL některé další triky [3] :
S každou proměnnou, která je kontrolována z hlediska proveditelnosti vzorce v algoritmu CDCL, je spojeno několik pomocných hodnot [3] :
Schematicky lze typický algoritmus CDCL znázornit následovně [3] :
Algoritmus CDCL(φ, ν) vstup: φ - vzorec (CNF) ν - zobrazení hodnot proměnných ve formě sady párů výstup: SAT (vzorec splnitelný) nebo UNSAT (nesplnitelný) if UnitPropagationConflict(φ, ν) pak Návrat UNSAT L := 0 -- hladina řešení zatímco NotAllVariablesAssigned(φ, ν) (x, v) := PickBranchingVariable(φ, ν) -- rozhodování L:= L + 1 ν := ν ∪ {(x, v)} if UnitPropagationConflict(φ, ν) -- výstupní důsledky pak β := ConflictAnalysis(φ, ν) -- diagnostika konfliktů pokud β < 0 pak Návrat UNSAT v opačném případě Backtrack(φ, ν, β) -- return (backtracking) L := β Návrat SATTento algoritmus používá několik podprogramů, které kromě vracení hodnot mohou také měnit proměnné φ, ν [3] , které jim byly předány odkazem :
Procedura analýzy konfliktů je ústředním prvkem algoritmu CDCL.
Hlavní datovou strukturou používanou v řešičích CDCL je implikační graf , který fixuje přiřazení k proměnným (jak jako výsledek rozhodnutí, tak i použitím jediného disjunktního pravidla), ve kterých vrcholy odpovídají vzorcovým literálům a oblouky fixují strukturu implikací [4 ] [5] .
Procedura analýzy konfliktu (viz schéma algoritmu) je volána, když je detekován konflikt podle pravidla jediné klauzule a na jejím základě je množina zapamatovaných klauzulí doplněna. Procedura začíná v uzlu implikačního grafu, kde je nalezen konflikt, a prochází rozhodovacími úrovněmi s nižšími čísly, jde zpět přes implikace, dokud nenarazí na naposledy přiřazenou (jako výsledek rozhodnutí) proměnnou [3] . Memorované věty se používají v nechronologickém backtrackingu , což je další technika typická pro řešitele CDCL [6] .
Pro srovnání:
DPLL : žádné memorování klauzulí, chronologický návrat.
CDCL: zapamatování klauzulí jako výsledek analýzy konfliktů a nechronologické zpětné sledování
Myšlenka použití struktury implikací, která vedla ke konfliktu, byla vyvinuta směrem k použití UIP ( angl. Unit Implication Points - „jednotné implikační body“). UIP je dominátor implikačního grafu , který lze pro tento typ grafu vypočítat v lineárním čase. UIP je alternativní přiřazení proměnné a klauzule uložená v prvním takovém bodě je zaručena, že bude mít nejmenší velikost a poskytne největší snížení úrovně řešení. Kvůli použití efektivních lazy datových struktur používají autoři mnoha SAT řešitelů, například Chaff, první metodu UIP k zapamatování klauzulí ( first UIP clause learning ) [3] .
Stejně jako DPLL je algoritmus CDCL správným a úplným řešičem SAT. Memorování klauzulí tedy neovlivňuje úplnost a správnost, protože každou zapamatovanou klauzi lze odvodit z počátečních klauzulí a dalších zapamatovaných klauzulí metodou rozlišení . Změněný mechanismus vracení také neovlivňuje úplnost a správnost, protože informace o vracení je uložena v zapamatované klauzuli [3] .
Ilustrace operace algoritmu:
Výběr větvené proměnné: x1 . Žlutý kruh znamená svévolné rozhodnutí.
Podle pravidla jednotné klauzule by x4 mělo být 1. Šedý kruh je vynucené přiřazení. Výsledný graf je implikační graf.
Libovolná volba jiné proměnné, x3 .
Aplikace pravidla jednotkové klauzule a nalezení nového implikačního grafu.
Proměnné x8 a x12 logicky nabývají hodnot 0 a 1.
Opět výběr větvené proměnné: x2 .
Konstrukce implikačního grafu.
Další proměnná: x7 .
Konstrukce implikačního grafu.
Nový implikační graf. Přijatý konflikt .
Hledání řezu grafu , který vedl ke konfliktu, a konfliktní klauzule.
Hledání disjunkce negací: jestliže z a vyplývá b , pak z ne-b následuje ne-a
Vzpomínka na disjunkt.
Nechronologický návrat na příslušnou rozhodovací úroveň.
Vhodné hodnoty nastavení.
SAT řešiče založené na algoritmu CDCL nacházejí uplatnění v automatickém dokazování teorémů , kryptografii , model checkingu a testování hardwaru a softwaru, bioinformatice , určování závislostí v systémech správy balíků atd. [3]