SAT@home

Aktuální verze stránky ještě nebyla zkontrolována zkušenými přispěvateli a může se výrazně lišit od verze recenzované 16. května 2018; kontroly vyžadují 5 úprav .
SAT@Home
Plošina BOINC
Velikost stahování softwaru 10 MB
Velikost načtených dat úlohy 2 kB
Množství odeslaných dat úlohy 20 kB
Místo na disku 10 MB
Využité množství paměti 80 MB
GUI Ne
Průměrná doba výpočtu úkolu až 5 hodin
Uzávěrka 10 dní
Schopnost používat GPU Ne

SAT@home je ruský dobrovolnický počítačový projekt na platformě BOINC , který byl spuštěn v září 2011 [1] . Vědeckým cílem projektu je řešení diskrétních problémů jejich redukcí na problém splnitelnosti booleovských vzorců (SAT, z angl.  Satisfiability - proveditelnost) v konjunktivní normální formě (CNF). Nalezení řešení zvoleného problému se provádí pomocí jednoho ze známých SAT řešitelů, který implementuje algoritmus DPLL . Projekt je podporován Laboratoří diskrétní analýzy a aplikované logiky Ústavu systémové dynamiky a teorie řízení Sibiřské pobočky Ruské akademie věd a Centrem distribuovaných výpočtů Ústavu pro problémy přenosu informací . K 19. září 2014 se projektu zúčastnilo 18394 počítačů 7239 uživatelů ze 124 zemí, které poskytovaly výkon asi 3,1 teraflopu [ 2] . Projektu se může zúčastnit kdokoli, kdo má počítač s přístupem na internet , a to tak, že si na něj nainstaluje program BOINC .

Historie projektu

Výpočty v rámci projektu byly zahájeny [3] v září 2011 řešením problému kryptoanalýzy generátoru A5/1 používaného v GSM komunikacích. Podle známého fragmentu toku klíčů bylo nutné určit inicializační sekvenci, tedy počáteční naplnění registrů generátoru . Účelem výpočtů bylo prokázat použitelnost SAT přístupu k řešení tohoto problému pro případy, kdy není možné najít řešení jinými metodami (např. pomocí duhových tabulek ). Na základě výpočtů bylo do května 2012 vyřešeno 10 testovacích problémů kryptoanalýzy A5/1 [4] .

V červnu 2012 byl zahájen nový experiment, jehož účelem bylo hledání ortogonálních dvojic diagonálních latinských čtverců řádu 9. Do srpna 2012 bylo nalezeno 134 dvojic, které prokázaly použitelnost tohoto přístupu k problému. Následně byl zahájen experiment na hledání ortogonálních dvojic diagonálních latinských čtverců řádu 10. Výsledkem výpočtů bylo dosud nalezeno 13 dvojic latinských čtverců [4] , které se neshodují se známými danými dvojicemi. v článku [5] .

Vědecké úspěchy

rok 2012 rok 2013

Projekt podle všeho v roce 2016 zanikl.

Poznámky

  1. ↑ SAT@Home . Datum přístupu: 26. prosince 2012. Archivováno z originálu 21. prosince 2012.
  2. ↑ Podrobné statistiky SAT@home . Získáno 5. září 2013. Archivováno z originálu 11. srpna 2013.
  3. ↑ Archiv zpráv SAT@home (stahovací odkaz) . Datum přístupu: 26. prosince 2012. Archivováno z originálu 4. ledna 2013. 
  4. ↑ 1 2 3 4 Nalezena řešení SAT@home (odkaz není k dispozici) . Datum přístupu: 26. prosince 2012. Archivováno z originálu 21. prosince 2012. 
  5. ↑ Brown a kol. Dokončení spektra ortogonálních diagonálních latinských čtverců. Přednášky z čisté a aplikované matematiky. 1992 sv. 139. S. 43–49.

Odkazy