Algorisme DPLL
En lògica i informàtica, l'algorisme de Davis–Putnam–Logemann–Loveland (DPLL) és un algorisme de cerca complet basat en retrocés per decidir la satisfacció de fórmules de lògica proposicional en forma conjuntiva normal, és a dir, per resoldre el problema CNF-SAT.[1]
Va ser introduït el 1961 per Martin Davis, George Logemann i Donald W. Loveland i és un perfeccionament de l'anterior algorisme de Davis-Putnam, que és un procediment basat en la resolució desenvolupat per Davis i Hilary Putnam el 1960. Especialment en publicacions més antigues, l'algorisme de Davis-Logemann-Loveland es coneix sovint com el "mètode Davis-Putnam" o l'"algorisme DP". Altres noms comuns que mantenen la distinció són DLL i DPLL.[2]
Implementacions i aplicacions
[modifica]El problema SAT és important tant des del punt de vista teòric com pràctic. En teoria de la complexitat, va ser el primer problema que es va demostrar que era NP-complet, i pot aparèixer en una àmplia varietat d'aplicacions com ara la verificació de models, la planificació i programació automatitzada i el diagnòstic en intel·ligència artificial.
Com a tal, escriure solucions SAT eficients ha estat un tema de recerca durant molts anys. GRASP (1996-1999) va ser una implementació primerenca utilitzant DPLL. A les competicions SAT internacionals, les implementacions basades en DPLL com zChaff i MiniSat [3] van ocupar els primers llocs de les competicions el 2004 i el 2005.
Una altra aplicació que sovint implica DPLL és la demostració automatitzada de teoremes o les teories del mòdul de satisfacció (SMT), que és un problema SAT en què les variables proposicionals es substitueixen per fórmules d'una altra teoria matemàtica.[4]
L'algorisme
[modifica]L'algorisme de retrocés bàsic s'executa escollint un literal, assignant-li un valor de veritat, simplificant la fórmula i després comprovant recursivament si la fórmula simplificada és satisfactòria; si aquest és el cas, la fórmula original és satisfacible; en cas contrari, es fa la mateixa comprovació recursiva assumint el valor de veritat oposat. Això es coneix com la regla de divisió, ja que divideix el problema en dos subproblemes més simples. El pas de simplificació elimina essencialment totes les clàusules que esdevenen certes sota l'assignació de la fórmula, i tots els literals que esdevenen falses de les clàusules restants.
L'algoritme DPLL millora l'algoritme de retrocés mitjançant l'ús diligent de les regles següents a cada pas:
- Propagació unitat
- Si una clàusula és una clàusula unitària, és a dir, conté només un únic literal sense assignar, aquesta clàusula només es pot satisfer assignant el valor necessari perquè aquest literal sigui cert. Per tant, no cal cap opció. La propagació d'unitat consisteix a eliminar totes les clàusules que continguin el literal d'una clàusula unitària i a descartar el complement del literal d'una clàusula unitat de totes les clàusules que continguin aquest complement. A la pràctica, això sovint condueix a cascades deterministes d'unitats, evitant així una gran part de l'espai de cerca ingenu.
- Pura eliminació literal
- Si una variable proposicional es produeix amb només una polaritat a la fórmula, s'anomena pura. Un literal pur sempre es pot assignar de manera que totes les clàusules que el contenen siguin certes. Així, quan s'assigna d'aquesta manera, aquestes clàusules ja no limiten la cerca i es poden suprimir.
La insatisfacció d'una assignació parcial determinada es detecta si una clàusula es queda buida, és a dir, si totes les seves variables s'han assignat de manera que els literals corresponents siguin falsos. La satisfacció de la fórmula es detecta quan s'assignen totes les variables sense generar la clàusula buida o, en les implementacions modernes, si es compleixen totes les clàusules. La insatisfacció de la fórmula completa només es pot detectar després d'una recerca exhaustiva.
L'algorisme DPLL es pot resumir en el següent pseudocodi, on Φ és la fórmula CNF :
Algorithm DPLL
Entrada: Un conjunt de clàusuless Φ.
Sortida: Un valor de veritat que indica si Φ és satisfacible.
function DPLL(Φ)
// unit propagation:
while there is a unit clause {l} in Φ do
Φ ← unit-propagate(l, Φ);
// pure literal elimination:
while there is a literal l that occurs pure in Φ do
Φ ← pure-literal-assign(l, Φ);
// stopping conditions:
if Φ is empty then
return true;
if Φ contains an empty clause then
return false;
// DPLL procedure:
l ← choose-literal(Φ);
return DPLL(Φ ∧ {l}) or DPLL(Φ ∧ {¬l});
- "←" indica l'assignació. Per exemple, "element ← més gran" significa que el valor del més gran canvia al valor de l'element. "retorn" finalitza l'algorisme i genera el valor següent.
En aquest pseudocodi, unit-propagate(l, Φ) i pure-literal-assign(l, Φ) són funcions que retornen el resultat d'aplicar la propagació d'unitats i la regla literal pura, respectivament, al literal l i a la fórmula Φ. En altres paraules, substitueixen cada aparició de l per "vertader" i cada aparició de not l per "fals" a la fórmula Φ i simplifiquen la fórmula resultant. L' or a la instrucció return és un operador de curtcircuit. Φ ∧ {l} denota el resultat simplificat de substituir "vertader" per l a Φ.
L'algorisme acaba en un dels dos casos. O la fórmula CNF Φ és buida, és a dir, no conté cap clàusula. Aleshores queda satisfet per qualsevol assignació, ja que totes les seves clàusules són vàcuament certes. En cas contrari, quan la fórmula conté una clàusula buida, la clàusula és vàcuament falsa perquè una disjunció requereix almenys un membre que sigui cert perquè el conjunt global sigui cert. En aquest cas, l'existència d'aquesta clàusula implica que la fórmula (avaluada com a conjunció de totes les clàusules) no pot avaluar-se com a vertadera i ha de ser insatisfactoria.
La funció de pseudocodi DPLL només retorna si l'assignació final compleix la fórmula o no. En una implementació real, l'assignació satisfactòria parcial normalment també es retorna amb èxit; això es pot derivar fent un seguiment dels literals ramificats i de les assignacions literals fetes durant la propagació d'unitats i l'eliminació literal pura.
L'algorisme de Davis–Logemann–Loveland depèn de l'elecció del literal de ramificació, que és el literal considerat en el pas de retrocés. Com a resultat, no es tracta exactament d'un algorisme, sinó d'una família d'algorismes, un per a cada forma possible d'escollir el literal de ramificació. L'eficiència es veu fortament afectada per l'elecció del literal de ramificació: hi ha casos en què el temps d'execució és constant o exponencial depenent de l'elecció dels literals de ramificació. Aquestes funcions d'elecció també s'anomenen funcions heurístiques o heurístiques de ramificació.[5]
-
Totes les clàusules que fan una fórmula CNF -
Trieu una variable -
Preneu una decisió, variable a = Fals (0), per tant les clàusules verdes esdevenen Vertaderes -
Després de prendre diverses decisions, trobem un gràfic d'implicacions que condueix a un conflicte. -
Ara feu marxa enrere al nivell immediat i per força assigneu un valor oposat a aquesta variable -
Però una decisió forçada encara porta a un altre conflicte -
Torna al nivell anterior i pren una decisió forçada -
Preneu una nova decisió, però condueix a un conflicte -
Preneu una decisió forçada, però de nou porta a un conflicte -
Tornar enrere al nivell anterior -
Continueu d'aquesta manera i el gràfic d'implicació final
Referències
[modifica]- ↑ «The DPLL Algorithm» (en anglès). [Consulta: 1r febrer 2025].
- ↑ Özlütıraş, Mert. «Brief Explanation of DPLL (Davis — Putnam — Logemann-Loveland) Algorithm» (en anglès), 18-02-2021. [Consulta: 1r febrer 2025].
- ↑ «Minisat website» (en anglès).
- ↑ «[https://upcommons.upc.edu/bitstream/handle/2099.1/18737/89494.pdf Solving integer programming problems using DPLL-based algorithms]» (en anglès). [Consulta: 1r febrer 2025].
- ↑ Marques-Silva, João P. «The Impact of Branching Heuristics in Propositional Satisfiability Algorithms». A: Barahona. Progress in Artificial Intelligence: 9th Portuguese Conference on Artificial Intelligence, EPIA '99 Évora, Portugal, September 21–24, 1999 Proceedings (en anglès). 1695, 1999, p. 62–63 (LNCS). DOI 10.1007/3-540-48159-1_5. ISBN 978-3-540-66548-9.