Cos'è ElectroYou | Login Iscriviti

ElectroYou - la comunità dei professionisti del mondo elettrico

7
voti

Forma cum laude: Logica proposizionale

Indice

PRESENTAZIONE

Bentornato, caro lettore! Dopo tanto tempo, ricominciamo queste nostre discussioni sui metodi formali e sulle loro basi teoriche: in questo articolo, proseguiremo la nostra analisi della logica proposizionale, adottando questa volta il punto di vista di un "teorico" (ma non troppo!) dei linguaggi formali, e contestualmente vedremo il problema della soddisfacibilità delle formule proposizionali, il quale rappresenta uno dei problemi più importanti nell'ambito dei metodi formali (come vedremo prossimamente) e non solo. Anzitutto, quel che faremo sarà descrivere un po' cosa sono i linguaggi formali, in modo da acquisire la terminologia e le basi teoriche che ci occorrono; a seguire, definiremo a dovere il linguaggio della logica proposizionale e accenneremo brevemente (molto brevemente!) al suo utilizzo nell'ambito delle dimostrazioni; per finire, tratteremo il problema della soddisfacibilità, ovvero la ricerca di una condizione che renda vera una certa formula, e vedremo un fondamentale algoritmo che useremo tantissimo quando parleremo effettivamente di metodi formali.
Prima di iniziare, la solita premessa: non ci si aspetta che il lettore abbia particolari competenze specifiche, per cui quest'articolo tratterà i vari argomenti in modo molto semplice, facendo ricorso ove possibile a paragoni e associazioni d'idee necessariamente riduttivi, ma sperabilmente in grado di favorire la comprensione dei concetti.


PRIMA DI INIZIARE: I LINGUAGGI FORMALI

Linguaggi e grammatiche

Abbiamo già utilizzato l'espressione "linguaggio formale" varie volte nel corso dei nostri articoli, ma adesso è il momento di parlarne... formalmente, appunto. Iniziamo dotandoci di un alfabeto, ovvero di un insieme di simboli: essi costituiranno la base del linguaggio, i "mattoncini" con cui costruire tutto ciò che il linguaggio ci permetterà di esprimere. Fatto questo, definiamo delle regole per mettere insieme questi simboli, ovvero una grammatica.
Bene, e poi? Abbiamo un alfabeto e abbiamo una grammatica: per costruire un linguaggio basta questo, giusto? La risposta è meno banale di quanto ci si potrebbe aspettare, perché nell'utilizzo quotidiano del linguaggio (sia esso il linguaggio naturale, un linguaggio di programmazione o qualsiasi altro tipo di linguaggio) noi diamo per scontate alcune cose che in realtà non lo sono: quando finisce una parola e ne inizia un'altra? Come si collega un significato a una seguenza di grafemi o di fonemi?
Abbandoniamo per un attimo il problema di dare un senso al nostro linguaggio, perché si tratta di un problema complesso e fortemente legato allo specifico linguaggio, e concentriamoci invece sul discorso puramente sintattico, notando anzitutto che noi sappiamo quando una parola finisce per due motivi: il primo, banalmente, è che siamo in grado di riconoscere le parole che conosciamo, e il secondo è che dopo ogni parola c'è uno spazio o un qualche segno di interpunzione. Non ci vuole tanto a notare che il primo dei due criteri è soggettivo e di formalizzazione discutibile (almeno per quanto ci riguarda), per cui dobbiamo basarci sul secondo e introdurre nel nostro linguaggio un qualche simbolo che ci dica quando una parola finisce. Stando così le cose, non indugiamo oltre e definiamo formalmente, utilizzando una scrittura analoga a quella di [HMU07] e [MAK88], una grammatica come una tupla G = (N,T,P,S) dove:

  • L'insieme N contiene tutti i simboli non terminali del linguaggio, ovvero i simboli che vengono utilizzati all'interno delle regole della grammatica ma che non compongono le parole del linguaggio.
  • L'insieme T contiene tutti i simboli terminali del linguaggio, i quali incredibilmente sono i simboli che vanno a comporre le parole del linguaggio; già che siamo in vena di cose incredibili, notiamo che se X è il nostro alfabeto allora X = N \cup T.
  • L'insieme P contiene tutte le produzioni della grammatica, ovvero le sue regole.
  • L'elemento S \in N è il cosiddetto elemento di partenza della grammatica, ovvero quello a partire dal quale si costruiscono tutte le parole.

