Conjunctieve normaalvorm

Uit Wikipedia, de vrije encyclopedie
Ga naar: navigatie, zoeken

In de logica is een propositie in conjunctieve normaalvorm (Eng. Conjunctive Normal Form, CNF, ook wel afgekort als CNV) als die bestaat uit een conjunctie van disjuncties met literals (ook een conjunctie van clauses genoemd). In een conjunctieve normaalvorm komen alleen de Booleaanse operatoren en, of en negatie voor waarbij de negatie alleen als onderdeel van een atomaire formule kan voorkomen. Er bestaat ook een disjunctieve normaalvorm, een disjunctie van conjuncties.

Elke propositie kan omgezet worden naar een equivalente propositie in conjunctieve normaalvorm met behulp van regels (zoals de wetten van De Morgan en distributiviteit) die de propositie omschrijven naar een logisch equivalente vorm in CNF.

Voorbeelden[bewerken]

Voorbeelden van proposities in conjunctieve normaalvorm:

(A \vee B) \wedge (\neg A \vee B)
C \wedge D
(P \vee Q \vee R) \wedge (\neg Q \vee \neg P) \wedge \neg R

De volgende formules zijn echter niet in conjunctieve normaalvorm:

\neg (B \vee C)
(A \wedge B) \vee C
A \wedge (B \vee (D \wedge E))

De volgende formules in conjunctieve normaalvorm zijn respectievelijk logisch equivalent aan de voorgaande drie formules:

\neg B \wedge \neg C
(A \vee C) \wedge (B \vee C)
A \wedge (B \vee D) \wedge (B \vee E)

Toepassingen[bewerken]

CNF is onder andere belangrijk in het vakgebied automatisch redeneren, het deelgebied van informatica waarin computers logische redeneerprocessen uitvoeren. Verschillende klassieke algoritmen in dat vakgebied, zoals het DPLL-algoritme, verwachten een formule in conjunctieve normaalvorm als invoer. Het omschrijven naar conjunctieve normaalvorm kan met behulp van logische wetten en met de Tseitin-transformatie; dit algoritme levert een vervulbaarheidsequivalente formule in conjunctieve normaalvorm op en geen logisch equivalente formule.

Conversie naar conjunctieve normaalvorm[bewerken]

Elke formule van de klassieke propositielogica kan omgezet worden naar CNF door herhaling van de volgende stappen.

  1. Elimineer \leftrightarrow (bi-implicatie) met behulp van:
    P \leftrightarrow Q \equiv (P \rightarrow Q) \wedge (Q \rightarrow P)
  2. Elimineer \rightarrow (implicatie) met behulp van:
    P \rightarrow Q \equiv \neg P \vee Q
  3. Verplaats \neg (negatie) naar binnen met behulp van:
    \neg(\neg P) \equiv P (elimineren van dubbele negatie)
    \neg(P \wedge Q) \equiv \neg P \vee \neg Q (wetten van De Morgan)
    \neg(P \vee Q) \equiv \neg P \wedge \neg Q (wetten van De Morgan)
  4. Distribueer \vee over \wedge:
    (P \wedge Q) \vee R \equiv (P \vee R) \wedge (Q \vee R)

Voor de klassieke predicatenlogica bestaat een soortgelijke procedure. In de modale logica is conversie naar CNF niet in alle gevallen mogelijk.

Vervulbaarheid[bewerken]

Binnen de complexiteitstheorie bestaat een vervulbaarheidsprobleem waarbij men onderzoekt of een formule in conjunctieve normaalvorm vervulbaar is; dit probleem heet CNF-SAT. Een formule in conjunctieve normaalvorm is vervulbaar als elk van de clausules (disjuncties) vervulbaar is.

Het k-SAT probleem bestaat uit het vervullen van een formule in conjunctieve normaalvorm waarbij elke disjunct k literals bevat. Het probleem 3-SAT is NP-volledig (evenals elk ander k-SAT probleem voor k > 2) terwijl voor 2-SAT een oplossing in polynomiale tijd gevonden kan worden.

Tautologie[bewerken]

Het is mogelijk om in polynomiale tijd te controleren of een formule in conjunctieve normaalvorm een tautologie is (een formule die altijd waar is). Het algoritme in pseudocode:

isCNFTautology(formule F):
 for each conjunct C in F:
   if C bevat geen complementaire literals:
     return false
 return true

Een formule in conjunctieve normaalvorm bestaat uit een conjunctie van disjuncties dus de gehele formule is waar als elk van de conjuncten waar is. Een disjunctie is altijd waar als het complementaire literals bevat (zowel p als de negatie daarvan). Het is dus mogelijk om een formule af te lopen en voor elk van de conjuncten te kijken of het complementaire literals bevat. Als dit het geval is voor elk van de conjuncten dan is de formule een tautologie. In de pseudocode hierboven wordt alleen true teruggegeven wanneer dit geldt; als voor 1 van de conjucten de gegeven voorwaarde niet geldt, dan wordt al gelijk false teruggegeven.

Trivia[bewerken]

  • Een conjunctie staat ook in conjunctieve normaalvorm; elk van de disjuncties bevat exact 1 literal.

Zie ook[bewerken]