Disjunctieve normaalvorm

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

Voorbeelden van formules in disjunctieve normaalvorm:

${\displaystyle (A\wedge B)\vee (B\wedge D)}$

${\displaystyle \neg P\wedge Q}$

${\displaystyle R\vee (P\wedge Q)\vee (Q\wedge \neg P)}$

De volgende formules zijn echter niet in disjunctieve normaalvorm:

${\displaystyle \neg (A\vee B)}$ (negatie is niet toegestaan als buitenste connectief)

${\displaystyle (A\vee (B\wedge (C\vee D)))}$ (een disjunctie staat in een conjunctie)

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.

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

• Conjunctieve normaalvorm