SAT@home

Den aktuella versionen av sidan har ännu inte granskats av erfarna bidragsgivare och kan skilja sig väsentligt från versionen som granskades den 16 maj 2018; kontroller kräver 5 redigeringar .
SAT@Home
Plattform BOINC
Storlek för nedladdning av programvara 10 MB
Job Data Loaded Storlek 2 KB
Mängd jobbdata som skickats 20 KB
Diskutrymme _ 10 MB
Använd mängd minne 80 MB
GUI Nej
Genomsnittlig tid för uppgiftsberäkning upp till 5 timmar
deadline 10 dagar
Möjlighet att använda GPU Nej

SAT@home är ett ryskt volontärprojekt på BOINC-plattformen , som lanserades i september 2011 [1] . Det vetenskapliga målet med projektet är att lösa diskreta problem genom att reducera dem till problemet med tillfredsställelse av booleska formler (SAT, från engelskan.  Satisfiability - feasibility) i konjunktiv normalform (CNF). Att hitta en lösning på det valda problemet utförs med en av de välkända SAT-lösarna som implementerar DPLL-algoritmen . Projektet stöds av Laboratory of Discrete Analysis and Applied Logic vid Institute of System Dynamics and Control Theory, Siberian Branch of Russian Academy of Sciencesoch Center for Distributed Computing vid Institutet för informationsöverföringsproblem . Den 19 september 2014 deltog 18394 datorer av 7239 användare från 124 länder i projektet, vilket gav en prestanda på cirka 3,1 teraflops [ 2] . Alla som har en dator med tillgång till Internet kan delta i projektet genom att installera programmet BOINC på den .

Projekthistorik

Beräkningar inom ramen för projektet startade [3] i september 2011 med lösningen av problemet med kryptoanalys av A5/1 -generatorn som används i GSM- kommunikation. Enligt det kända fragmentet av nyckelströmmen krävdes det att bestämma initialiseringssekvensen, det vill säga den initiala fyllningen av generatorregistren . Syftet med beräkningarna var att bevisa tillämpligheten av SAT-metoden för att lösa detta problem i de fall då det är omöjligt att hitta en lösning med andra metoder (till exempel med regnbågstabeller ). Som ett resultat av beräkningar, i maj 2012, löstes 10 testproblem av kryptoanalys A5/1 [4] .

I juni 2012 lanserades ett nytt experiment, vars syfte var att söka efter ortogonala par av diagonala latinska kvadrater av ordningen 9. I augusti 2012 hade 134 par hittats, vilket bevisade tillämpbarheten av detta tillvägagångssätt på problemet. Efter detta inleddes ett experiment för att söka efter ortogonala par av diagonala latinska kvadrater av ordningen 10. Som ett resultat av beräkningarna har man hittills hittat 13 par latinska kvadrater [4] som inte sammanfaller med de kända paren som ges i artikeln [5] .

Vetenskapliga landvinningar

år 2012 år 2013

Tydligen upphörde projektet att existera 2016.

Anteckningar

  1. ↑ SAT@Home . Datum för åtkomst: 26 december 2012. Arkiverad från originalet 21 december 2012.
  2. ↑ SAT@home detaljerad statistik . Hämtad 5 september 2013. Arkiverad från originalet 11 augusti 2013.
  3. ↑ SAT@home nyhetsarkiv (nedlänk) . Datum för åtkomst: 26 december 2012. Arkiverad från originalet den 4 januari 2013. 
  4. ↑ 1 2 3 4 SAT@home-lösningar hittades (länk ej tillgänglig) . Datum för åtkomst: 26 december 2012. Arkiverad från originalet 21 december 2012. 
  5. ↑ Brown et al. Slutförande av spektrumet av ortogonala diagonala latinska kvadrater. Föreläsningsanteckningar i ren och tillämpad matematik. 1992 vol. 139. S. 43–49.

Länkar