CDCL algoritm

CDCL -algoritmen ( konfliktdriven klausulinlärning  ) är en effektiv lösare ( NP-komplett ) av tillfredsställbarhetsproblem för booleska formler (SAT-lösare)  baserad på DPLL-algoritmen . Huvuddatastrukturen i CDCL-lösare är en implikationsgraf som fångar tilldelningar till variabler, och en annan funktion är användningen av icke-kronologisk backtracking och att komma ihåg satser under konfliktanalys.

Algoritmen föreslogs av João Marques -Silva och Karem A. Sakallah  1996 [ 1 ] och oberoende av Roberto J. Bayardo och Robert Schrag . Robert C. Schrag ) 1997 [2] [3] .    

Beskrivning

DPLL-algoritmen som ligger till grund för CDCL-algoritmen använder backtracking på konjunktiva normala former , vid varje steg av vilka en variabel väljs och tilldelas ett värde (0 eller 1) för efterföljande förgrening, vilket består i att tilldela ett värde till en variabel, varefter en förenklad formeln testas rekursivt för genomförbarhet. I fallet när en konflikt uppstår , det vill säga den resulterande formeln är inte genomförbar, aktiveras returmekanismen (backtracking), där grenar avbryts där båda värdena prövades för variabeln. Om sökningen återgår till en gren på första nivån, förklaras hela formeln otillfredsställande . En sådan avkastning, som är inneboende i DPLL-algoritmen, kallas kronologisk [3] .

Disjunkter som används i algoritmen delas in i nöjd (nöjd), när det finns 1 bland värdena som ingår i disjunkten, otillfredsställd (otillfredsställd) - alla värden är noll, singel (enhet) - alla nollor, utom en variabel som ännu inte har tilldelats något värde, och olöst - resten. En av de viktigaste komponenterna i SAT-lösare är den enda disjunktregeln , där valet av en variabel och dess värde är entydigt. (Det bör påminnas om att disjunkten inkluderar både variabler och deras negationer . ) Enhetsutbredningsproceduren ( i moderna CDCL -lösare är den nästan alltid baserad på den enda disjunktregeln) utförs efter förgrening för att beräkna de logiska konsekvenserna av det val som gjorts [ 3] .  

Förutom DPLL och dess bakåtspårningsmekanism använder CDCL några andra knep [3] :

Algoritmschema

Flera hjälpvärden är associerade med varje variabel som kontrolleras för genomförbarheten av formeln i CDCL-algoritmen [3] :

Schematiskt kan en typisk CDCL-algoritm representeras enligt följande [3] :

Algoritm CDCL(φ, ν) inmatning: φ - formel (CNF) ν - visning av värden för variabler i form av en uppsättning par utgång: SAT (formel tillfredsställande) eller UNSAT (otillfredsställande) if UnitPropagationConflict(φ, ν) sedan UNSAT retur L := 0 -- lösningsnivå medan NotAllVariablesAssigned(φ, ν) (x, v) := PickBranchingVariable(φ, ν) -- beslutsfattande L := L + 1 ν := ν ∪ {(x, v)} if UnitPropagationConflict(φ, ν) -- utdatakonsekvenser sedan β := ConflictAnalysis(φ, ν) -- konfliktdiagnostik om β < 0 sedan UNSAT retur annat Backtrack(φ, ν, β) -- return (backtracking) L := p SAT retur

Denna algoritm använder flera subrutiner som, förutom att returnera värden, också kan ändra variablerna φ, ν [3] som skickas till dem genom referens :

Konfliktanalysproceduren är central för CDCL-algoritmen.

Den huvudsakliga datastrukturen som används i CDCL-lösare är en implikationsgraf som fixar tilldelningar till variabler (både som ett  resultat av beslut och genom att tillämpa den enda disjunkta regeln), där hörn motsvarar formelliteraler och bågar fixar strukturen för implikationer [ 4 ] [5] .

Konfliktanalys

Konfliktanalysproceduren (se algoritmdiagrammet) anropas när en konflikt upptäcks enligt regeln för enkla satser, och på grundval av den fylls uppsättningen av memorerade satser på. Proceduren startar vid noden av implikationsgrafen där konflikten hittas, och går igenom beslutsnivåerna med lägre siffror, går tillbaka genom implikationerna tills den möter den senast tilldelade (som ett resultat av beslutet) variabeln [3] . Memorerade satser används i icke - kronologisk backtracking , vilket är en annan teknik som är typisk för CDCL-lösare [6] . 

För jämförelse:

Idén om att använda strukturen av implikationer som ledde till konflikten utvecklades mot användningen av UIP ( Eng.  Unit Implication Points  - "single impplication points"). UIP är implikationsgrafdominatorn , som kan beräknas i linjär tid för denna typ av graf . UIP är en alternativ variabel tilldelning, och klausulen som lagras vid den första punkten är garanterad att ha den minsta storleken och ge den största minskningen av lösningsnivån. På grund av användningen av effektiva lata datastrukturer använder författarna till många SAT-lösare, till exempel Chaff, den första UIP-metoden för att memorera satser ( första UIP-satsinlärning ) [3] . 

Korrekthet och fullständighet

Precis som DPLL är CDCL-algoritmen en korrekt och komplett SAT-lösare. Således påverkar memoreringen av satser inte fullständigheten och korrektheten, eftersom varje memorerad sats kan härledas från de initiala satserna och andra memorerade satser med hjälp av upplösningsmetoden . Den ändrade returmekanismen påverkar inte heller fullständigheten och riktigheten, eftersom information om returen lagras i den memorerade klausulen [3] .

Exempel

Illustration av algoritmoperation:

Applikationer

SAT-lösare baserade på CDCL-algoritmen hittar tillämpning inom automatisk satsprovning , kryptografi , modellkontroll och testning av hårdvara och mjukvara, bioinformatik , bestämning av beroenden i pakethanteringssystem , etc. [3]

Anteckningar

  1. ↑ JP Marques-Silva och KA Sakallah. GRASP: En ny sökalgoritm för tillfredsställelse. I International Conference on Computer-Aided Design, sidorna 220-227, november 1996.
  2. ↑ R. Bayardo Jr. och R. Schrag. Använder CSP-tillbakablickstekniker för att lösa verkliga SAT-instanser. I National Conference on Artificiell Intelligens, sidorna 203—208, juli 1997
  3. ↑ 1 2 3 4 5 6 7 8 9 10 11 Konfliktdriven klausul Inlärning av SAT Solvers, 2008 .
  4. ↑ Ett generaliserat ramverk för konfliktanalys, 2008 .
  5. ↑ Hamadi, 2013 .
  6. ↑ Pradhan, Harris, 2009 .

Litteratur

Länkar