SAT@acasă

Versiunea actuală a paginii nu a fost încă revizuită de colaboratori experimentați și poate diferi semnificativ de versiunea revizuită pe 16 mai 2018; verificările necesită 5 modificări .
SAT@Home
Platformă BOINC
Dimensiunea de descărcare a software -ului 10 MB
Dimensiunea datelor încărcate de job 2 KB
Cantitatea de date despre job trimisă 20 KB
Spațiu pe disc 10 MB
Cantitatea de memorie folosită 80 MB
GUI Nu
Timp mediu de calcul al sarcinii până la 5 ore
termen limita 10 zile
Abilitatea de a utiliza GPU Nu

SAT@home este un proiect de calcul voluntar rus pe platforma BOINC , lansat în septembrie 2011 [1] . Scopul științific al proiectului este de a rezolva probleme discrete prin reducerea acestora la problema satisfacabilității formulelor booleene (SAT, din engleză.  Satisfiability - feasibility) în formă normală conjunctivă (CNF). Găsirea unei soluții la problema selectată se realizează folosind unul dintre binecunoscutele soluții SAT care implementează algoritmul DPLL . Proiectul este susținut de Laboratorul de analiză discretă și logică aplicată al Institutului de dinamică a sistemelor și teoria controlului filialei din Siberia a Academiei Ruse de Științe și de Centrul de calcul distribuit al Institutului pentru probleme de transmisie a informațiilor . Începând cu 19 septembrie 2014, la proiect au participat 18394 de computere a 7239 de utilizatori din 124 de țări, oferind o performanță de aproximativ 3,1 teraflopi [ 2] . Oricine are un computer cu acces la Internet poate participa la proiect instalând pe acesta programul BOINC .

Istoricul proiectului

Calculele din cadrul proiectului au început [3] în septembrie 2011 cu soluționarea problemei criptoanalizei generatorului A5/1 utilizat în comunicațiile GSM . Conform fragmentului cunoscut al fluxului de chei, a fost necesar să se determine secvența de inițializare, adică umplerea inițială a registrelor generatorului . Scopul calculelor a fost acela de a demonstra aplicabilitatea abordării SAT pentru rezolvarea acestei probleme pentru acele cazuri în care este imposibil să se găsească o soluție prin alte metode (de exemplu, folosind tabelele curcubeu ). Ca urmare a calculelor, până în mai 2012 au fost rezolvate 10 probleme de testare ale criptoanalizei A5/1 [4] .

În iunie 2012, a fost lansat un nou experiment, al cărui scop a fost căutarea perechilor ortogonale de pătrate latine diagonale de ordinul 9. Până în august 2012 au fost găsite 134 de perechi, ceea ce a dovedit aplicabilitatea acestei abordări la problema. În urma acesteia, a fost lansat un experiment de căutare a perechilor ortogonale de pătrate latine diagonale de ordinul 10. În urma calculelor, au fost găsite până acum 13 perechi de pătrate latine [4] care nu coincid cu perechile cunoscute date. în articolul [5] .

Realizări științifice

anul 2012 anul 2013

Aparent, proiectul a încetat să mai existe în 2016.

Note

  1. ↑ SAT@Home . Data accesului: 26 decembrie 2012. Arhivat din original pe 21 decembrie 2012.
  2. ↑ Statistici detaliate SAT@home . Preluat la 5 septembrie 2013. Arhivat din original la 11 august 2013.
  3. ↑ Arhiva de știri SAT@home (link în jos) . Data accesului: 26 decembrie 2012. Arhivat din original pe 4 ianuarie 2013. 
  4. ↑ 1 2 3 4 SAT@home soluții găsite (link nu este disponibil) . Data accesului: 26 decembrie 2012. Arhivat din original pe 21 decembrie 2012. 
  5. ↑ Brown și colab. Completarea spectrului de pătrate latine diagonale ortogonale. Note de curs de matematică pură și aplicată. 1992 Vol. 139. Pg 43–49.

Link -uri