DPLL-algoritme

Het DPLL-algoritme (Davis-Putnam-Logemann-Loveland algoritme) is een algoritme voor het onderzoeken van de vervulbaarheid van een propositie in conjunctieve normaalvorm (dit probleem is ook bekend als CNF-SAT). Het algoritme werd gepubliceerd in 1962 door Martin Davis, Hilary Putnam, George Logemann en Donald W. Loveland als een verbetering van een eerder algoritme van Davis en Putnam uit 1960. Het algoritme maakt gebruik van backtracking indien nodig.

Er bestaan allerlei verbeterde varianten van het DPLL-algoritme, zoals het Chaff, GRASP en BerkMin.

Werking

Het DPLL-algoritme onderzoekt de vervulbaarheid van een logische formule door herhaaldelijk een waarheidswaarde toe te kennen aan een literal in de formule. Hierna wordt de formule vereenvoudigd en vervolgens wordt gekeken of de vereenvoudige formule vervuld kan worden. Als dit mogelijk is dan is de oorspronkelijke formule vervulbaar en anders niet.

Het algoritme maakt gebruik van drie regels:

• One-literal rule (OLR): als een clausule met 1 literal voorkomt dan kan men die clausule vervullen door de literal waar te maken en vervolgens de overige clausules weg te halen waar deze literal ook in voorkomt. De negatie van de betreffende literal kan weggehaald worden uit de andere clausules want deze zal niet langer bijdragen aan het waarmaken van die clausules.
• Pure literal rule (PLR, controle op pure literals): als een literal alleen positief (bijv p) of negatief (bijvoorbeeld ¬p) voorkomt dan kan men die literal waarmaken en alle clausules waar die in voorkomt weghalen (die clausules zijn nu vervuld).
• Splitsregel: als bovenstaande regels niet meer toegepast kunnen worden, dan kan men een literal kiezen en vervolgens op twee manieren verdergaan: men beschouwt de huidige clausules samen met het geval dat de gekozen literal waar is en het geval dat de gekozen literal onwaar is. Stel men wil controleren of $(p\vee q)\wedge (\neg p\vee \neg q)$ vervulbaar is dan is het mogelijk de splitsregel toe te passen op $p$ en vervolgens te controleren of $p\wedge (p\vee q)\wedge (\neg p\vee \neg q)$ of $\neg p\wedge (p\vee q)\wedge (\neg p\vee \neg q)$ vervulbaar is. Het algoritme zal nu beide alternatieven onderzoeken en als blijkt dat de ene niet vervulbaar is, dan zal het algoritme backtracken en verdergaan met het onderzoeken van de vervulbaarheid van de andere.

Het is mogelijk om ook meer regels te gebruiken voor het vereenvoudigen van een verzameling clausulen, zoals subsumptie waarbij een clausule $C$ wordt weggehaald als er een clausule $D$ is waarvoor geldt $D\subset C$; de clausule $C$ wordt namelijk al vervuld als $D$ vervuld wordt dus $C$ is niet relevant voor het vervullen van de formule. Een andere regel is gebaseerd op tautologieën: een clausule kan weggehaald worden als het complementaire literals bevat want een dergelijke clausule is altijd te vervullen.

Controle op vervulbaarheid

Een formule in conjunctieve normaalvorm is vervulbaar als alle clausules vervuld zijn. Dit is ook het geval wanneer de formule in conjunctieve normaalvorm geen clausules heeft: een formule in conjunctieve normaalvorm is een conjunctie en een conjunctie is ook vervuld wanneer er geen conjuncten zijn. Als het DPLL-algoritme erin slaagt om alle clausules weg te halen en de lege formule over te houden dan is de formule vervulbaar. Het is ook mogelijk een formule in conjunctieve normaalvorm met verzamelingen te noteren: zo wordt $(p\vee q)\wedge (\neg p\vee \neg q)$ genoteerd als de volgende verzameling clausules: $\{\{p,q\},\{\neg p,\neg q\}\}$. Wanneer men de lege verzameling clausules overhoudt dan is de formule ook vervulbaar (dit is hetzelfde als de vorige conditie aangezien men alleen de representatie van de formule heeft veranderd).

Wanneer het algoritme de lege clausule kan afleiden (een clausule zonder literals) dan is de formule niet vervulbaar. De reden hiervoor is dat elk van de clausules vervuld dient te worden en de lege clausule is niet te vervullen: een clausule is een disjunctie van literals en een disjunctie is pas vervuld als ten minste 1 van de literals waar is. Bij het gebruik van verzamelingen is een verzameling clausules $S$ onvervulbaar wanneer er geldt dat $S$ de lege verzameling bevat.

Pseudocode

Hieronder staat pseudocode waarmee DPLL op recursieve wijze geïmplementeerd kan worden. De invoer van het algoritme is een formule F in conjunctieve normaalvorm en de uitvoer is "vervulbaar" of "onvervulbaar".

DPLL(F):
  vereenvoudig F met behulp van vereenvoudigingsregels
  if F is leeg:
    return "vervulbaar"
  if F bevat lege clausule:
    return "onvervulbaar"
  kies een atomaire formule v
  kies een waarheidswaarde b (waar of onwaar)
  if DPLL(F met v = b) is "vervulbaar":
    return "vervulbaar"
  if DPLL(F met v = ¬b) is "vervulbaar":
    return "vervulbaar"
  return "onvervulbaar"