Definita una grammatica, il linguaggio ad essa relativo è sintatticamente identificabile in modo ovvio: si tratta dell'insieme di tutte e sole le parole costruite utilizzando il contenuto della grammatica; formalmente, se X è un alfabeto e G è una grammatica basata su di esso, per il linguaggio L(G) generato da una tale grammatica si usa scrivere L(G) \subset X^*, dove X * è il cosiddetto monoide libero dell'alfabeto, che intuitivamente possiamo interpretare come l'insieme di tutte e sole le "sequenze" (eventualmente vuote) costruite con i suoi simboli. Noi non ci occuperemo della teoria dei semigruppi e di conseguenza neanche (se non per brevi spunti) della teoria algebrica degli automi, per cui non useremo operativamente una tale definizione, ma è comunque fondamentale averla sempre ben presente; gli interessati, in ogni caso, sono invitati a consultare i testi in bibliografia, e in particolare [Bourbaki89] e [DLDA13].

Gerarchia di Chomsky

I linguaggi, ovviamente, non sono tutti uguali: le produzioni della grammatica di un linguaggio definiscono esattamente cosa esso permette di scrivere. Il linguista Noam Chomsky ha diviso i linguaggi in quattro categorie sulla base della potenza delle grammatiche:

  • I linguaggi più potenti sono i cosiddetti linguaggi ricorsivamente enumerabili, le cui grammatiche includono regole nella forma \alpha \rightarrow \beta, dove α è una stringa non vuota di simboli (di cui almeno uno non terminale) e β è una stringa (eventualmente vuota) di simboli terminali e non terminali.
  • La seconda classe contiene i cosiddetti linguaggi context-sensitive, che presentano produzioni nella forma \alpha A \beta \rightarrow \alpha\gamma\beta con A \in N e le lettere greche corrispondenti a stringhe di simboli qualsiasi del vocabolario, imponendo in particolare \gamma \neq \epsilon (dove ε è la stringa nulla) con la sola eccezione della regola S \rightarrow \epsilon se S non compare nel lato destro di alcuna produzione.
  • La terza classe, che permette solo regole nella forma A \rightarrow \gamma con A \in N e γ stringa qualsiasi di simboli del vocabolario, è quella dei linguaggi context-free; si tratta di una classe molto importante per tutti gli informatici, visto che è quella cui "appartengono" i linguaggi di programmazione (più esattamente, i linguaggi context-free sono in grado di specificare adeguatamente la sintassi dei linguaggi di programmazione). Occorre notare un dettaglio: le grammatiche context-free non vietano la sostituzione di un simbolo non terminale con la stringa vuota, per cui si potrebbe mettere in dubbio l'idea che i linguaggi context-free costituiscano un sottoinsieme dei linguaggi context-sensitive; in realtà, è possibile dimostrare un lemma, noto come lemma della stringa vuota, secondo il quale ogni grammatica context-free è equivalente (definendo come "equivalenti" due grammatiche se e solo se descrivono lo stesso linguaggio) a un'altra grammatica context-free che permette le sostituzioni incriminate solo secondo le regole tipiche dei linguaggi context-sensitive o non le permette affatto.
  • La quarta classe, che permette solo produzioni nella forma A \rightarrow \beta e in una sola tra due forme A \rightarrow B\alpha e A \rightarrow \alpha B (dove come al solito le lettere maiuscole indicano simboli non terminali e le lettere greche sequenze di simboli qualsiasi del vocabolario), è quella dei linguaggi regolari. Anche i linguaggi regolari, come i linguaggi context-free, sono molto importanti nell'ambito dell'informatica, ad esempio perché permettono di descrivere i tokenizzatori dei compilatori.

