SAT@home

Aus Rechenkraft
Wechseln zu: Navigation, Suche
Logo

Das Projekt zielt darauf ab, verschiedene kombinatorische Probleme zu lösen. Es gibt viele praktisch wichtige Probleme, für die es keine wirksame (Polynom) Algorithmen gibt. Die meisten dieser Probleme sind NP-schwer. Das bedeutet, dass das Problem unter (wenn auch unbewiesenen) Annahmen nicht in polynomialer Zeit gelöst werden kann.

Allerdings ergeben sich viele ihrer besonderen Fällen in der Praxis:

  • Verschiedene diskrete Optimierungsprobleme (z.B. Planung der Produktion) und
  • Probleme der Verifikation von diskreten Bauelementen (die sich z.B. bei der Gestaltung von Schaltungen und der Verifizierung der Korrektheit von Programmen ergeben).

Daher ist es sehr wichtig, Methoden zu ihrer Lösung zu besitzen, die keine polynomiale Komplexität haben, sich aber in der Praxis bewährt haben. Solche Methoden können zahlreichen Sonderfälle der NP-schweren Probleme mit großen Dimensionen bewältigen. Einer der in der Basis einfachsten und damit effizienteste bzgl. der Software Implementierung ist der SAT-Ansatz. Dieser Ansatz, der auf Reduzierbarkeit des ursprünglichen Problems zu einem SAT-Problem basiert, ist das Erfüllbarkeitsproblem der Aussagenlogik. SAT-Probleme haben eine sehr natürliche Form der Parallelität, die den Einsatz einer verteilten Computing-Umgebungen (einschließlich Grid) ermöglicht. Das Reduzieren auf ein SAT-Problem kann sehr effizient sein (in der Tat ergibt sich das aus dem berühmten Satz von Cook und Levin).

Die Kryptoanalyse bietet eine sehr attraktive Klasse von Problemen, bei dem der SAT-Ansatz verwendet werden kann. Es sei darauf hingewiesen, dass das Projekt keine Probleme löst um private Daten zu entschlüsseln. Alle Tests, die generiert werden, sind zufällig generiert. Das Projekt möchte die Stabilität moderner Verschlüsselungssysteme studieren. Das stärkste praktische Ergebnis ist die erfolgreiche logische Kryptoanalyse (d.h. in Form eines SAT-Problems) des Keystream Generators, der in in der bekannten A5/1 Verschlüsselung benutzt wird. Dieses Ergebnis wurde im Jahr 2009 mit dem Einsatz von BNB-Grid ermittelt (Artikel in der Zeitschrift für ISA RAS, Artikel auf arXiv.org, Artikel in Lecture Notes in Computer Science). In den Jahren 2010-2011 gab es Untersuchungen (z.B. CCC 2009 ), in denen echte Kryptoanalyse von A5/1 durchgeführt wurde, aber mit unterschiedlichen Methoden. Es wurde eine fortgeschrittene Technik der Rainbow-Tables verwendet. Aber auch die beste Rainbow-Tables decken nicht 100% des Suchraums ab. Daher wird in nahen Zukunft das Projekt SAT@home versuchen das Problem der Suche nach der Initialisierung von A5/1 Sequenzen zu lösen, die nicht von den bekanntesten Rainbow-Tables abgedeckt werden.

Weiterhin soll SAT@home genutzt werden um weitere kryptographische Funktionen zu studieren und einige "extrem schwere" Probleme der diskreten Optimierung, insbesondere die Quadratic Assignment Problem (QAP), und einige Probleme der Bioinformatik (Analyse diskreter Modelle von Gen-Netzwerken) zu lösen.

Das Projekt wird vom

durchgeführt.


Inhalt

Projektübersicht

InfoIcon.png SAT@home
Name SAT@home
Kategorie Kryptographie
Ziel Lösung verschiedener kombinatorischer Probleme
Kommerziell   nein
Homepage sat.isa.ru/pdsat
 
Russia01.gif     Dieses Projekt wird in Russland durchgeführt.

Projektstatus

InfoIcon.png Projektstatus
Status   aktiv
Beginn 29 September 2011
Ende noch aktiv

Projektlinks

Statistiken

Wo Übersicht Top Teams Top User
Projekt Home Page Top Teams Top User
BOINCstats.com Übersicht Top Teams Top User
stats.free-dc.org Übersicht Top Teams Top User

Clientprogramm

Betriebssysteme

Icon windows 16.png    Windows Checkbox 1.gif   
Icon windows 16.png    Windows 64bit Checkbox 1.gif   
Icon linux 16.png    Linux Checkbox 1.gif   
Icon linux 16.png    Linux 64bit Checkbox 1.gif   
Icon dos 16.png    DOS Checkbox 0.gif   
Icon macos 16.png    MacOS X Checkbox 0.gif   
Icon freebsd 16.png    BSD Checkbox 0.gif   
Icon solaris 16.png    Solaris Checkbox 0.gif   
Icon java 16.png    Java (betriebssystemunabhängig)  Checkbox 0.gif   

Client-Eigenschaften

Funktioniert auch über Proxy Checkbox 1.gif
Normal ausführbares Programm Checkbox 0.gif
Als Bildschirmschoner benutzbar Checkbox 0.gif
Kommandozeilenversion verfügbar Checkbox 1.gif
Personal Proxy für Work units erhältlich   Checkbox 0.gif
Work units auch per Mail austauschbar Checkbox 0.gif
Quellcode verfügbar Checkbox 0.gif
Auch offline nutzbar Checkbox 0.gif
Checkpoints Checkbox 0.gif

Veröffentlichte Versionen

Die jeweils aktuellen Versionen können hier eingesehen werden.

Installation

SAT@home benutzt die BOINC-Infrastruktur. Die Anmeldung, Installation und Konfiguration sind auf der allgemeinen BOINC-Seite beschrieben.

Screenshots

Meldungen

RSS RSS-Feed

Der RSS-Feed konnte nicht von http://boinc.isa.ru/dcsdg/rss_main.php|title=none|max=10 geladen werden: Fehler beim Abruf der URL: Connection timed out after 5001 milliseconds


Eigene Werkzeuge