CDCL ( conflikt -driven clause learning ) -algoritmi on tehokas ( NP-täydellinen ) Boolen kaavojen (SAT-ratkaisija) tyydyttävyysongelmien ratkaisija , joka perustuu DPLL-algoritmiin . CDCL-ratkaisijoiden pääasiallinen tietorakenne on implikaatiokaavio, joka kaappaa muuttujien määritykset, ja toinen ominaisuus on ei-kronologisten paluu- ja muistamislauseiden käyttö konfliktianalyysin aikana.
Algoritmia ehdottivat João Marques -Silva ja Karem A. Sakallah vuonna 1996 [ 1] ja itsenäisesti Roberto J. Bayardo ja Robert Schrag . Robert C. Schrag ) vuonna 1997 [2] [3] .
CDCL - algoritmin taustalla oleva DPLL-algoritmi käyttää paluuta konjunktiivisissa normaalimuodoissa , jonka jokaisessa vaiheessa valitaan muuttuja ja sille annetaan arvo (0 tai 1) myöhempää haarautumista varten, joka koostuu arvon määrittämisestä muuttujalle, jonka jälkeen yksinkertaistettu kaavan toteutettavuus testataan rekursiivisesti. Jos ristiriita kohdataan , eli tuloksena oleva kaava ei ole mahdollinen, palautusmekanismi (backtracking) aktivoituu, jossa haaroja peruutetaan, joissa kumpaakin arvoa yritettiin muuttujalle. Jos haku palaa ensimmäisen tason haaraan, koko kaava julistetaan tyydyttäväksi . Tällaista DPLL-algoritmille ominaista palautusta kutsutaan kronologiseksi [3] .
Algoritmissa käytetyt disjunktit jaetaan tyytyväisiin (tyytyväisiin), kun disjunktiin sisältyvien arvojen joukossa on 1, tyytymätön (tyytymätön) - kaikki arvot ovat nollia, yksi (yksikkö) - kaikki nollia, paitsi yksi muuttuja, jolle ei ole vielä määritetty arvoa, ja ratkaisematon - kaikki muu. Yksi SAT-ratkaisijoiden tärkeimmistä komponenteista on single disjunkt rule , jossa muuttujan ja sen arvon valinta on yksiselitteinen. (On muistettava, että disjunkti sisältää sekä muuttujat että niiden negatiivit . ) Yksikköproseduuri ( nykyaikaisissa CDCL -ratkaisijoissa se perustuu lähes aina yhden disjunktin sääntöön) suoritetaan haaroittamisen jälkeen tehdyn valinnan loogisten seurausten laskemiseksi [ 3] .
DPLL:n ja sen backtracking-mekanismin lisäksi CDCL käyttää joitain muita temppuja [3] :
Jokaiseen muuttujaan, jonka kaavan toteutettavuus tarkistetaan CDCL-algoritmissa [3] , liittyy useita apuarvoja :
Kaavamaisesti tyypillinen CDCL-algoritmi voidaan esittää seuraavasti [3] :
Algoritmi CDCL(φ, ν) syöttö: φ - kaava (CNF) ν - muuttujien arvojen näyttö parijoukon muodossa poistu: SAT (formula satisfiable) tai UNSAT (ei tyydyttävä) if UnitPropagationConflict(φ, ν) sitten UNSAT paluu L := 0 -- ratkaisutaso while Not AllVariablesAssigned(φ, ν) (x, v) := PickBranchingVariable(φ, ν) -- päätöksenteko L := L + 1 ν := ν ∪ {(x, v)} if UnitPropagationConflict(φ, ν) -- tulosten seuraukset sitten β := ConflictAnalysis(φ, ν) -- ristiriitadiagnostiikka jos β < 0 sitten UNSAT paluu muuten Backtrack(φ, ν, β) -- paluu (backtracking) L := β SAT paluuTämä algoritmi käyttää useita alirutiineja, jotka voivat palauttaa arvojen lisäksi myös muuttaa niille viittauksella välitettyjä muuttujia φ, ν [3] :
Konfliktianalyysimenettely on keskeinen CDCL-algoritmissa.
CDCL -ratkaisijoiden pääasiallinen tietorakenne on implikaatiograafi , joka kiinnittää muuttujien osoitukset (sekä päätösten tuloksena että yhden disjunkt-säännön avulla), jossa kärjet vastaavat kaavaliteraaaleja ja kaaret vahvistavat implikaatioiden rakenteen [4 ] [5] .
Konfliktianalyysimenettelyä (katso algoritmikaavio) kutsutaan, kun ristiriita havaitaan yksittäislausesäännön mukaan ja sen perusteella täydennetään muistiin tallennettujen lauseiden joukkoa. Proseduuri alkaa implikaatiokaavion solmusta, josta ristiriita löytyy, ja kulkee päätöstasojen läpi pienemmillä luvuilla ja menee takaisin implikaatioiden läpi, kunnes se kohtaa viimeksi määritetyn (päätöksen seurauksena) muuttujan [3] . Muistettuja lauseita käytetään ei - kronologisessa backtrackingissa , joka on toinen CDCL-ratkaisijoille tyypillinen tekniikka [6] .
Vertailun vuoksi:
DPLL : ei lauseiden ulkoa opettelua, kronologinen palautus.
CDCL: lauseen muistaminen ristiriitaanalyysin ja ei-kronologisen perääntymisen tuloksena
Ajatus konfliktiin johtaneiden implikaatioiden rakenteen käyttämisestä kehitettiin kohti UIP:n käyttöä ( Eng. Unit Impplication Points - "yksittäisimplikaatiopisteet"). UIP on implikaatiografiikkadominaattori , joka voidaan laskea lineaarisessa ajassa tämän tyyppiselle graafille . UIP on vaihtoehtoinen muuttujaosoitus, ja ensimmäiseen tällaiseen kohtaan tallennettu lause on taatusti pienin ja tarjoaa suurimman ratkaisutason laskun. Tehokkaiden laiskojen tietorakenteiden käytön vuoksi monien SAT-ratkaisijoiden, esimerkiksi Chaff, kirjoittajat käyttävät ensimmäistä UIP-menetelmää lauseiden ulkoamiseen ( ensimmäinen UIP-lauseen oppiminen ) [3] .
Kuten DPLL , CDCL-algoritmi on oikea ja täydellinen SAT-ratkaisija. Lauseiden ulkoa muistaminen ei siis vaikuta täydellisyyteen ja oikeellisuuteen, koska kukin ulkoa opittu lause voidaan päätellä alkulauseista ja muista muistiin tallennetuista lauseista resoluutiomenetelmällä . Myöskään muuttunut palautusmekanismi ei vaikuta täydellisyyteen ja oikeellisuuteen, koska tiedot palautuksesta tallennetaan muistiin tallennettuun lauseeseen [3] .
Algoritmin toiminnan kuva:
Haaramuuttujien valinta: x1 . Keltainen ympyrä tarkoittaa mielivaltaista päätöstä.
Yksikkölausesäännön mukaan x4 : n tulee olla 1. Harmaa ympyrä on pakotettu tehtävä. Tuloksena oleva graafi on implikaatiokaavio.
Toisen muuttujan, x3 , mielivaltainen valinta .
Yksikkölausesäännön soveltaminen ja uuden implikaatiograafin löytäminen.
Muuttujat x8 ja x12 ottavat loogisesti arvot 0 ja 1, vastaavasti.
Haaramuuttujan valinta uudelleen: x2 .
Implikaatiograafin rakentaminen.
Toinen muuttuja: x7 .
Implikaatiograafin rakentaminen.
Uusi implikaatiokaavio. Sai konfliktin .
Ristiriitaan johtaneen kaavion leikkauksen ja ristiriitalausekkeen löytäminen .
Disjunktin löytäminen negaatiolla: jos a :sta seuraa b , niin ei-b :stä seuraa not-a
Eron muistaminen.
Ei-kronologinen paluu sopivalle päätöstasolle.
Sopivat asetusarvot.
CDCL-algoritmiin perustuvat SAT-ratkaisijat löytävät sovelluksen automaattisessa lauseen todistamisessa , kryptografiassa , mallintarkistuksessa ja laitteiston ja ohjelmiston testauksessa, bioinformatiikassa , riippuvuuksien määrittämisessä paketinhallintajärjestelmissä jne. [3]