Maßgeschneiderte Autos aus der Massenproduktion

Nicht jeder Autokäufer kann sich eine Einzelanfertigung leisten. Aber auch ein erschwinglicher Neuwagen sollte individuellen Wünschen entsprechen – maßgeschneidert in der Massenproduktion. Die Informatiker Dr. Carsten Sinz und Prof. Wolfgang Küchlin haben auf dem Gebiet der Aussagenlogik und des automatischen Beweisens Programme entwickelt, die den Autobauern helfen, Wunschautos auf ihre Realisierbarkeit zu prüfen und die Bauteile „just-in-time“ bereit zu halten.

Tübinger Informatiker machen Bereich des automatischen Beweisens für Hersteller nutzbar

Wer in Deutschland einen Neuwagen kaufen will, erwartet eine möglichst große Auswahl an Lack- und Sitzfarben, eine flexible Gestaltung vielleicht mit Klimaanlage, Standheizung oder Schiebedach – kurz: ein individuelles Fahrzeug. Teuer wie eine Einzelanfertigung darf es aber auch nicht sein. Maßgeschneidert in der Massenfertigung heißt das Schlagwort. Doch ein solches Angebot stellt die Automobilhersteller vor Probleme. Das beginnt schon bei der Auftragsannahme: Die Zahl der möglichen Kombinationen von Farben, Ausstattungen und Extras erreicht schnell astronomische Ausmaße, und in der Praxis ist nicht jedes Autobauteil mit jedem anderen frei kombinierbar. Mancher Wunsch erfordert etwa einen stärkeren Motor, andere Ausstattungen sind nicht in allen Ländern notwendig wie etwa ein Katalysator. Nun muss vor der Produktion zunächst geklärt werden, ob der Wunschkatalog des Kunden überhaupt umsetzbar ist und welche Bauteile für diesen speziellen Wagen gebraucht werden. Um solche Anfragen schnell und korrekt beantworten zu können, haben Prof. Wolfgang Küchlin und Dr. Carsten Sinz vom Wilhelm-Schickard-Institut für Informatik der Universität Tübingen in Zusammenarbeit mit der Industrie die Anwendungsmöglichkeiten des symbolischen Rechnens und automatischen Beweisens für ein Baubarkeits-Informationssystem erforscht.

„Im Durchschnitt wird eine individuelle Fertigung in der Automassenproduktion erst nach circa 35.000 Autos in der gleichen Kombination und Ausstattung wiederholt“, sagt Wolfgang Küchlin. Bei Schwerlasttransportern werde jedes Fahrzeug im Schnitt sogar nur anderthalbmal gebaut. Doch wie kann das symbolische Rechnen dabei helfen, die großen Datenmengen bei der Maßanfertigung in der Massenproduktion zu bewältigen? Da muss Wolfgang Küchlin dann doch ein wenig ausholen: „In unserem Arbeitsgebiet rechnen wir mit Symbolen statt mit konkreten Zahlen. Ein Teilbereich ist das automatische Beweisen. Es geht um einen Zweig der mathematischen Logik, der Aussagenlogik, die auch als so genannte Boolesche Algebra bekannt ist. Man kann mathematische Sätze automatisch mit Hilfe der Rechenleistung von Computern beweisen“, sagt er. Man könne in der Logik Aussagen so formulieren und in den Computer eingeben, dass dieser errechnen kann, ob die Aussage wahr oder falsch ist. Gibt zum Beispiel ein Kaufinteressent für seinen Pkw in den Wunschkatalog unter anderem Klimaanlage und Doppelscheinwerfer ein, so lässt sich dies mathematisch in eine Regel fassen, die von einem Rechenprogramm im Computer auf „wahr“ beziehungsweise „machbar“ oder „falsch“ beziehungsweise „nicht möglich“ getestet werden kann. „Nun lassen sich manche Wünsche aus technischen Gründen nicht kombinieren, weil sie etwa räumlich nicht alle unterzubringen sind. Andere Dinge sind aus rechtlichen Gründen zu berücksichtigen“, erklärt der Wissenschaftler. Schließlich gebe es noch Kombinationen im Wunschkatalog, die die Marketingabteilung des Herstellers nicht zulassen möchte, zum Beispiel Sitzfarben, die sich mit der Karosseriefarbe beißen.

Solche Kombinationen und Einschränkungen werden in der Aussagenlogik durch umfangreiche Regelsysteme formuliert. Das sieht dann zum Beispiel so aus: B(S175)= M1/M3/M5/M6 – das heißt: Die Bestelloption wird in einem Code niedergelegt, hier die Nummer S175. Die Baubarkeitsregel dafür besagt, dass Motor 1, 3, 5 oder 6 eingebaut werden muss. „Nicht immer reichen so einfache Verknüpfungen aus. Die Regeln können sich über viele Zeilen hinziehen“, sagt Küchlin. Dabei muss unter Umständen mit 600 Optionen für das Auto, 350 Ländercodes und etwa 3300 Regeln herumjongliert werden. „Die erste Frage lautet immer: Lässt sich das gewünschte Auto bauen?“. Wegen der Größe und Anzahl der Regeln schließt sich aber sofort die weitere Frage an: „Ist das Regelsystem selbst korrekt oder enthält es in sich Widersprüche?“. Auch hier kommt das automatische Beweisen zu Hilfe. Ein korrektes Regelsystem muss gewisse Kriterien erfüllen, die sich wiederum als mathematische Aussagen formulieren und automatisch beweisen – oder widerlegen – lassen. Rein theoretisch könne man in der Aussagenlogik für jede Aussage beweisen, ob sie wahr oder falsch ist. Doch wenn die Aussagen lang und verwickelt sind, könne es in der Praxis wegen begrenzter Rechnerkapazitäten zu Problemen kommen.

