SAT@home

Den aktuelle version af siden er endnu ikke blevet gennemgået af erfarne bidragydere og kan afvige væsentligt fra den version , der blev gennemgået den 16. maj 2018; checks kræver 5 redigeringer .
SAT@Home
Platform BOINC
Software download størrelse 10 MB
Jobdata indlæst størrelse 2 KB
Mængden af ​​sendt jobdata 20 KB
Diskplads _ 10 MB
Brugt mængde hukommelse 80 MB
GUI Ingen
Gennemsnitlig opgaveberegningstid op til 5 timer
deadline 10 dage
Mulighed for at bruge GPU Ingen

SAT@home er et russisk frivilligt computerprojekt på BOINC platformen , lanceret i september 2011 [1] . Det videnskabelige mål med projektet er at løse diskrete problemer ved at reducere dem til problemet med tilfredsstillelse af booleske formler (SAT, fra engelsk.  Satisfiability - feasibility) i konjunktiv normalform (CNF). At finde en løsning på det valgte problem udføres ved hjælp af en af ​​de velkendte SAT-løsere, der implementerer DPLL-algoritmen . Projektet er støttet af Laboratory of Discrete Analysis and Applied Logic fra Institute of System Dynamics and Control Theory i den sibiriske afdeling af det russiske videnskabsakademi og Center for Distributed Computing ved Instituttet for Informationstransmissionsproblemer . Den 19. september 2014 deltog 18394 computere af 7239 brugere fra 124 lande i projektet, hvilket leverede en ydeevne på omkring 3,1 teraflops [ 2] . Alle, der har en computer med internetadgang , kan deltage i projektet ved at installere BOINC -programmet på den .

Projekthistorie

Beregninger inden for rammerne af projektet startede [3] i september 2011 med løsningen af ​​problemet med krypteringsanalyse af A5/1 -generatoren, der anvendes i GSM - kommunikation. Ifølge det kendte fragment af nøglestrømmen var det nødvendigt at bestemme initialiseringssekvensen, det vil sige den indledende udfyldning af generatorregistrene . Formålet med beregningerne var at bevise anvendeligheden af ​​SAT-tilgangen til at løse dette problem i de tilfælde, hvor det er umuligt at finde en løsning med andre metoder (for eksempel ved brug af regnbuetabeller ). Som et resultat af beregninger, i maj 2012, var 10 testproblemer af kryptoanalyse A5/1 [4] løst .

I juni 2012 blev et nyt eksperiment lanceret, hvis formål var at søge efter ortogonale par af diagonale latinske kvadrater af orden 9. I august 2012 var der fundet 134 par, hvilket beviste anvendeligheden af ​​denne tilgang til problemet. I forlængelse heraf blev der igangsat et eksperiment for at søge efter ortogonale par af diagonale latinske kvadrater af orden 10. Som resultat af beregningerne er der indtil videre fundet 13 par latinske kvadrater [4] , som ikke er sammenfaldende med de kendte par givet. i artiklen [5] .

Videnskabelige resultater

år 2012 år 2013

Tilsyneladende ophørte projektet med at eksistere i 2016.

Noter

  1. ↑ SAT@Home . Dato for adgang: 26. december 2012. Arkiveret fra originalen 21. december 2012.
  2. ↑ SAT@home detaljeret statistik . Hentet 5. september 2013. Arkiveret fra originalen 11. august 2013.
  3. ↑ SAT@home nyhedsarkiv (downlink) . Dato for adgang: 26. december 2012. Arkiveret fra originalen 4. januar 2013. 
  4. ↑ 1 2 3 4 SAT@home-løsninger fundet (link ikke tilgængeligt) . Dato for adgang: 26. december 2012. Arkiveret fra originalen 21. december 2012. 
  5. ↑ Brown et al. Færdiggørelse af spektret af ortogonale diagonale latinske firkanter. Forelæsningsnotater i ren og anvendt matematik. 1992 bind. 139. S. 43-49.

Links