Chiudiamo la nostra breve disamina rispondendo a una domanda che sicuramente, caro lettore, ti sarà spuntata in testa: dove lo mettiamo il linguaggio naturale? Si tratta di un dubbio tutt'altro che banale, perché la lingua parlata esibisce dei caratteri molto peculiari e inoltre non ne è nota in partenza la grammatica formale: non è neanche certo, in realtà, che il linguaggio naturale sia ricorsivamente enumerabile, per cui esso potrebbe non rientrare affatto nella gerarchia di Chomsky, oppure appartenere a una classe ancor più ampia di quella dei linguaggi ricorsivamente enumerabili. Non essendo il sottoscritto un esperto nel campo dell'analisi del linguaggio naturale, quanto appena esposto è tutto ciò che diremo in questi articoli sulla sua visione formale; il lettore interessato è ovviamente invitato a svolgere ricerche autonome per approfondire, magari partendo dall'apposita sezione della bibliografia proposta in [MAK88].

Interpreti

Prima di abbandonare la teoria generale dei linguaggi formali e andare a parlare dello specifico linguaggio che ci interessa, prendiamoci un minuto per discutere un aspetto di straordinaria importanza: tutte le grammatiche dei linguaggi formali sono almeno ricorsivamente enumerabili, per cui è possibile automatizzare il riconoscimento delle parole. Formalmente, quel che si fa è definire delle "macchine astratte" (dei computer "ideali", diciamo) in grado di leggere una parola carattere per carattere e dire alla fine se essa appartiene o no a un certo linguaggio; precisamente, identifichiamo tre tipi "classici" di macchine:

  • Gli automi a stati finiti (da non confondere con le macchine a stati finiti che usiamo per modellare i circuiti sequenziali: sono oggetti della stessa categoria e della stessa potenza, ma non sono la stessa cosa!), che possono riconoscere i linguaggi regolari: matematicamente, definiamo un tale automa come una tupla \mathcal{M} = (X, Q, q_0, F, \delta), dove X è l'alfabeto del linguaggio da analizzare, Q l'insieme finito degli stati in cui l'automa può trovarsi, q0 lo stato iniziale, F il sottoinsieme di Q che identifica gli stati finali (vedremo tra poco cosa sono) e δ è la funzione di transizione dello stato.
  • Gli automi push-down, che possono riconoscere i linguaggi context-free: matematicamente, li definiamo con la tupla \mathcal{M} = (X, Q, \Gamma, q_0, Z_0, F, \delta), la quale ci permette di interpretare questi automi come automi a stati finiti con in più uno stack (idealmente infinito) con simbolo iniziale Z0 e alfabeto Γ (ovvero, uno stack che ha come elemento "più in basso" Z0 e sul quale si possono scrivere solo simboli di Γ).
  • Le famosissime macchine di Turing, che sono in grado di riconoscere tutti i linguaggi ricorsivamente enumerabili... anzi no: se è vero che possiamo riconoscere tutti i linguaggi context-free e dunque in particolare tutti i linguaggi regolari (possiamo addirittura dare definizioni esplicite di entrambe le classi!), non è vero che possiamo riconoscere tutti i linguaggi ricorsivamente enumerabili. Questo è uno dei limiti più importanti dell'informatica: notando che di fatto le macchine astratte non sono altro che algoritmi e notando inoltre che secondo la tesi di Church-Turing (una dimostrazione elegantissima e molto istruttiva, quantunque molto lunga, della quale si può trovare in [BBJ07]) qualsiasi linguaggio riconoscibile può essere riconosciuto da una macchina di Turing, l'impossibilità di riconoscere alcuni linguaggi ci dice sostanzialmente che esistono dei problemi che non possono essere risolti (per i più curiosi, segnaliamo che [Sipser12] dedica un capitolo davvero ben scritto alla discussione di alcuni di questi problemi).

Come funzionano queste macchine? L'idea di principio è semplice: partendo dallo stato iniziale, ad ogni carattere che leggono le macchine cambiano il loro stato, e se alla fine dell'input hanno raggiunto uno degli stati finali allora la parola è riconosciuta come una parola del linguaggio. Ovviamente, un tale procedimento può essere "decorato" con specificità ulteriori, ed effettivamente è ciò che accade: gli automi a stati finiti si comportano esattamente come descritto, ma gli automi push-down ad esempio leggono sia il proprio ingresso sia lo stack e accettano le parole non solo se raggiungono uno stato finale, ma anche se a fine lettura lo stack risulta vuoto.
Concludiamo il nostro paragrafo osservando un attimo un semplice automa a stati finiti per un linguaggio costruito sull'alfabeto X = {0,1}:

