Algoritme DPLL

Algoritme DPLL

Algoritme DPLL

El algoritme DPLL/Davis-Putnam-Logemann-Loveland és un algoritme complet basat en la regrés arrere que servix per a decidir la satisfactibilidad de les fòrmules de llògica proposicional en una forma normal conjuntiva, és dir, per a resoldre el problema CNF-SAT.

Va ser presentat en 1962 per Martin Davis, Hilary Putnam, George Logemann i Donald W. Loveland i és una refinación del previ algoritme de Davis-Putnam, el qual és un procediment de resolució desenrollat per Davis i Putnam en 1960. L'algoritme Davis-Putnam-Logemann-Loveland és nomenat a sovint com el "método Davis-Putnam" o el "algoritme DP", especialment en publicacions antigues. Atres noms comuns que mantenen la distinció són DLL i DPLL.

El DPLL és un procediment molt eficient i despuix de més de 40 anys encara conforma la base dels solucionadores més eficaços de SAT, aixina com de molts demostradores de teoremes per a fragments de llògica de primer orde.

Algoritme

L'algoritme de regrés arrere (backtracking) s'eixecuta elegint un lliteral, assignant-li un valor de veres a est, simplificant la fòrmula i a continuació, en forma recursiva comprovant si la fòrmula simplificada és satisfacible; si este és el cas la fòrmula original és satisfacible; de lo contrari, la mateixa verificació recursiva termina assumint el valor de veres contrari. Açò es coneix com a regla de divisió, ya que dividix el problema en dos subproblemas més simples. El pas de simplificació essencialment elimina totes les clàusules que es convertixen en verdaderes en funció de la fòrmula, i tots els lliterals de les clàusules restants es convertixen en falses.

L'algoritme DPLL millora sobre l'algoritme de regrés arrere (backtracking) per l'us eficaç de les següents regles:

Unitat de propagació

Si una clàusula és una clàusula unitària, és dir, solament conté un sol lliteral sense assignar, esta clàusula solament pot ser satisfacible per mig de l'assignació del valor necessari per a fer verdader al lliteral. Per lo tant, no hi ha una atra opció. En la pràctica, açò a sovint conduïx a les cascades determinista de les unitats, evitant aixina una gran part de l'ingenu espai de busca.

Eliminació pura lliteral

Si una variable proposicional es produïx en una sola polaridad en la fòrmula, es diu pura. El lliteral pur sempre pot ser assignat de manera que faça que totes les clàusules que les contenen siguen verdaderes. D'esta manera, estes clàusules no llimiten la busca i puguen ser eliminades. ^{cita requerida}

La insatisfacibilidad d'una assignació parcial donada, es detecta si una clàusula es buida, és dir, si totes les variables han segut assignades de manera que fa als lliterals corresponents falsos. La satisfacibilidad de la fòrmula es detecta quan totes les variables s'assignen sense generar la clàusula buida, o en les implementacions modernes, si totes les clàusules són satisfetes. La insatisfacibilidad de la fòrmula completa solament pot detectar-se despuix d'una busca exhaustiva.

Treball Actual

El treball actual sobre la millora de l'algoritme s'ha realisat en tres direccions: la definició de criteris diferents per a l'elecció dels lliterals de ramificació, la definició de noves estructures de senyes per a fer l'algoritme més ràpit, especialment la part sobre la propagació de l'unitat; i la definició de les variants de l'algoritme de regrés arrere bàsic. La direcció d'este últim inclou Regrés arrere no cronològic (senar-chronological backtracking) i Aprenentage de clàusules. Estos refinament descriuen un método de regrés arrere despuix d'aplegar a una clàusula de conflicte que "deprén" la raïl de les causes (assignació a variables) dels conflictes a fi d'evitar aplegar al mateix conflicte.

Vore també

• Algoritme de Davis-Putnam