„Die Grundzüge des automatischen Beweisens sind bereits Anfang der 1960er-Jahre gelegt worden. Damals war das aber ein rein theoretisches Arbeitsgebiet“, erzählt Küchlin. Erst in den 1990er-Jahren hätten dann Wissenschaftler ein Arsenal an Methoden entwickelt, mit dem das automatische Beweisen praktisch anwendbar wurde. „Der Anstoß zu diesen Fortschritten kam aus der Chip-Produktion. Die Industrie ist höchst interessiert daran, dass die mikroelektronischen Schaltungen, die in Boolescher Algebra beschrieben werden, logisch korrekt gebaut sind“, sagt Küchlin. Ein Prozessorenhersteller habe vor einigen Jahren wegen eines Fehlers in der Logik der Schaltungen Chips zurücknehmen und neu produzieren müssen, die Kosten erreichten 400 Millionen Dollar. Um Fehlern und unnötigen Kosten vorzubeugen, wurde in der Chip-Produktion ein zusätzliches Prüfverfahren auf der Basis des automatischen Beweisens etabliert.

Dr. Carsten Sinz hat die Erkenntnisse aus den Hardware-Testverfahren genutzt, um die Anwendungen für die Automobilindustrie zu entwickeln. Dafür hat er im Dezember 2004 den Förderpreis für den wissenschaftlichen Nachwuchs des Verbands der Metall- und Elektroindustrie Baden-Württemberg an der Uni Tübingen erhalten. Jetzt arbeiten die Tübinger Forscher in Projekten mit einem Auto- und einem Medizintechnikhersteller zusammen. Die Prüfprogramme sind prinzipiell auch für andere Bereiche oder Produkte wie zum Beispiel Schweißgeräte nutzbar. „Auch die werden heute in Modulen hergestellt, sodass der Kunde zum Beispiel auswählen kann, welche Materialien mit dem Gerät hauptsächlich geschweißt werden sollen“, erklärt Küchlin. Doch mit der Feststellung, ob ein Auto oder ein Gerät sich in der Praxis bauen lässt, sind die Methoden des automatischen Beweisens noch nicht ausgereizt. Denn nun muss der Hersteller wissen: Sind alle Bauteile für das gewünschte Auto vorhanden und rechtzeitig lieferbar? „Dafür müssen die Regeln mit Stücklisten verknüpft werden. Und das sind für einen Pkw schätzungsweise 35.000 Positionen“, sagt Küchlin. Andersherum kann mit den Programmen der Informatiker auch die Frage beantwortet werden: Sind in der langen Liste Bauteile, die etwa wegen der Änderung von Modellen nicht mehr gebraucht werden? „Das müssen die Hersteller aus Kostengründen ständig überprüfen.“

Das automatische Beweisen geht in diesen Bereichen über das akademische Interesse hinaus, erklärt der Informatiker: „Wenn die Regeln für die Baubarkeit eines Autos falsch formuliert sind, kann es passieren, dass ein Auftrag zurückgewiesen wird, obwohl man das Auto hätte bauen können. Das ist ein wirtschaftlicher Schaden für das Unternehmen.“ Der kann auch entstehen, wenn ein Auftrag auf der Grundlage falscher Regeln angenommen wird und dann doch nicht realisierbar ist: „Dann ist der Kunde verärgert.“ „Geschäftskritisch“ ist auch die Verwaltung der Stücklisten für die Produktion. „Bei der heutigen Lieferung ’just-in-time’ werden bei den Herstellern nur noch minimale Lager angelegt. Wird also auch nur ein winziges Teil nicht pünktlich angeliefert, bleibt das Fließband in der Produktion stehen“, schildert Küchlin die Probleme. Er meint aber, dass die Fertigung und damit die Arbeitsplätze nur durch die Individualisierung der Produkte in Deutschland gehalten werden können. „Wenn eine Firma tausend genau gleiche Stücke – Autos, Schweißgeräte oder andere Maschinen – herstellen will, ist die Produktion in China viel billiger, damit kann man hier zu Lande nicht konkurrieren.“ (7780 Zeichen)

Nähere Informationen:

Prof. Dr. Wolfgang Küchlin
Wilhelm-Schickard-Institut für Informatik
Sand 14
72076 Tübingen
Tel. 0 70 71/2 97 04 70; Sekretariat Tel. 0 70 71/2 97 04 71
Fax 0 70 71/29 50 61
E-Mail kuechlin@informatik.uni-tuebingen.de