Warum der Handlungsreisende nicht die beste Route findet

Kennen Sie das Problem des Handlungsreisenden? Der Handlungsreisende soll die kürzeste Route finden, mit der er alle größten 15 deutschen Städte besuchen kann. Das Problem dabei: durch die 15 Städte gibt es 43.589.145.600 mögliche Routen. Und in der Informatik wurde momentan noch kein allgemeiner Lösungsweg gefunden, keine 43.589.145.600 Möglichkeiten durchzuprobieren.

Es gibt dutzende solcher schweren Probleme in der Informatik

Die Handlungsreisenden sind nicht allen. Derart hohen Rechenaufwand zur Problemlösung müssen auch für andere Probleme aufgewandt werden:

• Das Rucksackproblem: Ein Rucksack mit definiertem Volumen soll mit Gegenständen von gewissem Wert und Volumen gefüllt werden, sodass man den maximalen Wert erreicht.
• Cliquenproblem: Finde die größte Clique, bei der jeder mit jedem vernetzt ist (z.B. auf Facebook Personen, die alle paarweise miteinander vernetzt sind)
• Job-Sequencing-Problem: Finde die optimale Auswahl und zeitliche Eintaktung von möglichen Aufträgen für eine Maschine, von denen die Abarbeitungs-Zeit, Deadline und der Profit bekannt sind.
• Terminkalender: Finden Sie für eine Woche mit 20 Terminen, die jeweils 2-4 Terminvorschläge haben eine Wochenbelegung.
• Verschlüsselung knacken: Die NSA beißt sich die Zähne daran aus, Verbindungen zu simplen Online-Shops zu belauschen, da diese verschlüsselt sind.

Alle diese Probleme stellen dasselbe Problem dar

All diesen harten Probleme haben eins gemeinsam: Sie stellen ein- und dasselbe Problem dar und lassen sich ineinander umwandeln. So lässt sich beispielsweise das Problem des Handlungsreisenden auch als Rucksackproblem darstellen, indem das Gewicht der Stücke für den Rucksack die 15 zu erreichenden Städte darstellt und der Wert der Stücke die negierte Entfernung der Städte zueinander.

Symbolisches Rechnen

Eines dieser harten Probleme (auch NP-Hart genannt) ist das sogenannte SAT-Problem: Gegeben eine logische Formel ist zu prüfen, ob diese lösbar ist.

Genialerweise lässt sich jedes dieser Optimierungs- und Suchprobleme als eine logische Formel darstellen, die als SAT-Problem gelöst werden kann. Zudem ist SAT durch die einfache 3-SAT-Schreibweise sehr handlich. Ein Programm, das SAT-Probleme lösen kann, nennt man SAT-Solver.

Das Grundprinzip eines SAT-Solvers ist einfach: Die gegebene logische Formel wird so lange umgestellt, bis die Lösung aus der Formel ablesbar ist. Jedoch muss ein SAT-Solver bei unbekannten Werten (entweder 1 oder 0) beide Varianten durchprobieren, um die Lösung zu finden. Das sind bei zwei unbekannten Werten schon 4 Varianten, bei 10 Unbekannten 1024 Möglichkeiten und bei 20 Unbekannten schon eine Million.

Anbindung an eine Datenbasis

Die Kunst, SAT praktisch anzuwenden liegt darin, Probleme als SAT-Probleme zu definieren. So können beispielsweise Fakten aus einer Datenbank als Formeln kodiert werden, um später Schlussfolgerungen aus den Daten zu ziehen.

Wir bei Launix können Ihnen helfen, Daten digital zu verwalten, sowie für SAT-Solver aufzubereiten. Mit unseren Datenbanken eröffnen sich neue Wege fürs Planen und Optimieren.