Disjunctieve normaalvormIn 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. VoorbeeldenVoorbeelden van formules in disjunctieve normaalvorm: De volgende formules zijn echter niet in disjunctieve normaalvorm:
VervulbaarheidHet is mogelijk om in polynomiale tijd te controleren of een formule in disjunctieve normaalvorm vervulbaar is. Het algoritme in pseudocode:
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. Bijzonderheid
Zie ook |