Bij de recursieve aanroepen wordt de formule F meegegeven nadat deze vereenvoudigd is op basis van de gekozen toekenning van waar of onwaar aan de atomaire formule v. Elke clausule die waargemaakt wordt door deze toekenning wordt weggehaald en uit de overige clausulen wordt, indien aanwezig, de negatie van de literal in kwestie weggehaald.

Men zou ook de toekenningen van waar of onwaar aan atomaire formules kunnen bijhouden zodat na afloop ook het model bekend is waarmee de formule wordt waargemaakt (indien de formule vervulbaar bleek).

Kenmerken

Het DPLL-algoritme is gezond, volledig en het termineert altijd. Voor elk van de regels van het DPLL-algoritme geldt dat als de oorspronkelijke verzameling clausules (on)vervulbaar is, dan is de resulterende verzamelingen clausules dat ook en vice versa. Bij de splitsregel zal de (on)vervulbaarheid behouden blijven in ten minste een van de twee takken.

Voorbeelden

Onvervulbare formule

Stel men wil onderzoeken of $\phi =(p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)$ vervulbaar is.

Het algoritme verloopt als volgt:

$(p\vee q\vee \neg r)\wedge (\neg q\vee p)\wedge (\neg p)\wedge (r\vee q)$

Er is een clausule met 1 literal ($\neg p$) dus de one-literal rule kan toegepast worden: $\neg p$ moet waar zijn om die clausule te vervullen dus $p$ is onwaar.

$(q\vee \neg r)\wedge (\neg q)\wedge (r\vee q)$

De one-literal rule kan opnieuw toegepast worden, ditmaal op $\neg q$ (q = onwaar).

$(\neg r)\wedge (r)$

De one-literal rule kan nu toegepast worden op zowel $r$ als $\neg r$. We passen de regel toe op $r$.

De lege clausule wordt nu afgeleid want r = waar en $\neg r$ wordt weggehaald; de lege clausule blijft hierdoor over. Het afleiden van de lege clausule geeft aan dat de formule niet vervulbaar was: een clausule is alleen te vervullen als ten minste 1 van de literals vervuld wordt en bij een lege clausule zijn er geen dus de lege clausule is niet te vervullen. Dit betekent dat $\phi$ onvervulbaar is: er is geen toekenning van waar of onwaar aan de atomaire formules zodanig dat de formule waar is.

Hieronder staat het bovenstaande maar dan genoteerd met verzamelingen:

$\{\{p,q,\neg r\},\{\neg q,p\},\{\neg p\},\{r,q\}\}$

(OLR, p = onwaar)

$\{\{q,\neg r\},\{\neg q\},\{r,q\}\}$

(OLR, q = onwaar)

$\{\{\neg r\},\{r\}\}$

(OLR, r = waar)

$\{\{\}\}$

Vervulbare formule

De formule is $\phi =(s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)$.

Het algoritme verloopt als volgt:

$(s\vee t)\wedge (\neg s\vee \neg t)\wedge (p\vee u)\wedge (\neg p\vee u)$

Literal $u$ komt alleen positief voor dus de formule kan vereenvoudigd worden met u = waar

$(s\vee t)\wedge (\neg s\vee \neg t)$

Beide vereenvoudigingsregels kunnen niet toegepast worden maar de splitsregel kan wel toegepast worden. We splitsen op $s$ en $\neg s$

$\phi _{1}=(s)\wedge (s\vee t)\wedge (\neg s\vee \neg t)$ en $\phi _{2}=(\neg s)\wedge (s\vee t)\wedge (\neg s\vee \neg t)$

De one-literal rule kan nu toegepast worden op $\phi _{1}$ (s = waar).

$\phi _{1}'=(\neg t)$

Deze formule is vervulbaar met t = onwaar. Deze tak na de splitsing is dus vervulbaar. Dit betekent dat de oorspronkelijke formule vervulbaar is en dat de vervulbaarheid van $\phi _{2}$ niet onderzocht hoeft te worden (er is nu al een manier gevonden om de formule te vervullen). De oorspronkelijke formule kan vervuld worden met u = waar, s = waar en t = onwaar. Deze waarheidswaarden zijn tijdens het uitvoeren van het DPLL-algoritme bepaald.

Het bovenstaande genoteerd met verzamelingen:

$\{\{s,t\},\{\neg s,\neg t\},\{p,u\},\{\neg p,u\}\}$

(PLR, u = waar)

$\{\{s,t\},\{\neg s,\neg t\}\}$

(splitsen op $s$ en $\neg s$)

$\phi _{1}=\{\{s\},\{s,t\},\{\neg s,\neg t\}\}$ en $\phi _{2}=\{\{\neg s\},\{s,t\},\{\neg s,\neg t\}\}$

(OLR op $\phi _{1}$, s = waar)

$\phi _{1}'=\{\{\neg t\}\}$

(OLR op $\phi _{1}'$, t = onwaar)

$\{\}$

De verzameling clausules in deze tak na de splitsing is leeg dus de oorspronkelijke formule is vervulbaar.

Zie ook

• Resolutie

Bronnen, noten en/of referenties