Valutazione attuale: 5 / 5

Stella attivaStella attivaStella attivaStella attivaStella attiva
 
SAT

 

AMBITO: Matematica
STATO:  ATTIVO 
VOTO: ( N.P. )

 

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.



Per commentare questo post nel forum devi effettuare il login

Articoli

Written on 21/05/2018, 21:55 by boboviz
nuovo-client-boinc-7-10-2Oggi è stato ufficialmente rilasciato il nuovo client Boinc, la versione 7.10.2 Qui la lista delle modifiche rispetto alla versione precedente.

Ultime dal Blog

Written on 19/06/2017, 14:38 by boboviz
addio-lugano-bellaCari sodali scaccolatori,come alcuni di voi sanno, il sottoscritto, oltre ad essere appassionato di Boinc, è anche "appassionato" di HPC e, visto che il...