SAT@home

Aus BC-Wiki
Zur Navigation springen Zur Suche springen
Die druckbare Version wird nicht mehr unterstützt und kann Darstellungsfehler aufweisen. Bitte aktualisiere deine Browser-Lesezeichen und verwende stattdessen die Standard-Druckfunktion des Browsers.

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.

SAT@home
Beginn 2011
Ende Ende 2017
Status beendet
Admin Oleg Zaikin
Institut Institute for Systems Analysis of RAS and Institute for System Dynamics and Control Theory of SB RAS
Land Russland
Bereich Grid/Informatik
Anwendungen
Win ParallelAndDistributedSATsolver 3.20
PD-SAT for cryptology 2.05
Linux ParallelAndDistributedSATsolver 3.20
PD-SAT for cryptology 2.05
Mac
64bit ParallelAndDistributedSATsolver 3.20 [win/linux]
PD-SAT for cryptology 2.05 [win/linux]
PS3
ATI
CUDA
Intel
Android
RPi
NCI
Systemspezifikationen
VRAM SP DP
RAM 4,8MB
Laufzeit 2,5h
HDD 0,7MB
Traffic dl/ul kb / kb
Deadline 3 Tage
Checkpoints