Qui tocca a te, caro lettore: sapresti leggere questo automa, riconoscere i suoi stati iniziali e finali e identificare almeno un sottoinsieme delle parole del linguaggio che descrive?

FINALMENTE, LA LOGICA

Anzitutto, la sintassi...

Finita la nostra panoramica sulla teoria dei linguaggi formali, possiamo andare a ciò che davvero ci interessa: la logica proposizionale. Abbiamo già visto la definizione "algebrica" di un tale linguaggio, e ora lo ridefiniremo partendo dalla sua grammatica G = (N,T,P,S):

  • L'insieme dei simboli non terminali N contiene tutte le lettere maiuscole dell'alfabeto.
  • L'insieme dei simboli terminali T contiene le lettere minuscole dell'alfabeto, i valori di verità 0 e 1 e gli operatori \cdot, + e \neg; rimarchiamo (ma dovrebbe essere ovvio) che per quanto ne sappiamo fin'ora (o almeno, per quanto abbiamo codificato nella grammatica fin'ora) questi sono solo dei simboli, quindi chiamarli "valori di verità" oppure "operatori" è solo un modo per identificarli più facilmente: al momento, i nostri simboli non hanno un significato, sono solo segni grafici.
  • Assumiamo come simbolo iniziale F \in N.
  • L'insieme delle produzioni, indicando con p una generica lettera minuscola e con G e H degli elementi qualsiasi di N, consta dei seguenti elementi:

H \rightarrow  p | 0 | 1
H \rightarrow \neg H
H \rightarrow H \cdot G
H \rightarrow H + G

Ci chiediamo, ovviamente: questa grammatica permette di ottenere tutte e sole le formule ben formate secondo la nostra definizione dell'algebra di commutazione? La risposta è positiva (non avremmo proposto una grammatica sbagliata!), ma il lettore è comunque invitato a costruire qualche formula per rendersi conto da sè del risultato.

...E la semantica

