Algoritmi - algoritmo per applicare proprietà distributiva

Ciao a tutti, ho una domanda piuttosto difficile per voi, e con difficile intendo che non mi servono risposte banali ma solo cose veramente astute.

Data una formula ben formata della logica proposizionale F, mi servirebbe qualche consiglio per un algoritmo che applichi a F la proprietà distributiva rispetto alla disgiunzione (or).

Ecco degli esempi:

Expr f: (*1 | (*2 & *3))
Applico distr f: ((*1 | *2) & (*1 | *3))

Expr f: ((*4 & !*5) | (*2 & !*3))
Applico distr f: ((*4 | *2) & (*4 | !*3) & (!*5 | *2) & (!*5 | !*3))

Expr f: ((*4 & !*5) | (*2 & !*3) | (*7 & !*8))
Applico distr f: ((*7 | *4 | *2) & (*7 | *4 | !*3) & (*7 | !*5 | *2) & (*7 | !*5 | !*3) & (!*8 | *4 | *2) & (!*8 | *4 | !*3) & (!*8 | !*5 | *2) & (!*8 | !*5 | !*3))

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

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

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

Expr f: ((*1 & *2) | (*3 & *4) | (*5 & *6))
Applico distr 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))

Concludendo, specifico che (come si può notare dagli esempi che appunto sono l'output di un programma) una funzione che implementi l'applicazione della proprietà distributiva l'ho scritta, ma dato l'utilizzo che ne devo fare (su formule decisamente ENORMI), me ne serve una versione in cui l'efficienza sia un requisito fondamentale!!!

un grazie infinito a chi ha la bontà di suggerire qualcosa!

sicuramente potresti implementarla con le regex, che poi una volta compilata volerà

EDIT: ad esempio una regex che fa il replace della prima può essere:

(?<first>\*?\d)\s*\|\s*\((?<second>\*?\d)\s*&\s*(?<third>\*?\d)\)

replace: (${first} | ${second}) & (${first} | ${third})

innanzitutto grazie per la risposta.
ci sono però due problemi:
1- l'espressione è rappresentata attraverso un albero di parsing i cui nodi sono oggetti java
2- le regex funzionerebbe nel caso singolo, ma a me serve che applichi la proprietà a ogni fbf. per fare ciò dovrei comunque usare una forma di ricorsione, (cosa che per altro faccio già.

il problema è che data una espressione in DNF, applicare la distributività per portarla in CNF causa una ESPLOSIONE (nel senso matematico del termine) del numero di termini di cui è composta, rendendo intrattabile il problema (se affrontato nella maniera più ovvia e più comune) cioè se come algoritmo si usa quello intuitivo che chiunque ha imparato a scuola quando gli hanno insegnato ad applicare tale proprietà.
mi servirebbe una euristica o qualcosa di simile che non "subisca" il peso di quella specie di iper-prodotto cartesiano che viene fatto applicando la distributività dell'or a una formula tipo questa:

sist[0]= ((*22 & *28 & *39 & *54 & *37 & *4) | (!*54 & *22 & *28 & *39 & *37 & *4) | (!*54 & !*4 & *22 & *28 & *39 & *37) | (!*54 & !*37 & *22 & *28 & *39 & *4) | (!*39 & *22 & *28 & *54 & *37 & *4) | (!*39 & !*4 & *22 & *28 & *54 & *37) | (!*39 & !*37 & !*4 & *22 & *28 & *54) | (!*39 & !*54 & !*37 & *22 & *28 & *4) | (!*39 & !*54 & !*37 & !*4 & *22 & *28) | (!*28 & !*4 & *22 & *39 & *54 & *37) | (!*28 & !*37 & *22 & *39 & *54 & *4) | (!*28 & !*37 & !*4 & *22 & *39 & *54) | (!*28 & !*54 & *22 & *39 & *37 & *4) | (!*28 & !*39 & !*4 & *22 & *54 & *37) | (!*28 & !*39 & !*37 & *22 & *54 & *4) | (!*28 & !*39 & !*54 & !*37 & !*4 & *22) | (!*22 & *28 & *39 & *54 & *37 & *4) | (!*22 & !*37 & *28 & *39 & *54 & *4) | (!*22 & !*54 & *28 & *39 & *37 & *4) | (!*22 & !*54 & !*37 & !*4 & *28 & *39) | (!*22 & !*39 & !*4 & *28 & *54 & *37) | (!*22 & !*39 & !*54 & *28 & *37 & *4) | (!*22 & !*39 & !*54 & !*4 & *28 & *37) | (!*22 & !*28 & !*4 & *39 & *54 & *37) | (!*22 & !*28 & !*54 & !*4 & *39 & *37) | (!*22 & !*28 & !*54 & !*37 & *39 & *4) | (!*22 & !*28 & !*39 & *54 & *37 & *4) | (!*22 & !*28 & !*39 & !*37 & *54 & *4) | (!*22 & !*28 & !*39 & !*37 & !*4 & *54) | (!*22 & !*28 & !*39 & !*54 & *37 & *4) | (!*22 & !*28 & !*39 & !*54 & !*4 & *37) | (!*22 & !*28 & !*39 & !*54 & !*37 & !*4))

considerando che java si mette a ciclare senza lasciare speranza, che questa è la versione più "corta" delle formule che mi servono e che anche in questo caso semplice tale formula ha 64 fratelli che devono subire la stessa "distributiva" sorte.. non so veramente che fare!

ok ragazzi ho trovato la soluzione.. in realtà non l'ho trovata io ma il signor Tseitin, che merita un gran rispetto! però se volete possiamo aprire un bel CHALLENGE per vedere all'interno di pierotofy.it chi riesce a mettere in piedi l'algoritmo migliore!
vi dico che per ora il lower bound è applicare la proprietà distributiva in tempo lineare NON in-place.