Come anche Wikipedia chiarisce (http://it.wikipedia.org/wiki/Distributivit%C3%A0), la disgiunzione logica (or) è distributiva rispetto alla congiunzione (and).

Data una formula f = ( A | (C & D)), dove | rappresenta l'or e & l'and, l'applicazione della proprietà distributiva porta f in forma normale congiuntiva (CNF), cioè a essere una congiunzione di disgiunzioni.

f(cnf) = ((A | C) & (A | D))

L'algoritmo più banale per applicare questa proprietà, che ci è stato (si spera) insegnato alle scuole medie ha il grosso difetto di far crescere in maniera esponenziale la dimensione della formula CNF al crescere della dimensione di f.

Per esempio, nel caso più sfortunato con cui ci può capitare di avere a che fare, cioè il dover passare da una forma normale disgiuntiva (DNF) alla CNF:

f' = ((A & B) | (C & D)), f'(cnf) = ((A | C) & (A | D) & (B | C) & (B | D))

aumentando di poco la dimensione della formula di partenza, il numero di clausole finali tende a "esplodere", rendendo intrattabile il problema veramente molto presto:

Expr f: ((*1 & *2) | (*3 & *4) | (*5 & *6))
Applico distr a f: ((*5 | *1 | *3) & (*5 | *1 | *4) & (*5 | *2 | *3) & (*5 | *2 | *4) & (*6 | *1 | *3) & (*6 | *1 | *4) & (*6 | *2 | *3) & (*6 | *2 | *4))

Va inoltre considerato che il caso in cui si deve passare da DNF a CNF non è così remoto, perchè anche solo una applicazione delle regole di Demorgan lasciano la formula in questo stato:

!(A | !B) -demorgan-> (!A & B)

Algoritmo di Tseitin

Questo scienziato russo, nel suo ostico articolo "G.S. Tseitin: On the complexity of derivation in propositional calculus.", (risalente agli anni settanta) ha proposto un metodo a di poco semplice e geniale che permette di portare una formula f qualsiasi in CNF in tempo lineare rispetto alla dimensione di f, semplicemente introducendo nuove variabili.

Partendo dal presupposto (piuttosto semplice) che:

(A -> B) = (!A | B) = A implica B

(A <-> B) = ((A -> B) & (B -> A)) = ((!A | B) & (!B | A)) = A se e solo se B

Data la formula con cui siamo partiti, cioè  f = ( A | (C & D)), dobbiamo come prima cosa elaborarne un semplice albero di parsing, che avrà questa forma:

         OR

      /         \

  A             AND

                 /      \

              C           D

A questo punto non ci resta che sostituire ogni nodo che rappresenta un operatore logico con una variabile appositamente introdotta, ottenendo tale albero:

         h1

      /         \

  A              h2

                 /      \

              C           D

Sfruttando quindi le equivalenze semantiche di conseguenza logica e del "se e solo se", l'espressione che descrive questo nuovo albero può essere nella forma:

(h1 <-> (A | h2)) & h1 & (h2 <-> (C & D))

La formula si presenta quindi come un AND n-ario di espressioni composte da letterali singoli o da "se e solo se".

Sfruttando la favorevole regola di eliminazione del "se e solo se", si possono sostituire queste formule con delle espressioni equivalenti già in CNF:

((!h1 | (A | h2)) & (!(A | h2)  | h1)) & h1 & ((!h2 | (C & D)) & (!(C & D)  | h2))

A questo punto si può "compattare" l'espressione quando operatori logici hanno come figli operatori dello stesso tipo e applicare la versione "banale" della distributività dell'or dove invece è necessario. In questo modo l'algoritmo inefficiente viene usato solo su piccole porzioni del problema originario, evitando di dare luogo all'"esplosione" computazionale che altrimenti si sarebbe verificata.

Rimuovendo le parentesi inutili si ottiene:

(!h1 | A | h2) & (!(A | h2)  | h1) & h1 & (!h2 | (C & D)) & (!(C & D) | h2)

Applicando la demorgan:

(!h1 | A | h2) & ((!A & !h2) | h1) & h1 & (!h2 | (C & D)) & (!C | !D | h2)

Applicando la proprietà distributiva:

(!h1 | A | h2) & (!A | h1) & (!h2 | h1) & h1 & (C | !h2) & (D | !h2) & (!C | !D | h2)

Asserire h1, facendolo comparire come variabile singola nell'AND più esterno rende è indispensabile per la sottostante "catena" di implicazioni.

Ogni operatore dell'algebra booleana può essere sostituito da una variabile appositamente introdotta, per cui questo algoritmo è in grado di portare in forma CNF qualsiasi formula ben formata della logica proposizionale.

Mi scuso per gli eventuali errori, spero che possa essere utile a qualcuno come lo è stato a me.