DPLL

DPLL
Backtracking eksempel uten DPLL backjumping
KlasseBoolsk tilfredsstillelse
Data strukturFormler for proposisjonell logikk
I verste fall tidsmessig
I verste fall romlig
FullJa

DPLL ( Davis-Putnam-Logemann-Loveland ) er en uttømmende søkealgoritme , basert på tilbakesporing , brukt til å bestemme den boolske tilfredsstillelsen til proposisjonelle logiske formler i konjunktiv normalform (CNF), et problem kjent som CNF-SAT .

Den ble introdusert i 1962 av Martin Davis , Hilary Putnam , George Logemann og Donald W. Loveland , og representerer en spesialisering av den tidligere Davis-Putnam-algoritmen , en prosedyre utviklet i 1960 . Av denne grunn, spesielt i eldre publikasjoner, blir Davis-Logemann-Loveland-algoritmen ofte referert til som "Davis-Putnam-metoden" eller "DP-algoritmen". Andre vanlige nomenklaturer som opprettholder skillet mellom de to er DLL og DPLL.

DPLL er en svært effektiv prosedyre, og etter mer enn 40 år danner den fortsatt grunnlaget for de mest effektive komplette SAT-løserne, så vel som for mange teorembevisere for fragmenter av førsteordens logikk .

Algoritme

Den grunnleggende tilbakesporingsalgoritmen utføres ved å velge en bokstavelig, tilordne den en sannhetsverdi (sann eller usann), forenkle formelen og deretter, rekursivt, verifisere om den forenklede formelen er tilfredsstillende; hvis dette er tilfelle, er den opprinnelige formelen også tilfredsstillende; ellers utføres den samme rekursive prosedyren forutsatt at den andre sannhetsverdien (false eller sann). Denne prosedyren er kjent som splittelsesregelen , siden den deler problemet inn i to enklere underproblemer. Forenklingstrinnet fjerner i hovedsak alle ledd som har blitt sanne i den delvise formeltilordningen, og eliminerer fra de resterende leddene alle bokstaver som har blitt falske.

DPLL-algoritmen forbedrer tilbakesporing med tvungen bruk av disse reglene, ved hvert trinn:

Unitær forplantning Hvis en klausul er enhetlig , dvs. den inneholder bare en enkelt ikke-tilordnet bokstavelig, vil denne setningen bare tilfredsstilles ved å tildele den nødvendige sannhetsverdien som gjør den bokstavelige sannheten sann. Så det trengs ikke noe valg, og i praksis fører dette ofte til en kaskade av enhetlige klausuler som vil redusere størrelsen på søkerommet. Eliminering av rene bokstaver Hvis en proposisjonsvariabel vises i formelen bare i én polaritet, sies den å være ren . Rene bokstaver kan alltid tilordnes for å gjøre alle klausuler som inneholder dem sanne. Derfor påvirker disse klausulene ikke lenger forskning og kan elimineres. Selv om denne optimaliseringen er en del av den originale DPLL, utelater mange nåværende implementeringer den, ettersom effekten på effektiviteten til slike implementeringer enten ikke kan beregnes eller, basert på kostnadene for renhetssjekken, til og med negativ.

Utilfredsstillelsen til en gitt deltilordning verifiseres hvis en klausul blir tom, det vil si hvis alle dens variabler har blitt tilordnet på en slik måte at de korresponderende bokstavene blir falske. Formelens tilfredsstillelse kontrolleres når alle variabler er tilordnet uten å generere tomme klausuler eller, i moderne implementeringer, hvis alle klausuler er oppfylt. Utilfredsstillelsen av den komplette formelen kan bare bekreftes etter en uttømmende undersøkelse av problemet.

DPLL-algoritmen kan syntetiseres fra denne pseudokoden , der Φ er CNF-formelen og μ er en delvis, i utgangspunktet tom tilordning:

DPLL-funksjon (Φ, μ) hvis Φ = T returner deretter sant; hvis Φ = F returner deretter false; hvis enhetssetning (l) finnes i Φ returner deretter DPLL (tilordne (l, Φ), μ Λ l); hvis bokstavelig l er funnet ren i Φ returner deretter DPLL (tilordne (l, Φ), μ Λ l); l: = velg-bokstavelig (Φ); returnere DPLL (tilordne (l, Φ), μ Λ l) ELLER DPLL (tildele (IKKE (l), Φ), μ Λ IKKE (l));

I denne pseudokoden er assign(l,Φ)det en funksjon som returnerer en formel som oppnås ved å erstatte hver forekomst av lmed "true" og hver forekomst av not lmed "false" i formelen Φ, og forenkle den resulterende formelen. Denne DPLL-funksjonen returnerer bare når den endelige tildelingen tilfredsstiller formelen eller ikke. I en reell implementering returneres den tilfredsstillende tilordningen til formelen av selve algoritmen (i dette tilfellet ble den utelatt for enkelhets skyld).

Davis-Logemann-Loveland-algoritmen har ytelser som avhenger av valget av forgreningsvariabelen , det vil si den bokstavelige som brukes i tilbakesporingstrinnet. Som du kan se, har vi ikke å gjøre med en algoritme, men mer korrekt en familie av algoritmer, en for hvert mulig valg angående forgreningsvariabelen. Effektiviteten er sterkt påvirket av dette valget, noe som noen ganger fører til forskjellige forekomster av problemet som har konstant snarere enn eksponentiell kjøretid.

Aktuelle studier

Forskning for å forbedre algoritmen tok tre retninger:

  1. definisjon av ulike retningslinjer for valg av forgreningsvariabelen;
  2. definisjon av nye datastrukturer for å gjøre algoritmen raskere, spesielt i enhetsforplantningstrinnet;
  3. definisjon av varianter av den grunnleggende tilbakesporingsalgoritmen, inkludert ikke-kronologisk tilbakesporing (backjumping) og klausullæring . Disse forbedringene gjør det mulig å "lære" hva som var årsakene (tilordninger av variabler) som førte til en konflikt på klausulene, for å unngå å nå denne konflikttilstanden igjen under tilbakesporingen.

Bibliografi

Relaterte elementer

Andre prosjekter