DPLL

DPLL ( Davis-Putnam-Logeman-Loveland algorithm ) är en komplett bakåtspårningsalgoritm för att lösa CNF-SAT- problemet  - bestämma tillfredsställelsen av booleska formler skrivna i konjunktiv normal form .

Publicerad 1962 av Martin Davis , Hilary Putnam , George Logeman och Donald Loveland som en förbättring av den tidigare Davis-Putnam-algoritmen baserad på upplösningsregeln .

Det är en mycket effektiv algoritm och förblir relevant efter ett halvt sekel och används i de flesta SAT -lösare och automatiska bevissystem för fragment av första ordningens logik [1] .

Implementeringar och tillämpningar

Problemet med tillfredsställelse av booleska formler är viktigt ur både teoretisk och praktisk synvinkel. I komplexitetsteorin är detta det första problemet för vilket medlemskap i klassen av NP-kompletta problem har bevisats . Det kan också förekomma i en mängd olika praktiska tillämpningar, såsom modellkontroll , schemaläggning och diagnostik.

Detta område var och är fortfarande ett växande forskningsområde, tävlingar hålls årligen mellan olika SAT-lösare [2] ; moderna implementeringar av DPLL-algoritmen, såsom Chaff , zChaff [3] [4] , GRASP och Minisat [5] , tar förstaplatsen i sådana tävlingar.

En annan typ av applikation där DPLL ofta används är system som bevisar teorem .

Beskrivning av algoritmen

Den grundläggande bakåtspårningsalgoritmen börjar med att välja en variabel, ställa in den på sann, förenkla formeln och sedan rekursivt testa den förenklade formeln för genomförbarhet; om det är genomförbart, så är den ursprungliga formeln också genomförbar; annars upprepas proceduren, men den valda variabeln är inställd på false. Detta tillvägagångssätt kallas "delad regel" eftersom det delar upp uppgiften i två enklare deluppgifter. Förenklingssteget består i att ta bort alla satser från formeln som blir sanna efter att ha tilldelats värdet "true" till den valda variabeln och att ta bort alla förekomster av denna variabel som blir falska från de återstående satserna.

DPLL-algoritmen förbättrar den grundläggande backtracking-algoritmen genom att använda följande regler i varje steg:

Variabel spridning om en sats innehåller exakt en variabel som ännu inte har tilldelats ett värde, kan den satsen bara bli sann om variabeln tilldelas ett värde som gör den sann (sant om variabeln finns i satsen utan negation, och falskt om variabeln är negativ). Det finns alltså inget behov av att göra ett val i detta steg. I praktiken följs detta av en kaskad av tilldelningar till variabler, vilket avsevärt minskar antalet iterationsalternativ. Exkludering av "rena" variabler om någon variabel anger formeln med endast en "polaritet" (det vill säga antingen bara utan negationer eller bara med negationer), kallas den ren . "Rena" variabler kan alltid ges ett värde så att alla satser som innehåller dem blir sanna. Således kommer dessa klausuler inte att påverka utrymmet för varianter, och de kan tas bort.

Otillfredsställelse för givna specifika variabelvärden definieras när en av klausulerna blir "tom", det vill säga alla dess variabler ges värden på ett sådant sätt att deras förekomst (med eller utan negation) blir falsk. Tillfredsställelsen av en formel anges antingen när alla variabler är inställda på värden så att det inte finns några "tomma" satser, eller, i moderna implementeringar, om alla satser är sanna. Otillfredsställelsen av hela formeln kan fastställas först efter slutet av uttömmande uppräkning.

DPLL-algoritmen kan uttryckas med följande pseudokod, där Φ betecknar en formel i konjunktiv normalform:

Indata: En uppsättning satser med formeln Φ. Output: Sanningsvärde funktion DPLL(Φ) om Φ är uppsättningen av körbara satser returnerar true ; om Φ innehåller en tom sats , returnera false ; för varje sats från en variabel l till Φ Φ enhetsförökning ( 1 , Φ); för varje variabel l som förekommer i ren form i Φ Φ ren-bokstavlig-tilldela ( l , Φ); l välj bokstavlig (Φ); returnera DPLL (Φ&l) eller DPLL (Φ¬(l));

I denna pseudokod unit-propagate(l, Φ), och pure-literal-assign(l, Φ) är funktioner som returnerar resultatet av applicering på en variabel loch en variabel förökningsformel Φrespektive en "ren variabel" uteslutningsregel. Med andra ord, de ersätter varje förekomst av en variabel lmed sant och varje förekomst av en negerad variabel med not lfalse i formeln Φoch förenklar sedan den resulterande formeln. Ovanstående pseudokod returnerar bara ett svar - om den sista av de tilldelade uppsättningarna av värden uppfyller formeln. I moderna implementeringar ger partiella exekveringsuppsättningar också framgång.

Algoritmen beror på valet av en "grenvariabel", det vill säga en variabel som väljs i nästa steg i algoritmen med en avkastning. att tilldela det ett specifikt värde. Det är alltså inte en algoritm, utan en hel familj av algoritmer, en för varje möjligt sätt att välja "grenvariabler". Algoritmens effektivitet beror starkt på detta val: det finns exempel på problem där algoritmens gångtid kan vara konstant eller växa exponentiellt, beroende på valet av "grenvariabler". Urvalsmetoder är heuristiska tekniker och kallas även "förgrenande heuristik" [6] .

Samtida forskning

Aktuell forskning för att förbättra algoritmen utförs i tre riktningar: definitionen av olika optimeringsmetoder för att välja en "grenvariabel"; utveckling av nya datastrukturer för att påskynda algoritmen, särskilt för variabel spridning; och utveckling av olika varianter av den grundläggande backtracking-algoritmen. Den sista riktningen inkluderar "icke-kronologisk backtracking" och att komma ihåg dåliga fall . Dessa förbättringar kan beskrivas som en metod för att återvända efter att en falsk klausul har uppnåtts, där det kommer ihåg vilken speciell tilldelning av ett värde till en variabel som orsakade detta resultat för att undvika exakt samma sekvens av beräkningar i framtiden, och därigenom minska arbetstid.

En nyare algoritm, Stalmark-metoden, har varit känd sedan 1990. Även sedan 1986 har beslutsdiagram använts för att lösa SAT-problemet.

Baserat på DPLL-algoritmen skapades CDCL-algoritmen i mitten av 1990-talet och har blivit mycket använd .

Anteckningar

  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 > Arkiverad 17 november 2011 på Wayback Machine 
  2. ↑ Webbsidan för internationella SAT-tävlingar , sat! live , < http://www.satcompetition.org/ > Arkiverad 12 februari 2005 på Wayback Machine 
  3. ↑ zChaffs webbplats , < http://www.princeton.edu/~chaff/zchaff.html > Arkiverad 19 april 2017 på Wayback Machine 
  4. ↑ Chaffs webbplats , < http://www.princeton.edu/~chaff/ > Arkiverad 23 februari 2020 på Wayback Machine 
  5. ↑ Minisat webbplats . Arkiverad från originalet den 20 april 2012.
  6. ↑ Marques-silva, Joao. The impact of branching heuristics in propositional satisfiability algorithms  (engelska)  // In 9th Portuguese Conference on Artificial Intelligence (EPIA): journal. - 1999. - doi : 10.1.1.111.9184 . Arkiverad från originalet den 14 april 2012.

Litteratur