Neuigkeit aus der Forschungsgruppe Wissensverarbeitung vom 9. Oktober 2015

Mitarbeiter der Wissensverarbeitung entwickeln Weltspitze-Werkzeuge für Generische Problemlöser

Im Zeitalter der Automatisierung müssen immer komplexerer Systeme in immer kürzerer Zeit viel mehr Aufgaben lösen. Die Forschung beschäftigt sich daher seit einiger Zeit mit der Entwicklung möglichst effizienter Verfahren (sogenannter SAT-Solver), um die Zuverlässigkeit und Korrektheit von Programmen und Geräten zu garantieren. SAT Solver helfen beispielsweise beim Überprüfen eines Computersystems auf Fehler, beim Erstellen eines guten Fahrplans, den Betriebsablauf in einer Fabrik zu optimieren, Programmfehler in Software oder fehlerhafte Zustände in Schaltkreisentwürfen zu finden. Dazu überprüfen sie riesige Systembeschreibungen und bestimmen die Voraussetzungen, unter denen das jeweilige System fehlerfrei arbeitet oder zeigen einen konkreten Fehler auf.

An der Fakultät Informatik der TU Dresden entwickelt Norbert Manthey an der Professur für Wissensverarbeitung seit fünf Jahren den SAT Solver „Riss“ und gemeinsam mit Studenten darauf aufbauende Werkzeuge. Diese Forschung wird inzwischen durch ein DFG Projekt gefördert. In den diesjährigen internationalen SAT-Wettbewerben für Hardware Model Checking, der MaxSAT Evaluation sowie der SAT Race hat die Gruppe gezeigt, dass die entwickelten Werkzeuge in allen drei Bereichen an der Weltspitze agieren. Norbert Manthey freut sich über den Erfolg: "Es macht uns stolz, dass wir in immer mehr Bereichen weltweit wettbewerbsfähig werden und an die Vorjahreserfolg anknüpfen können.“ Die Ziele der drei Wettbewerbe decken wesentliche Anwendungsgebiete der SAT-Solver ab: Die Hardware Model Checking Competition vergleicht, wie gut Systemprüfer, sogenannte Modelchecker, beweisen können, ob ein Schaltkreis einen fehlerhaften Zustand erreichen kann oder nicht. Ein besonderes Augenmerk liegt auf nicht komplett beweisbare Schaltkreise - hier versucht man zu zeigen, dass der fehlerhafte Zustand möglichst lange nicht auftritt. In dieser Kategorie hat das von Manthey entwickelte Werkzeug „ShiftBMC“ den ersten Platz belegen können, welcher mit einem 500 USD Preisgeld der Firma Oski Technology dotiert wurde. In der SAT Race werden Lösungen für industrielle kombinatorische Probleme gesucht und entsprechende Werkzeuge miteinander verglichen. Besonders bedeutsam ist hier das Anpassen an die wechselnden Problemkombinationen, da die Zahl der Anwendungsgebiete, von Jahr zu Jahr steigt. Der SAT Solver „Riss“ konnte hier einen dritten Platz belegen. In der MaxSAT Evaluierung werden optimale Lösungen von diskrete Optimierungsprobleme gesucht. Dabei gibt es zwei unterschiedliche Kategorien: das Beweisen einer optimalen Lösung mit relativ viel Zeit oder das Auffinden einer möglichst guten Lösung innerhalb von zehn Minuten. Für Optimierungsaufgaben aus der Industrie konnte das Werkzeug „Optiriss“ in der zweiten Kategorie erste zweite und dritte Plätze belegen, je nach Beschaffenheit der Optimierungsaufgaben.

Ein Grund für das gute Abschneiden der Systeme ist unter anderem auch der dieses Jahr eingeweihte Hochleistungsrechner der TU Dresden, durch den Auswertungszeiten wesentlich verkürzt werden.