>   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

Logica proposizionale

Dispense del corso

Codice Descrizione
D.II.1 Logica proposizionale

Programmi disponibili

Nome Descrizione
javaSAT Semplice risolutore SAT basato su backtracking (solo per scopi didattici)
zChaff Risolutore SAT basato su DPLL e clause learning
BG-Walksat Risolutore SAT incompleto basato su tecniche di ricerca locale

Esempi di encoder di problemi combinatori in SAT

Problema Descrizione
Queens2SAT Encoder del problema N-queens in SAT

Esercizi

Codice Descrizione Soluzione
E.II.20070320 Quadrato magico --
E.II.20070723 Schur's lemma Download
E.II.20080110 Ramsey problem --
E.II.20070711 Social golfer Download
E.II.20080703 Shop Scheduling Download
E.II.20080718 Rostering Download
E.II.20080918 Ciclo Hamiltoniano con priorità Download
E.II.20090116 Langford's numbers --

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