DPLL

DPLL ( Davis-Putnam-Logeman-Loveland algorithm ) er en komplet backtracking -algoritme til løsning af CNF-SAT- problemet  - bestemmelse af tilfredsstillelsen af ​​booleske formler skrevet i konjunktiv normal form .

Udgivet i 1962 af Martin Davis , Hilary Putnam , George Logeman og Donald Loveland som en forbedring af den tidligere Davis-Putnam-algoritme baseret på opløsningsreglen .

Det er en yderst effektiv algoritme og forbliver relevant efter et halvt århundrede og bruges i de fleste SAT -løsere og automatiske bevissystemer til fragmenter af førsteordens logik [1] .

Implementeringer og applikationer

Problemet med tilfredsstillelse af booleske formler er vigtigt fra både teoretiske og praktiske synspunkter. I kompleksitetsteorien er dette det første problem, for hvilket medlemskab i klassen af ​​NP-komplette problemer er blevet bevist . Det kan også optræde i en lang række praktiske anvendelser, såsom modelkontrol , planlægning og diagnostik.

Dette område var og er stadig et voksende forskningsområde, konkurrencer afholdes årligt mellem forskellige SAT-løsere [2] ; moderne implementeringer af DPLL-algoritmen, såsom Chaff , zChaff [3] [4] , GRASP og Minisat [5] , indtager førstepladsen i sådanne konkurrencer.

En anden type applikation, hvor DPLL ofte bruges, er teorembevissystemer .

Beskrivelse af algoritmen

Den grundlæggende backtracking-algoritme starter med at vælge en variabel, sætte den til sand, forenkle formlen og derefter rekursivt teste den forenklede formel for gennemførlighed; hvis det er muligt, så er den oprindelige formel også mulig; ellers gentages proceduren, men den valgte variabel indstilles til falsk. Denne tilgang kaldes "splitreglen", fordi den deler opgaven op i to enklere underopgaver. Forenklingstrinnet består i at fjerne alle klausuler fra formlen, der bliver sande efter at have tildelt værdien "true" til den valgte variabel og fjerne alle forekomster af denne variabel, der bliver falske, fra de resterende sætninger.

DPLL-algoritmen forbedrer den grundlæggende backtracking-algoritme ved at bruge følgende regler ved hvert trin:

Variabel udbredelse hvis en klausul indeholder præcis én variabel, der endnu ikke er blevet tildelt en værdi, kan den sætning kun blive sand, hvis variablen tildeles en værdi, der gør den sand (sand, hvis variablen er i klausulen uden negation, og falsk, hvis variablen er negativ). Der er således ingen grund til at træffe et valg på dette trin. I praksis efterfølges dette af en kaskade af tildelinger til variabler, hvilket reducerer antallet af iterationsmuligheder markant. Udelukkelse af "rene" variable hvis en variabel indtaster formlen med kun én "polaritet" (det vil sige enten kun uden negationer eller kun med negationer), kaldes den ren . "Rene" variabler kan altid gives en værdi, så alle klausuler, der indeholder dem, bliver sande. Disse klausuler vil således ikke påvirke variationsrummet, og de kan fjernes.

Utilfredsstillelse for givne specifikke variabelværdier er defineret, når en af ​​klausulerne bliver "tom", det vil sige, at alle dens variable får værdier på en sådan måde, at deres forekomster (med eller uden negation) bliver falske. En formels tilfredsstillelse angives enten, når alle variable er sat til værdier, så der ikke er nogen "tomme" klausuler, eller, i moderne implementeringer, hvis alle klausuler er sande. Utilfredsstillelsen af ​​hele formlen kan først fastslås efter afslutningen af ​​udtømmende opregning.

DPLL-algoritmen kan udtrykkes ved hjælp af følgende pseudokode, hvor Φ angiver en formel i konjunktiv normal form:

