Algoritmul CDCL ( conflict-driven clause learning ) este un rezolvator eficient ( NP-complet ) de probleme de satisfacție pentru formule booleene (solver SAT) bazat pe algoritmul DPLL . Structura principală a datelor din soluțiile CDCL este un grafic de implicație care surprinde asignările variabilelor, iar o altă caracteristică este utilizarea clauzelor de backtracking non-cronologic și memorarea clauzelor în timpul analizei conflictului.
Algoritmul a fost propus de João Marques -Silva și Karem A. Sakallah în 1996 [ 1] și independent de Roberto J. Bayardo și Robert Schrag . Robert C. Schrag ) în 1997 [2] [3] .
Algoritmul DPLL care stă la baza algoritmului CDCL folosește backtracking pe forme normale conjunctive , la fiecare pas din care se selectează o variabilă și i se atribuie o valoare (0 sau 1) pentru ramificarea ulterioară, care constă în atribuirea unei valori unei variabile, după care o variabilă simplificată. formula este testată recursiv pentru fezabilitate. În cazul în care se întâlnește un conflict , adică formula rezultată nu este fezabilă, se activează mecanismul de returnare (backtracking), în care se anulează ramurile în care s-au încercat ambele valori pentru variabilă. Dacă căutarea revine la o ramură de prim nivel, întreaga formulă este declarată nesatisfăcătoare . O astfel de întoarcere, inerentă algoritmului DPLL, se numește cronologic [3] .
Disjuncțiile utilizate în algoritm sunt împărțite în satisfăcut (satisfăcut), când există 1 dintre valorile incluse în disjunct, nesatisfăcut (nesatisfăcut) - toate valorile sunt zero, singur (unitate) - toate zerourile, cu excepția unuia variabilă căreia nu i s-a atribuit încă o valoare și nerezolvată - tot restul. Una dintre cele mai importante componente ale rezolutorilor SAT este regula disjunctă unică , în care alegerea unei variabile și a valorii acesteia este fără ambiguitate. (Trebuie reamintit că disjunctul include atât variabilele, cât și negațiile acestora . ) Procedura de propagare a unității ( în soluțiile CDCL moderne se bazează aproape întotdeauna pe regula disjuncturii unice) se realizează după ramificare pentru a calcula consecințele logice ale alegerii făcute [ 3] .
Pe lângă DPLL și mecanismul său de backtracking, CDCL folosește alte trucuri [3] :
Mai multe valori auxiliare sunt asociate cu fiecare variabilă care este verificată pentru fezabilitatea formulei în algoritmul CDCL [3] :
Schematic, un algoritm CDCL tipic poate fi reprezentat după cum urmează [3] :
Algoritmul CDCL(φ, ν) intrare: φ - formula (CNF) ν - afișarea valorilor variabilelor sub forma unui set de perechi Ieșire: SAT (formula satisfăcătoare) sau UNSAT (nesatisfăcut) if UnitPropagationConflict(φ, ν) apoi UNSAT întoarcere L := 0 -- nivel de decizie în timp ce NotAllVariablesAssigned(φ, ν) (x, v) := PickBranchingVariable(φ, ν) -- luarea deciziilor L := L + 1 ν := ν ∪ {(x, v)} if UnitPropagationConflict(φ, ν) -- consecințele de ieșire apoi β := ConflictAnalysis(φ, ν) -- diagnosticarea conflictelor dacă β < 0 apoi UNSAT întoarcere in caz contrar Backtrack(φ, ν, β) -- întoarcere (backtrack) L := β Retur SATAcest algoritm folosește mai multe subrutine care, pe lângă returnarea valorilor, pot modifica și variabilele φ, ν [3] transmise acestora prin referință :
Procedura de analiză a conflictului este centrală pentru algoritmul CDCL.
Principala structură de date utilizată în rezolutoarele CDCL este un grafic de implicație care fixează alocări variabilelor (atât ca rezultat al deciziilor, cât și prin aplicarea regulii disjuncturii unice), în care vârfurile corespund literalilor de formule, iar arcele fixează structura implicațiilor [ 4 ] ] [5] .
Procedura de analiză a conflictului (vezi diagrama algoritmului) este apelată atunci când un conflict este detectat conform regulii unei singure clauze, iar pe baza acesteia se reînnoiește setul de clauze memorate. Procedura începe de la nodul grafului de implicație unde se găsește conflictul și parcurge nivelurile de decizie cu numere mai mici, retrocedând prin implicații până când întâlnește cea mai recentă variabilă atribuită (ca urmare a deciziei) [3] . Clauzele memorate sunt folosite în backtracking non - cronologic , care este o altă tehnică tipică pentru rezolvatorii CDCL [6] .
Pentru comparație:
DPLL : fără memorare a clauzelor, întoarcere cronologică.
CDCL: memorarea clauzelor ca rezultat al analizei conflictului și al backtracking non-cronologic
Ideea utilizării structurii implicațiilor care a dus la conflict a fost dezvoltată spre utilizarea UIP ( Eng. Unit Implication Points - „puncte unice de implicare”). UIP este dominatorul graficului de implicație , care poate fi calculat în timp liniar pentru acest tip de grafic. UIP este o alocare variabilă alternativă, iar clauza stocată la primul astfel de punct este garantată să aibă cea mai mică dimensiune și să ofere cea mai mare reducere a nivelului de soluție. Datorită utilizării unor structuri eficiente de date leneșe, autorii multor solutoare SAT, de exemplu, Chaff, folosesc prima metodă UIP pentru a memora clauze ( first UIP clause learning ) [3] .
La fel ca DPLL , algoritmul CDCL este un solutor SAT corect și complet. Astfel, memorarea clauzelor nu afectează completitudinea și corectitudinea, deoarece fiecare clauză memorată poate fi dedusă din clauzele inițiale și din alte clauze memorate prin metoda rezoluției . De asemenea, mecanismul de returnare modificat nu afectează completitatea și corectitudinea, deoarece informațiile despre returnare sunt stocate în clauza memorată [3] .
Ilustrația funcționării algoritmului:
Selectarea variabilei de ramură: x1 . Cercul galben înseamnă o decizie arbitrară.
Conform regulii clauzei singulare , x4 ar trebui să fie 1. Cercul gri este o atribuire forțată. Graficul rezultat este graficul de implicație.
O alegere arbitrară a unei alte variabile, x3 .
Aplicarea regulii clauzei unitare și găsirea unui nou grafic de implicație.
Variabilele x8 și x12 iau în mod logic valorile 0 și, respectiv, 1.
Selectarea variabilei de ramură din nou: x2 .
Construirea unui grafic de implicație.
O altă variabilă: x7 .
Construirea unui grafic de implicație.
Noul grafic de implicare. A primit un conflict .
Găsirea tăieturii graficului care a dus la conflict și clauza de conflict.
Găsirea unui disjunct prin negație: dacă din a urmează b , atunci din not-b urmează not-a
Amintind disjunctul.
Revenirea non-cronologică la nivelul de decizie adecvat.
Valori de setare adecvate.
Rezolvatorii SAT bazați pe algoritmul CDCL își găsesc aplicații în demonstrarea automată a teoremelor , criptografia , verificarea și testarea modelelor hardware și software, bioinformatică , determinarea dependențelor în sistemele de management al pachetelor etc. [3]