SAT@home

Aus BC-Wiki
Wechseln zu: Navigation, Suche
Sat-logo.png

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.

Erde.png SAT@home
Beginn 2011
Ende
Status beta
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
Info.png Anwendungen
Win.png Win ParallelAndDistributedSATsolver 3.20
PD-SAT for cryptology 2.05
Linux2.png Linux ParallelAndDistributedSATsolver 3.20
PD-SAT for cryptology 2.05
Macos.gif Mac
Amd64.jpg 64bit ParallelAndDistributedSATsolver 3.20 [win/linux]
PD-SAT for cryptology 2.05 [win/linux]
Ps3.png PS3
Ati.jpg ATI
Cuda.jpg CUDA
Intel.jpg Intel
Android.png Android No.gif
Raspberri Pi.png RPi No.gif
Nci.jpg NCI No.gif
Specs.png Systemspezifikationen
VRAM SP No.gif DP No.gif
RAM 4,8MB
Laufzeit 2,5h
HDD 0,7MB
Traffic dl/ul kb / kb
Deadline 3 Tage
Checkpoints Yes.gif