Conjunctieve normaalvorm

In de logica is een formule in conjunctieve normaalvorm (Eng. conjunctive normal form, CNF, ook wel afgekort als CNV) als die bestaat uit een conjunctie van disjuncties met literalen (ook een conjunctie van clausules genoemd). In een conjunctieve normaalvorm komen alleen de booleaanse operatoren 'en', 'of' en negatie voor, waarbij de negatie alleen als onderdeel van een literaal kan voorkomen. Er bestaat ook een disjunctieve normaalvorm, een disjunctie van conjuncties.

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

Voorbeelden

Voorbeelden van formules 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 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

De 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 de 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

Elke formule van de klassieke propositielogica kan omgezet worden naar een 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

Binnen de complexiteitstheorie bestaat een vervulbaarheidsprobleem waarbij men onderzoekt of een formule in conjunctieve normaalvorm vervulbaar is; dit probleem heet CNF-SAT.

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

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 een van de conjucten de gegeven voorwaarde niet geldt, dan wordt al gelijk false teruggegeven.

Trivia

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

Zie ook

• Disjunctieve normaalvorm