>   Dipartimento di Informatica   >   Toni Mancini
[login|nuovo account]      [Italiano|English]

Laurea Specialistica in Ingegneria Informatica, Corso di

Metodi Formali nell'Ingegneria del Software

Edizione dell'a.a. 2007/08

Progetti svolti dagli studenti

Torna alla lista dei progetti »


Existential second order logic e sue applicazioni

  • Autori: , ,

  • Categorie: Logica del primo ordine; Logica del secondo ordine; Risolutori SAT; Sintesi automatiche di soluzioni

Sommario

La prima parte di questo lavoro si propone di presentare una logica molto espressiva, la Logica del Secondo Ordine, applicata (nel suo frammento esistenziale, ESO) al contesto della Programmazione Dichiarativa, in particolare alla modellazione di problemi combinatori. In particolare, viene inizialmente fornita un'introduzione alla Logica del Secondo Ordine, con particolare riguardo a sintassi e semantica e differenze rispoetto alla FOL, e successivamente si restringe l'attenzione al suo frammento che fa uso del solo quantificatore esistenziale per quantificare simboli di predicato. Viene posta particolare attenzione agli ambiti di applicazione di tale linguaggio e vengono forniti poi diversi esempi di problemi combinatori modellati in ESO. Inoltre vengono descritte alcune importanti proprietà di specifiche di problemi: le dipendenze funzionali tra predicati. Come si vedrà, la conoscenza di tali proprietà può giocare un ruolo molto importante nell'efficienza del processo di risoluzione.
Vengono poi messi a confronto diversi linguaggi e formalismi con ESO, ovvero il linguaggio di modellazione OPL e il framework dei Constraint Satisfaction Problem (CSP), e vengono mostrate differenze e analogie. Infine si introducono le attuali tecniche "furbe" di istanzione in SAT, prestando particolare attenzione a quello che avviene in Spec2SAT. Viene inoltre illustrato come le dipendenze funzionali tra predicati della specifica si traducono in dipendenze funzionali tra le corrispondenti variabili proposizionali, che si sommano alle altre dipendenze funzionali derivate ad esempio dall'introduzione di nuove variabili durante la traduzione dell'istanza in CNF.
Nella seconda parte si assume di avere creato un'istanza proposizionale di tali problemi comprensiva di una struttura che indica le dipendenze funzionali tra le variabili. Viene dunque presentata la versione modificata di un moderno solver "state-of-the-art" (Minisat - vincitore nella competizione SAT Race 2006) che evita di scegliere variabili funzionalmente dipendenti in fase di branching quando la lista di quelle indipendenti non è ancora esaurita. Le prestazioni del solver modificato vengono messe a confronto con quelle del solver originale. Infine viene fornita una panoramica delle moderne tecniche di risoluzione di istanze proposizionali, seguendo lo sviluppo storico attraverso le innovazioni di 2 SAT solver che hanno rivoluzionato la ricerca in questo campo, ovvero GRASP e zChaff, e indicando come tali tecniche vengano utilizzate in Minisat.

Materiale prodotto


Disclaimer: Questo materiale viene offerto gratuitamente ai soli studenti del corso di Metodi Formali nell'Ingegneria del Software del Corso di Laurea Specialistica in Ing. Informatica dell'Università degli Studi di Roma "La Sapienza". E' vietato ogni utilizzo diverso da quello inerente la preparazione dell'esame del suddetto corso, ed in particolare è espressamente vietato il suo utilizzo per qualsiasi scopo commerciale e/o di lucro.

Questo materiale è stato prodotto da un gruppo di studenti del predetto corso, e viene pubblicato senza alcuna garanzia, da parte del docente, circa la sua correttezza e completezza.

Il copyright di questo materiale è detenuto congiuntamente dagli autori e dal docente.
E' permessa la libera copia di tutto il materiale disponibile, purché ne vengano rispettate le condizioni d'uso qui enunciate, ne venga sempre citata la fonte, e venga riportato questo testo.
Gli autori consentono la stampa di questo materiale da parte di società di servizi (ad es. copisterie), purché queste non ne ottengano alcun ricavo oltre quello dovuto alla vendita di semplici fotocopie a prezzi di mercato. Si precisa tuttavia che gli autori ed il docente non percepiscono alcun guadagno dalla diffusione del materiale da parte di chiunque.



[This web site could never be realised without the sophisticated features of a pure text editor and the extreme power of 220V]