Indice articoli

Valutazione attuale: 5 / 5

Stella attivaStella attivaStella attivaStella attivaStella attiva
 
SAT

 

AMBITO: Matematica
STATO:CHIUSO

 

SAT@home è un progetto di ricerca che utilizza computer connessi a Internet per risolvere problemi difficili e praticamente importanti (problemi di inversione di funzioni discrete, ottimizzazione discreta, bioinformatica, ecc.) Che possono essere efficacemente ridotti al problema di soddisfacibilità booleana. Al momento stiamo risolvendo il problema della ricerca di coppie ortogonali di quadrati latini diagonali di ordine 9 e 10. Nel prossimo futuro speriamo di trovare la tripla di quadrati latini mutuamente ortogonali di ordine 10 o di dimostrare l'assenza di tali triple. Il progetto è stato implementato usando la libreria DC-API.
 Ci sono molti problemi praticamente importanti per i quali non è stata dimostrata l'esistenza di algoritmi (polinomiali) efficaci della loro risoluzione.  Molti di questi problemi sono NP-hard. Significa che sotto alcune supposizioni ragionevoli (anche se non provate), questi problemi non possono essere risolti in tempo polinomiale. Tuttavia, molti dei loro casi speciali si presentano in applicazioni pratiche: vari problemi di ottimizzazione discreti (ad esempio, pianificazione della produzione) e problemi di verifica dei dispositivi discreti (derivanti, ad esempio, dalla progettazione di circuiti e dalla verifica della correttezza del programma). Pertanto è molto importante avere metodi per la loro risoluzione che non hanno complessità polinomiale, ma che sono efficaci nella pratica: tali metodi possono far fronte ai numerosi casi speciali di problemi NP-hard di dimensioni enormi. Uno dei metodi più semplici nella sua base, e quindi il più efficiente in termini di implementazioni software, è l'approccio SAT. Questo approccio è basato sulla riducibilità del problema originale ad un Boolean satisfiability problem (SAT). I problemi SAT ammettono una forma molto naturale di parallelismo, consentendo l'uso del calcolo distribuito (incluso il calcolo volontario) per risolverli. In realtà la riduzione al SAT può essere effettuata in modo efficace (in effetti, deriva dal famoso teorema di Cook-Levin).

Pertanto, il progetto è finalizzato alla risoluzione di vari problemi combinatori difficili (dalle aree di crittografia, ottimizzazione discreta, bioinformatica) che possono essere efficacemente ridotti a SAT.
 

 

Per ulteriori informazioni visitate il thread ufficiale presente nel nostro forum.


Accedi per commentare