Metodi Formali nell'Ingegneria del Software

Progetti svolti dagli studenti

Torna alla lista dei progetti »

Risolutori SAT non-CNF

• Autori:

• Categorie: Logica proposizionale; Risolutori SAT; Verifica di algoritmi, programmi, protocolli e hw; Sintesi automatiche di soluzioni

Sommario

L'obiettivo di questa tesina è quello di far conoscere il panorama, per lo più ancora acerbo, dei risolutori SAT non clausali, ovvero risolutori che operano su formule booleane non Cnf, attraverso un excursus che va dallo studio di alcuni formati, come l'EDIMACS e L'ISCAS, mediante la generazione automatica di istanze di problemi visti a lezione (ShopScheduling, Rostering e HamiltonVipCicle), per poi passare ad un'analisi sulle prestazioni di questi risolutori, confrontandoli anche con risolutori di tipo Cnf, come MiniSat, BerkMin, ... Per concludere infine mostriamo in grandi linee, fornendo una rapida descrizione di sintassi e semantica, un nuovo formato, l'AIGER, nato in questi ultimi anni (2006/2007) che pian piano si sta imponendo nel mondo dei risolutori non-clausal per formule non-cnf senza perdita di struttura.

Materiale prodotto

• Relazione

• Codice

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.