SAT@home

Az oldal jelenlegi verzióját még nem ellenőrizték tapasztalt közreműködők, és jelentősen eltérhet a 2018. május 16-án áttekintett verziótól ; az ellenőrzések 5 szerkesztést igényelnek .
SAT@Home
Felület BOINC
Szoftverletöltés mérete 10 MB
Munkaadatok betöltött mérete 2 KB
Az elküldött munkaadatok mennyisége 20 KB
Lemezterület _ 10 MB
Felhasznált memória mennyisége 80 MB
GUI Nem
Átlagos feladat számítási idő legfeljebb 5 óra
határidő 10 nap
GPU használatának képessége Nem

A SAT@home egy orosz önkéntes számítástechnikai projekt a BOINC platformon , 2011 szeptemberében indult [1] . A projekt tudományos célja diszkrét problémák megoldása a logikai formulák (SAT, angol nyelvből  Satisfiability - feasibility) konjunktív normál formában (CNF) kielégíthetőségének problémájára redukálva. A kiválasztott probléma megoldásának megtalálása az egyik jól ismert SAT-megoldó segítségével történik, amely megvalósítja a DPLL algoritmust . A projektet az Orosz Tudományos Akadémia Szibériai Kirendeltsége Rendszerdinamikai és Vezérléselméleti Intézetének Diszkrét Analízis és Alkalmazott Logikai Laboratóriuma és az Információátviteli Problémák Intézetének Elosztott Számítástechnikai Központja támogatja . 2014. szeptember 19-én 124 ország 7239 felhasználójának 18394 számítógépe vett részt a projektben, mintegy 3,1 teraflop teljesítményt biztosítva [ 2] . A BOINC program telepítésével bárki részt vehet a projektben, aki rendelkezik Internet hozzáféréssel rendelkező számítógéppel .

Projekttörténet

A projekt keretén belüli számítások [3] 2011 szeptemberében kezdődtek a GSM kommunikációban használt A5/1 generátor kriptoanalízise problémájának megoldásával. A kulcsfolyam ismert töredéke szerint meg kellett határozni az inicializálási sorrendet, vagyis a generátorregiszterek kezdeti kitöltését . A számítások célja az volt, hogy bebizonyítsák a SAT megközelítés alkalmazhatóságát a probléma megoldására olyan esetekben, amikor más módszerekkel (például szivárványtáblázatok segítségével) nem lehet megoldást találni . A számítások eredményeként 2012 májusáig az A5/1 [4] kriptoanalízis 10 tesztproblémája megoldódott .

2012 júniusában új kísérlet indult, melynek célja 9-es rendű átlós latin négyzetek merőleges párjainak felkutatása volt . 2012 augusztusáig 134 pár került elő, ami igazolta ennek a megközelítésnek a probléma megoldására való alkalmazhatóságát. Ezt követően kísérletet indítottak 10-es rendű átlós latin négyzetek merőleges párjainak keresésére. A számítások eredményeként eddig 13 latin négyzetpárt [4] találtak , amelyek nem esnek egybe a megadott ismert párokkal. cikkben [5] .

Tudományos eredmények

2012-es év 2013-as év

Úgy tűnik, a projekt 2016-ban megszűnt.

Jegyzetek

  1. ↑ SAT@Home . Hozzáférés dátuma: 2012. december 26. Az eredetiből archiválva : 2012. december 21.
  2. ↑ SAT@home részletes statisztika . Letöltve: 2013. szeptember 5. Az eredetiből archiválva : 2013. augusztus 11..
  3. ↑ SAT@home hírarchívum (downlink) . Hozzáférés dátuma: 2012. december 26. Az eredetiből archiválva : 2013. január 4.. 
  4. ↑ 1 2 3 4 SAT@home megoldások találhatók (hivatkozás nem érhető el) . Hozzáférés dátuma: 2012. december 26. Az eredetiből archiválva : 2012. december 21. 
  5. ↑ Brown et al. Az ortogonális átlós latin négyzetek spektrumának befejezése. Jegyzetek a tiszta és alkalmazott matematikából. 1992. évf. 139. Pp 43–49.

Linkek