A questo punto, dobbiamo dare un senso al nostro linguaggio, ovvero dobbiamo definirne la semantica; senza girarci troppo intorno, possiamo dire subito (come abbiamo fatto implicitamente quando abbiamo discusso l'approccio algebrico) a cosa vogliamo far corrispondere i simboli terminali 0, 1, \cdot, + e \neg, mentre per gli altri simboli terminali, ovvero le lettere minuscole, dobbiamo riflettere un attimo: noi vogliamo, ovviamente, che questi simboli rappresentino delle frasi dichiarative del tipo "oggi c'è il sole", giusto?
La risposta a questa domanda è interessante, perché per la prima volta ci mette davvero di fronte - in qualche modo - al problema dell'espressività: cosa vogliamo e possiamo dire nel nostro linguaggio? Quando mettiamo insieme delle parole, di cosa esattamente stiamo parlando? Notiamo subito un dettaglio molto importante: il nostro linguaggio non include verbi, articoli e sostantivi, quindi la frase "oggi c'è il sole" non possiamo dirla... ma allora, di che parliamo quando parliamo di logica proposizionale (ciao, Raymond Carver)?
La risposta è semplice, ma talmente importante da meritare di essere evidenziata ogni qual volta si presenti l'occasione: la logica proposizionale parla della verità. In altri termini: quando esprimiamo una formula proposizionale, quel che stiamo dicendo è che una certa concatenazione di proposizioni è vera o falsa, null'altro. Piuttosto astratto, vero? Ecco perché è prassi comune, quando si definisce informalmente il significato delle formule logiche, associare alle proposizioni delle frasi dichiarative: perché il linguaggio naturale è qualcosa che possiamo intuitivamente capire, è qualcosa di molto vicino a noi e alla nostra esperienza quotidiana, mentre le formule proposizionali non lo sono, per cui ben venga l'associazione, a patto che non si dimentichi la realtà dei fatti: l'associazione tra proposizioni logiche e frasi dichiarative è arbitraria, per nulla intrinseca nel linguaggio formale che stiamo trattando.
Puntualizzato ciò che bisognava puntualizzare, torniamo a noi: come la definiamo la semantica della logica proposizionale? Semplice: assegnando un valore di verità alle formule proposizionali! E come lo facciamo? Suvvia caro lettore, non far dire tutto all'autore, sai bene dove vogliamo arrivare: lo facciamo con le tavole di verità! Diciamolo formalmente: la semantica della logica proposizionale è data dalle tavole di verità, le quali stabiliscono quando la congiunzione, la disgiunzione e la negazione di proposizioni sono vere, e di conseguenza permettono di derivare ricorsivamente il valore di verità di qualsiasi formula proposizionale.
A questo punto, per dare un senso a una qualche formula \mathcal{F} dobbiamo solo assegnare un valore di verità alle sue proposizioni "atomiche": definiamo interpretazione \mathcal{I} di \mathcal{F} un tale assegnamento, e se quest'assegnamento è tale da rendere vera la formula stessa diciamo che \mathcal{I} è un modello semantico di \mathcal{F}, e scriviamo \mathcal{I} \models \mathcal{F}; caro lettore, ti ricorda niente tutto questo?

Bene... e adesso?

Perfetto, ora abbiamo il nostro linguaggio formale con la sua sintassi e la sua semantica... e che ci facciamo, con 'sto linguaggio che parla di verità? Ma è ovvio, caro lettore: ci dimostriamo cose! Se il nostro linguaggio è in grado di dirci, partendo dall'assegnazione di un valore di verità alle proposizioni atomiche, quando una certa formula è vera, cosa ci impedisce di dare alle proposizioni di una formula Φ il valore di verità di certi risultati matematici (che praticamente, nella nostra associazione informale, vuol dire far corrispondere alle proposizioni gli enunciati di tali risultati) e utilizzare le regole della logica per provare che \Phi \vdash \Psi, e cioè che a partire dal risultato matematico Φ si può dimostrare un altro risultato matematico Ψ?
Ovviamente, non c'è un solo approccio alla dimostrazione, e comunque l'intero discorso si espone a non banali considerazioni di carattere filosofico... noi non discuteremo tali implicazioni (pur invitando caldamente il lettore interessato a consultare [Berto07] per farsi un'idea della situazione) e passeremo direttamente a vedere una tabella (tratta da [HR04]) che mostra le regole delle nostre dimostrazioni, secondo l'idea del calcolo della deduzione naturale formulato dal matematico tedesco G.K.E. Gentzen:

Per poter comprendere pienamente il senso di tutto ciò, puntualizziamo alcuni dettagli:

  • Le regole della deduzione naturale sono divise in regole d'introduzione (le quali introducono una nuova operazione nella formula) e regole d'eliminazione (le quali, ovviamente, eliminano un'operazione presente nella formula).
  • La scrittura tipicamente adottata per le regole deduttive prescrive di mettere sopra le premesse che si assumono vere e sotto la conseguenza di tale assunzione: la regola d'introduzione per la congiunzione, ad esempio, può essere letta come "se Φ è vera e lo è anche ψ, allora \Phi \cdot \psi è vera a sua volta".
  • Le sequenze entro riquadri indicano delle dimostrazioni: la regola d'introduzione della negazione, ad esempio, può essere letta come "se si può dimostrare in qualche modo che la formula Φ è falsa, allora la formula \neg\Phi è vera".

Si invita caldamente il lettore a leggere attentamente tutte le regole e cercare di dar loro un senso, se è il caso ricorrendo ad associazioni con il linguaggio naturale: è un esercizio molto istruttivo e senz'altro in grado di ispirare interessanti riflessioni circa l'approccio umano al ragionamento e alla comunicazione; in ogni caso, il lettore pigro può trovare una spiegazione molto ben realizzata di ciascuna delle regole logiche proposte nella tabella (e anche di alcune regole "derivate") in [HR04] e anche in [Berto07].

IL PROBLEMA DELLA SODDISFACIBILITÀ

Introduzione

Dato che il nostro linguaggio parla di verità, ovviamente ci interessa sapere se una qualsiasi formula, non importa quanto complessa, sia vera o falsa... ma non sempre questo risultato è facile da ottenere: le tavole di verità possono essere usate esplicitamente solo per funzioni semplici, e in generale il teorema di Cook-Levin stabilisce che determinare un'interpretazione in grado di soddisfare una certa formula è un problema i cui tempi di risoluzione esplodono al crescere della dimensione della formula trattata.
Tutto è perduto, quindi? Non esattamente: come spesso accade, trattare casi particolari dei problemi aiuta a semplificarne la risoluzione in modo determinante. Nel caso di nostro interesse, è stato determinato che è spesso possibile risolvere in tempi accettabili il problema della soddisfacibilità rappresentando le formule proposizionali con la loro conjunctive normal form, ovvero come congiunzione di disgiunzioni (dette clause) di letterali. Vediamo un esempio per capire bene: data la formula proposizionale \alpha = a \cdot b, la sua CNF è la formula \gamma = (\neg a + \neg b + \alpha)(a + \neg \alpha)(b + \neg \alpha), la quale risulta vera se e solo se le tre variabili a, b e α assumono i valori dati dalla formula originale \alpha = a \cdot b. In generale, per ricavare la CNF di una formula si agisce come segue:

  1. Data la formula α = f(a,b,...,k), si disegna una mappa di Karnaugh contenente sia le variabili d'ingresso sia la variabile d'uscita, e si inseriscono degli 1 in corrispondenza delle configurazioni che descrivono la funzione.
  2. Si effettua la copertura inversa della mappa di Karnaugh, ovvero si coprono gli 0 anziché gli 1.
  3. Si disgiungono i termini identificati e si nega il risultato.
  4. Si sviluppa quanto ottenuto, arrivando in fine alla CNF voluta.

Vediamo, giusto per spiegarci, il semplice esempio della formula c = a\cdot b, così ne approfittiamo per dimostrare l'esempio che abbiamo visto poche righe fa: la tavola di verità della funzione ci dice che c = 1 se e solo se a = b = 1, per cui la funzione è descritta dalle tuple (a,b,c) = {(0,0,0),(1,0,0),(0,1,0),(1,1,1)}; a questo punto, la sua mappa risulta la seguente:

La "copertura inversa" di questa mappa riporta gli implicanti \overline{a}c, \overline{b}c e ab\overline{c}, per cui possiamo dire che la nostra funzione è descritta dalla formula \overline{(\overline{a}c + \overline{b}c + ab\overline{c})}; sviluppando questa formula (compito puramente meccanico, applicando la legge di De Morgan), si arriva alla scrittura (\overline{a} + \overline{b} + c)(a + \overline{c})(b + \overline{c}), la quale è la CNF di c = a\cdot b.

L'algoritmo DPLL

Dunque, abbiamo detto che rappresentando una formula proposizionale con la sua CNF possiamo determinarne la soddisfacibilità in modo semplice e tendenzialmente efficiente... vediamo come fare:

  1. Si pone una variabile della CNF a 1.
  2. Si eliminano tutte le clause che risultano vere.
  3. Si pongono a 1 tutte le variabili che costituiscono da sole una clause, perché necessariamente esse devono essere vere se vogliamo soddisfare la nostra formula; questo processo di "propagazione" delle assunzioni di verità si chiama boolean constraint propagation.
  4. Si ripete il processo finché non si arriva a un valore di verità per la formula: se è 1, allora l'abbiamo soddisfatta e in particolare abbiamo trovato un'interpretazione (quella composta dai valori di verità che abbiamo assegnato) in grado di soddisfarla, mentre se il valore di verità ottenuto è 0 occorre fare un passo indietro e ri-assegnare qualche valore.

Tutto qui: semplicemente, assegniamo dei valori di verità finché non troviamo un'interpretazione che risolva il nostro problema (o finché non determiniamo l'inesistenza di un'interpretazione in grado di farlo). Questo algoritmo, che è il celeberrimo algoritmo di Davis-Putnam-Logemann-Loveland, è alla base di gran parte del lavoro svolto negli ultimi decenni per sviluppare dei SAT solver (ovvero, dei programmi in grado di determinare la soddisfacibilità delle formule) efficienti. Giusto per fare un attimo il punto, vediamo graficamente come funziona l'algoritmo per una semplice CNF:

Sviluppi recenti

L'algoritmo DPLL è intuitivo e tutto sommato abbastanza semplice, ma è tutt'altro che perfetto: per cominciare, le sue prestazioni dipendono fortemente dalla scelta delle variabili su cui lavorare, e inoltre si tratta di un algoritmo sostanzialmente "stupido", che potenzialmente durante il suo lavoro è in grado di assegnare ripetutamente un certo valore a una variabile pur avendo avuto modo di "notare" che ciò basta a rendere insoddisfacente l'interpretazione. Alla luce di tutto ciò, non stupirà il lettore che molto si sia fatto e scritto al fine di migliorare l'algoritmo e renderlo più efficiente; vediamo due delle soluzioni che sono state formulate:

  • Al fine di rendere "intelligente" l'algoritmo, sono comparse in letteratura delle sue versioni in grado di compiere il cosiddetto conflict-driven learning, e cioè in grado di "imparare" dal lavoro precedentemente svolto e dunque scartare in partenza tutte le strade che evidentemente non possono portare a una soluzione. Tendenzialmente, quel che succede in queste versioni dell'algoritmo è che, quando si determina che una carta interpretazione rende falsa la formula in esame, si aggiunge a tale forma una conflict clause, ovvero una clause che permetta di "far notare" immediatamente all'algoritmo quando sta imboccando un vicolo cieco già visitato in precedenza. Un esempio di algoritmo DPLL con conflict-driven learning è quello riportato in [CCK03] ed effettivamente utilizzato dal solver CHAFF.
  • Al fine di determinare quali variabili selezionare per prime, sono state proposte varie figure di merito in grado di classificare le variabili in base alla loro importanza; una di queste metriche è la cosiddetta metrica di Jeroslow-Wang, che assegna al letterale x un punteggio determinato sulla base delle sue occorrenze nelle varie clause Ci della formula in esame, pesate sulla base della loro lunghezza; precisamente, la metrica di Jeroslow-Wang è calcolata con la formula J(x) = \sum_{i \; | \; x \in C_i}2^{-|C_i|}. Sulla base di questa metrica, in [DK06] è stato definito un algoritmo di classificazione delle variabili in grado di migliorare sensibilmente le prestazioni del SAT solver CHAFF su un certo numero di test case standard.

BIBLIOGRAFIA

[Berto07] F. Berto, Logica da zero a Gödel, Editori Laterza, 2007
[BBJ07] G.S. Boolos, J.P. Burgess, R.C. Jeffrey, Computability and logic, Cambridge University Press, 2007
[Bourbaki89] N. Bourbaki, Algebra I, Springer, 1989
[CCK03] P. Chauhan, E.M. Clarke, D. Kroening, Using SAT-based image computation for reachability analysis, Technical Report CMU-CS-03-151, Carnegie Mellon University, 2003
[DLDA13] A. De Luca, F. D'Alessandro, Teoria degli automi finiti, Springer, 2013
[DK06] V. Durairaj, P. Kalla, Guiding CNF-SAT search by analyzing constraint-variable dependencies and clause lengths, in Proceedings of the 11th annual IEEE International High-Level Design Validation and Test Workshop, 2006, pp.155-161
[HMU07] J.E. Hopcroft, R. Motwani, J.D. Ullman, Introduction to automata theory, languages and computation, Addison-Wesley, 2007
[HR04] M. Huth, M. Ryan, Logic in computer science, Cambridge University Press, 2004
[MAK88] R.N. Moll, M.A. Arbib, A.J. Kfoury, An introduction to formal language theory, Springer, 1988
[Sipser12] M. Sipser, Introduction to the theory of computation, Thomson Course Technology, 2012

5

Commenti e note

Inserisci un commento

di ,

Mi suscita ricordi di tanti anni fa.

Rispondi

di ,

I limiti esistono per essere superati :) Se hai tempo magari provaci: non sono cose difficili quelle di cui parlo in quest'articolo, ma fanno riflettere ;)

Rispondi

di ,

ma no assolutamente non è colpa tua, è che dopo l'università ho avuto poche occasioni di usare quanto imparato sui libri.... Altri più ferrati potranno dare un giudizio più autorevole sui tuoi articoli, il mio era solo uno sfogo sui miei limiti.

Rispondi

di ,

Potresti iniziare dai due articoli che ho scritto prima di questo: le premesse son tutte lì :) E se anche leggendo quegli articoli non capisci bene alcune cose... beh, fammelo sapere e per favore sii molto dettagliato, perché probabilmente c'è qualche aspetto del mio modo di spiegare le cose che va rivisto ;)

Rispondi

di ,

Un voto per l'impegno, ma per me è arabo mi servirebbe un corso base ;-)

Rispondi

Inserisci un commento

Per inserire commenti è necessario iscriversi ad ElectroYou. Se sei già iscritto, effettua il login.