Modello di Lipton nei DNA Computing
Uno scienziato di Princeton, Richard Lipton, ha inventato uno schema per tradurre le coppie di basi del DNA in sequenze di 0 e di 1. Egli è anche stato in grado di sviluppare una tecnica che consente alle molecole di DNA nella provetta di reazione di simulare il comportamento delle porte logiche di un computer elettronico. Lipton ha così mostrato come un computer molecolare ovvero il DNA Computing possa utilizzare anch’esso la logica booleana degli operatori NOT, OR, AND ed essere quindi sostanzialmente programmabile come qualsiasi altro computer general-purpose. Lipton ha affrontato in particolare il problema della soddisfacibilità di una formula booleana (SAT-problem) che ha da subito suscitato notevole interesse nella comunità scientifica.
Nel 1995 Richard Lipton propose uno schema teorico di algoritmo per la risoluzione con il DNA del problema della soddisfacibilità per una formula booleana. Egli considerò una formula booleana nella forma normale disgiuntiva, dove una particolare formula booleana viene detta clausola.
Idea dell’algoritmo di Lipton
L’algoritmo utilizzato da Lipton per trovare la soluzione al SAT-problem è il seguente: si generano tutte le possibili combinazioni di valori per le n variabili della formula booleana; poi si eliminano tutte le assegnazioni che non soddisfano la prima clausola e si ripete progressivamente la stessa operazione per tutte le assegnazioni che non soddisfano la clausola, con i = 2, …, m. Infine, si verifica se sono rimaste delle assegnazioni di valori per le variabili e, in caso positivo, quelle assegnazioni soddisfano la formula booleana.
Implementazione del modello di Lipton
L’implementazione proposta da Lipton si basava sulla codifica di un grafo orientato con la stessa tecnica adottata da Adleman, in cui ogni nodo xi rappresenta una variabile della formula booleana ed ogni xi’ la sua negazione. I cammini che vanno dal nodo a1 al nodo an+1 si possono considerare come la codifica di un numero binario ad n cifre, in cui si può stabilire per convenzione che se dal vertice ai il cam-mino va verso un vertice xi allora quel tratto codifica uno 0, altrimenti se va verso un vertice xi’ codifica un 1.
