Disjunctieve normaalvorm

In de logica is een formule in disjunctieve normaalvorm (Engels: disjunctive normal form, DNF) als die bestaat uit een disjunctie van conjuncties. In een disjunctieve normaalvorm komen slechts drie booleaanse operatoren voor: en, of en negatie. Daarbij kan de negatie alleen als onderdeel van een atomaire formule voorkomen. Er bestaat ook een conjunctieve normaalvorm, een conjunctie van disjuncties.

VoorbeeldenBewerken

Voorbeelden van formules in disjunctieve normaalvorm:

 
 
 

De volgende formules zijn echter niet in disjunctieve normaalvorm:

  (negatie is niet toegestaan als buitenste connectief)
  (een disjunctie staat in een conjunctie)

VervulbaarheidBewerken

Het is mogelijk om in polynomiale tijd te controleren of een formule in disjunctieve normaalvorm vervulbaar is. Het algoritme in pseudocode:

isDNFSatisfiable(formule F):
for each disjunct D in F:
if D bevat geen complementaire literals:
return true
return false

Een formule in disjunctieve normaalvorm is namelijk vervulbaar als ten minste 1 van zijn disjuncten vervulbaar is; elk van deze disjuncten is een conjunctie van literals. Een conjunctie van literals is vervulbaar als het geen complementaire literals (zowel p als de negatie daarvan) bevat. Men kan dus de formule aflopen en voor elk van de disjuncten controleren of het geen complementaire literals bevat. Als dit het geval is voor een disjunct dan is die vervulbaar en daarmee is de gehele formule ook vervulbaar.

BijzonderheidBewerken

  • Een disjunctie staat ook in disjunctieve normaalvorm; elk van de conjuncties bevat exact 1 literal.

Zie ookBewerken