Only available in German
Informatiker auf der Suche nach Erfüllung
Unter Mitarbeit der AG „Rechnerarchitektur“ der Universität Bremen ist das erste umfassende Handbuch zum Thema Boolesche Erfüllbarkeit erschienen
Logistische Prozesse optimal gestalten, Schaltkreise als korrekt Nachweisen oder komplexe Sachverhalte übersichtlich graphisch darstellen. Mit Problemen dieser Art haben es Informatiker in ihrer täglichen Arbeit zu tun. So unterschiedlich diese Aufgaben klingen, haben sie doch eines gemeinsam: Wenn es gelingen würde, eines dieser Probleme zu lösen, so könnte man daraus auch unmittelbar Lösungen für die anderen Probleme ableiten. Wie schwer das ist, zeigt ein Aufruf aus den USA, bei dem vom Clay Mathematics Institute (CMI) of Cambridge, Massachusetts, eine Million Dollar geboten werden, wenn jemand für nur eines dieser Probleme eine Lösung finden würde.
Inzwischen wurde für über tausend Probleme nachgewiesen, dass sie – in diesem Sinne – gleich schwierig sind. Das Problem, für das erstmals diese Eigenschaft gezeigt werden konnte, ist die Boolesche Erfüllbarkeit. Der Nachweis dafür liegt bereits über 25 Jahre zurück. Aufgrund der großen theoretischen und praktischen Bedeutung des Problems ist jetzt erstmals ein umfassendes Handbuch in dem internationalen Fachverlag IOS Press erschienen. An dem englischsprachigen Nachschlagewerk mit dem Titel „Handbook of Satisfiability“ haben zahlreiche Wissenschaftler mitgearbeitet – ein Autor ist der Informatiker der Universität Bremen, Prof. Dr. Rolf Drechsler, mit seiner Arbeitsgruppe „Rechnerarchitektur“.
Das Handbuch umfasst knapp tausend Seiten und beschreibt sowohl theortische als auch praktische Aspekte des Problems. Insbesondere werden erstmals auch die jüngsten Ergebnisse aufgegriffen, die es erlauben, große Probleminstanzen schnell zu lösen. Professor Drechsler hat darin einen Beitrag zum praktischen Einsatz von Boolescher Erfüllbarkeit zum Testen von Schaltkreisen und Systemen geschrieben. Die von seiner Arbeitsgruppe „Rechnerarchitektur“ erarbeiteten Resultate entstanden im Rahmen eines vom Bundesministerium für Bildung und Forschung (BMBF) geförderten Projektes in Kooperation mit der Hamburger Firma NXP Semiconductors und wurden darüber hinaus von der Deutschen Forschungsgemeinschaft (DFG) unterstützt.