Inputdata: Et sæt sætninger med formlen Φ. Output: Sandhedsværdi funktion DPLL(Φ) hvis Φ er sættet af eksekverbare klausuler , returneres true; hvis Φ indeholder en tom klausul, så returner falsk; for hver klausul fra én variabel l til Φ Φ enhed-propager ( l , Φ); for hver variabel l , der forekommer i ren form i Φ Φ rent-bogstaveligt-tildele ( l , Φ); l vælg-bogstaveligt (Φ); returnere DPLL (Φ&l) eller DPLL (Φ¬(l));

I denne pseudokode unit-propagate(l, Φ), og pure-literal-assign(l, Φ) er funktioner, der returnerer resultatet af at anvende til henholdsvis en variabel log en variabel udbredelsesformel Φog en "ren variabel" udelukkelsesregel. Med andre ord erstatter de hver forekomst af en variabel lmed sand og hver forekomst af en negeret variabel med not lfalsk i formlen Φ, og forenkler derefter den resulterende formel. Ovenstående pseudo-kode returnerer kun et svar - om det sidste af de tildelte værdisæt opfylder formlen. I moderne implementeringer returnerer delvise udførelsessæt også succes.

Algoritmen afhænger af valget af en "grenvariabel", det vil sige en variabel, der vælges ved næste trin i algoritmen med et afkast. at tildele den en bestemt værdi. Det er således ikke én algoritme, men en hel familie af algoritmer, én for hver mulig måde at vælge "grenvariabler på". Algoritmens effektivitet afhænger stærkt af dette valg: Der er eksempler på problemer, hvor algoritmens køretid kan være konstant eller vokse eksponentielt afhængigt af valget af "grenvariable". Udvælgelsesmetoder er heuristiske teknikker og kaldes også "forgrenende heuristik" [6] .

Samtidsforskning

Nuværende forskning for at forbedre algoritmen udføres i tre retninger: definitionen af ​​forskellige optimeringsmetoder til at vælge en "grenvariabel"; udvikling af nye datastrukturer for at fremskynde algoritmen, især til variabel udbredelse; og udvikling af forskellige varianter af den grundlæggende backtracking-algoritme. Den sidste retning omfatter "ikke-kronologisk tilbagesporing" og at huske dårlige sager . Disse forbedringer kan beskrives som en metode til at returnere, efter at en falsk klausul er nået, hvor det huskes, hvilken bestemt tildeling af en værdi til en variabel, der forårsagede dette resultat for at undgå nøjagtig samme rækkefølge af beregninger i fremtiden, og derved reducere arbejdstid.

En nyere algoritme, Stalmark-metoden, har været kendt siden 1990. Også siden 1986 er beslutningsdiagrammer blevet brugt til at løse SAT-problemet.

Baseret på DPLL-algoritmen blev CDCL-algoritmen oprettet i midten af ​​1990'erne og er blevet meget brugt .

Noter

  1. ↑ Nieuwenhuis, Robert; Oliveras, Albert & Tinelly, Cesar (2004), Abstract DPLL and Abstract DPLL Modulo Theories , Logic for Programming, Artificial Intelligence, and Reasoning, LPAR 2004, Proceedings : 36–50 , < http://www.lsi.upc.edu /~roberto/papers/lpar04.pdf > Arkiveret 17. november 2011 på Wayback Machine 
  2. ↑ Den internationale SAT Competitions-webside , sat! live , < http://www.satcompetition.org/ > Arkiveret 12. februar 2005 på Wayback Machine 
  3. ↑ zChaff hjemmeside , < http://www.princeton.edu/~chaff/zchaff.html > Arkiveret 19. april 2017 på Wayback Machine 
  4. ↑ Chaff hjemmeside , < http://www.princeton.edu/~chaff/ > Arkiveret 23. februar 2020 på Wayback Machine 
  5. ↑ Minisat hjemmeside . Arkiveret fra originalen den 20. april 2012.
  6. ↑ Marques-silva, Joao. Indvirkningen af ​​forgreningsheuristik i propositionelle tilfredshedsalgoritmer  (engelsk)  // I 9. portugisiske konference om kunstig intelligens (EPIA): tidsskrift. - 1999. - doi : 10.1.1.111.9184 . Arkiveret fra originalen den 14. april 2012.

Litteratur