DPLL

DPLL ( algoritmul Davis-Putnam-Logeman-Loveland ) este un algoritm complet de backtracking pentru rezolvarea problemei CNF-SAT  - determinând satisfacabilitatea formulelor booleene scrise în formă normală conjunctivă .

Publicat în 1962 de Martin Davis , Hilary Putnam , George Logeman și Donald Loveland ca o îmbunătățire a algoritmului anterior Davis-Putnam bazat pe regula rezoluției .

Este un algoritm extrem de eficient și rămâne relevant după o jumătate de secol și este folosit în majoritatea solutoarelor SAT și a sistemelor automate de demonstrare pentru fragmente de logica de ordinul întâi [1] .

Implementări și aplicații

Problema satisfacabilității formulelor booleene este importantă atât din punct de vedere teoretic, cât și din punct de vedere practic. În teoria complexității, aceasta este prima problemă pentru care s- a dovedit apartenența la clasa de probleme NP-complete . De asemenea, poate apărea într-o mare varietate de aplicații practice, cum ar fi verificarea modelului , programarea și diagnosticarea.

Acest domeniu a fost și este încă un domeniu de cercetare în creștere, anual se țin concursuri între diferiți rezolvatori SAT [2] ; implementările moderne ale algoritmului DPLL, precum Chaff , zChaff [3] [4] , GRASP și Minisat [5] , ocupă primul loc în astfel de competiții.

Un alt tip de aplicație în care DPLL este adesea folosit este sistemele de demonstrare a teoremelor .

Descrierea algoritmului

Algoritmul de bază de backtracking începe prin selectarea unei variabile, setarea acesteia la adevărat, simplificarea formulei și apoi testarea recursiv a formulei simplificate pentru fezabilitate; dacă este fezabilă, atunci formula originală este și ea fezabilă; în caz contrar, procedura se repetă, dar variabila selectată este setată la fals. Această abordare este numită „regula împărțirii” deoarece descompune sarcina în două subsarcini mai simple. Pasul de simplificare constă în eliminarea tuturor clauzelor din formulă care devin adevărate după atribuirea valorii „adevărat” variabilei selectate și eliminarea din clauzele rămase toate aparițiile acestei variabile care devin false.

Algoritmul DPLL îmbunătățește algoritmul de bază de backtracking utilizând următoarele reguli la fiecare pas:

Propagare variabilă dacă o clauză conține exact o variabilă căreia nu i s-a atribuit încă o valoare, acea clauză poate deveni adevărată numai dacă variabilei i se atribuie o valoare care o face adevărată (adevărată dacă variabila se află în clauză fără negație și falsă dacă variabila este negativ). Astfel, nu este nevoie să faceți o alegere la acest pas. În practică, aceasta este urmată de o cascadă de atribuiri la variabile, reducând astfel semnificativ numărul de opțiuni de iterație. Excluderea variabilelor „pure”. dacă o variabilă intră în formula cu o singură „polaritate” (adică fie numai fără negații, fie numai cu negații), se numește pură . Variabilelor „pure” li se poate da întotdeauna o valoare astfel încât toate clauzele care le conțin să devină adevărate. Astfel, aceste clauze nu vor afecta spațiul variantelor, putând fi eliminate.

Nesatisfiabilitatea pentru anumite valori ale variabilelor specifice este definită atunci când una dintre clauze devine „vide”, adică tuturor variabilelor sale li se dau valori în așa fel încât aparițiile lor (cu sau fără negație) devin false. Satisabilitatea unei formule este afirmată fie atunci când toate variabilele sunt setate la valori, astfel încât să nu existe clauze „vide”, fie, în implementările moderne, dacă toate clauzele sunt adevărate. Nesatisfacerea întregii formule poate fi stabilită numai după încheierea enumerarii exhaustive.

Algoritmul DPLL poate fi exprimat folosind următorul pseudocod, unde Φ denotă o formulă în formă normală conjunctivă:

