« zurück

SATRIX - Algorithmen für Boolesche Erfüllbarkeit

Die Bedeutung integrierter Schaltkreise ist auf Grund ihrer großen Verbreitung enorm. Integrierte Schaltkreise werden beispielsweise in Küchengeräten, Waschmaschinen, Telefonen aber auch medizinischen Geräten oder Kraftfahrzeugen eingesetzt. Bei den beiden letztgenannten Beispielen handelt es sich um sicherheitskritische Anwendungen. Aus diesem Grund muss die Korrektheit solcher Systeme garantiert werden. Um eine hohe Qualität des entworfenen Systems sicherzustellen, werden Verfahren zur Verifikation und zum Testen eingesetzt. Während bei der Verifikation die Überprüfung der funktionalen Korrektheit bereits im Entwurfsprozess stattfindet, dienen Testverfahren zur Überprüfung des gefertigten Systems. In den vergangenen Jahren wurden große Fortschritte in den genannten Gebieten durch den Einsatz formaler Methoden erreicht. Grundlage formaler Methoden sind effiziente Algorithmen und Datenstrukturen. Besondere Bedeutung haben hierbei Algorithmen zur Lösung des Erfüllbarkeitsproblems (SAT-Problem) gewonnen, da diese die Handhabung großer Schaltungen ermöglichen und inzwischen auch kommerziell mit großem Erfolg eingesetzt werden. Allerdings wächst die Größe der Schaltungen und Systeme rasant, was eine ständige Effizienzsteigerung dieser Algorithmen erfordert. Vor diesem Hintergrund startete das zweijährige studentische Projekt SATRIX im Jahr 2004 an der Universität Bremen. Ziel des Projektes war es, den gesamten Ablauf von der Modellierung einer Fragestellung als SAT-Problem bis hin zur effizienten Lösung einer gegebenen Instanz zu betrachten. Insbesondere sollten dabei Fragestellungen aus dem Schaltkreisentwurf untersucht werden. Die Resultate des Projektes sind im vorliegenden Buch zusammengefasst.