Symbolische KI für die Produktkonfiguration in der Automobilindustrie

Die Automobilindustrie bietet ihre Fahrzeuge in einer praktisch endlosen Vielzahl von Varianten an. Diese entstehen durch Kombinationen von Ausstattungsoptionen, die sich von Kunden zu einem individuellen Produkt konfigurieren, d. h. zusammenstellen lassen. Die Kombinationsmöglichkeiten unterliegen dabei einer Vielzahl von Konfigurationsregeln, die typischerweise in einer Spielart von Aussagenlogik notiert sind. Hierbei repräsentieren die Symbole die Ausstattungsoptionen, und die Formeln definieren die Möglichkeiten zu ihrer Zusammenstellung in einem Fahrzeug. Insgesamt erhält man eine symbolische Beschreibung des Fahrzeugangebots, die sog. Modellbeschreibung. Aber auch die Auswahl der Teile, aus denen jedes Fahrzeug letztendlich aufgebaut wird, ist durch Formeln der Aussagenlogik beschrieben. Fehler in den Formeln können teure Konsequenzen in der Produktion nach sich ziehen. Aufgrund der astronomischen Varianz ist es praktisch unmöglich, solche Fehler durch erschöpfendes Testen zu finden. Jedoch ermöglichen automatische Beweisverfahren der Symbolischen KI, sog. Erfüllbarkeitsprüfer (SAT-Solver), die effiziente formal-logische Analyse auch sehr großer Regelmengen. Nicht nur die Anwesenheit von Fehlern, sondern auch deren Abwesenheit kann automatisch bewiesen werden, und alle Resultate können nachvollziehbar erklärt werden. Diese Methoden sind mittlerweile im breiten industriellen Einsatz.