Date de intrare: Un set de clauze cu formula Φ. Ieșire: Valoarea adevărului funcția DPLL(Φ) dacă Φ este setul de clauze executabile, atunci returnează adevărat; dacă Φ conține o clauză goală atunci returnează false; pentru fiecare clauză de la o variabilă l la Φ Φ unitate-propagă ( l , Φ); pentru fiecare variabilă l care apare sub formă pură în Φ Φ pur-literal-assign ( l , Φ); l alege-literal (Φ); returnează DPLL (Φ&l) sau DPLL (Φ¬(l));

În acest pseudocod unit-propagate(l, Φ), și pure-literal-assign(l, Φ) sunt funcții care returnează rezultatul aplicării unei variabile lși unei formule de propagare a variabilei Φși, respectiv, o regulă de excludere a „variabilei pure”. Cu alte cuvinte, ele înlocuiesc fiecare apariție a unei variabile lcu adevărat și fiecare apariție a unei variabile negate cu not lfals în formula Φși apoi simplifică formula rezultată. Pseudo-codul de mai sus returnează doar un răspuns - dacă ultimul dintre seturile de valori atribuite îndeplinește formula. În implementările moderne, seturile de execuție parțială revin și ele la succes.

Algoritmul depinde de alegerea unei „variabile de ramură”, adică a unei variabile care este selectată la pasul următor al algoritmului cu un randament. pentru a-i atribui o anumită valoare. Astfel, nu este un algoritm, ci o întreagă familie de algoritmi, câte unul pentru fiecare modalitate posibilă de alegere a „variabilelor de ramificație”. Eficiența algoritmului depinde puternic de această alegere: există exemple de probleme pentru care timpul de rulare al algoritmului poate fi constant sau poate crește exponențial, în funcție de alegerea „variabilelor de ramificație”. Metodele de selecție sunt tehnici euristice și sunt numite și „euristice de ramificare” [6] .

Cercetare contemporană

Cercetările actuale de îmbunătățire a algoritmului se desfășoară în trei direcții: definirea diferitelor metode de optimizare pentru alegerea unei „variabile de ramură”; dezvoltarea de noi structuri de date pentru accelerarea algoritmului, în special pentru propagarea variabilelor; și dezvoltarea diferitelor variante ale algoritmului de bază de backtracking. Ultima direcție include „backtracking non-cronologic” și amintirea cazurilor proaste . Aceste îmbunătățiri pot fi descrise ca o metodă de revenire după ce se ajunge la o clauză falsă, în care se reține ce anume atribuire a unei valori unei variabile a determinat acest rezultat pentru a evita exact aceeași secvență de calcule în viitor, reducând astfel timp de muncă.

Un algoritm mai nou, metoda Stalmark, este cunoscut din 1990. Tot din 1986, diagramele de decizie au fost folosite pentru a rezolva problema SAT.

Bazat pe algoritmul DPLL, algoritmul CDCL a fost creat la mijlocul anilor 1990 și a devenit utilizat pe scară largă .

Note

  1. ↑ Nieuwenhuis, Robert; Oliveras, Albert & Tinelly, Cesar (2004), Abstract DPLL și 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 > Arhivat 17 noiembrie 2011 la Wayback Machine 
  2. ↑ Pagina web a Competițiilor internaționale SAT , sat! live , < http://www.satcompetition.org/ > Arhivat 12 februarie 2005 la Wayback Machine 
  3. ↑ Site-ul web zChaff , < http://www.princeton.edu/~chaff/zchaff.html > Arhivat 19 aprilie 2017 la Wayback Machine 
  4. ↑ Site-ul web Chaff , < http://www.princeton.edu/~chaff/ > Arhivat 23 februarie 2020 la Wayback Machine 
  5. ↑ Site-ul Minisat . Arhivat din original pe 20 aprilie 2012.
  6. ↑ Marques-silva, Joao. Impactul euristicii de ramificare în algoritmii de satisfacție propozițională  (engleză)  // În a 9-a Conferință portugheză privind inteligența artificială (EPIA): jurnal. - 1999. - doi : 10.1.1.111.9184 . Arhivat din original pe 14 aprilie 2012.

Literatură