1 Einleitung
Symbolische Logik spielt eine wichtige und zentrale Rolle in der Automobilindustrie. Allgemein gesprochen geht es sowohl um die Beschreibung aller Konfigurationsmöglichkeiten für die Fahrzeuge im Angebot eines Herstellers, als auch um die Beschreibung der Teile, die für den Bau einer beliebigen Fahrzeugkonfiguration benötigt werden. Da Formulierungen in natürlicher Sprache oder einfache Angebotstabellen mit der wachsenden Komplexität des Angebots nicht Schritt halten konnten, verwenden viele Hersteller bereits seit längerer Zeit maschinell auswertbare Formeln der Aussagenlogik (Schöning 1987), wenn auch in herstellerspezifischen Dialekten und Schreibweisen. Allerdings ergeben sich dadurch auch sehr große und komplexe Formelwerke und somit neue Fehlerquellen. Diese lassen sich mit modernen Algorithmen des Automatischen Beweisens, einer Disziplin der Symbolischen KI bzw. des Symbolischen Rechnens, beherrschen.
Symbolische KI ist eine Teildisziplin der klassischen KI, bei der es um die Automatisierung logischer Schlussfolgerungen geht mit dem ursprünglichen Ziel, das allgemeine Problemlösen zu automatisieren (Nilsson 1971, 1980; Genesereth und Nilsson 1987). Der dominante Ansatz nutzt Prädikatenlogik als Modellierungssprache für Problemstellungen in Kombination mit der mechanischen Inferenzmethode der Resolution (Robinson 1965). Ein zeitlich früherer Ansatz bestand in einer Reduktion des prädikatenlogischen Problems auf Aussagenlogik in Kombination mit einer maschinellen Erfüllbarkeitsprüfung (Davis und Putnam 1960). In ihrer verbesserten Form (Davis et al. 1962) ist die Prüfung nach ihren Autoren als DPLL SAT-Solving bekannt geworden. Es wurde aber schnell offensichtlich (Davis et al. 1962), dass das Davis-Putnam Verfahren auf der Prädikatenlogik völlig ineffizient ist. In den 1990er-Jahren wuchsen schließlich in der Halbleiterindustrie immer größere rein aussagenlogische Problemstellungen heran, die zu einem erstarkten Interesse an SAT-Solving als Analyse- und Verifikationsmethode führten. Etwa seit dem Jahr 2000 steht eine aus DPLL weiterentwickelte, deutlich mächtigere Generation von „lernenden“ SAT-Solvern nach der CDCL Methode zur Verfügung (Marques-Silva und Sakallah 1999), mit der viele industrielle und wissenschaftliche Probleme effizient gelöst werden können (Biere et al. 2009; Schöning and Torán 2012; Knuth 2016).
In der zweiten Hälfte der 1990er-Jahre erforschte der Autor mit seinen Doktoranden, gefördert durch die damalige DaimlerChrysler AG, wie die immer größer werdenden Formelsysteme der Automobilkonfiguration unter Einsatz von SAT-Solving analysiert und besonders hinsichtlich häufiger Fehler untersucht werden können (Küchlin und Sinz 2000; Sinz et al. 2003). Inzwischen sind die in Tübingen entstandenen Methoden bei einer Anzahl von Automobilherstellern im täglichen industriellen Einsatz, nicht zuletzt mit Software, die unmittelbar am Tübinger Technologietransferzentrum aus dieser Forschung entstand.
2 Individualisierte Massenfertigung und Produktdokumentation
Automobile werden nach dem Prinzip der individualisierten Massenfertigung (mass customization) produziert (Tiihonen und Felfernig 2017). Sie werden zwar in großen Massen am Fließband gefertigt, aber sie werden zuvor individuell konfiguriert, indem man aus einer großen Anzahl von Ausstattungsoptionen eine Auswahl trifft und diese zu einem persönlichen Fahrzeug kombiniert. Auf diese Weise können höchst individuelle Fahrzeuge angeboten werden, die sich trotzdem zu relativ günstigen Kosten produzieren lassen.
Produkte der individuellen Massenfertigung sind modularisiert, d. h. sie werden aus Modulen zusammengestellt, von denen jeder wieder in einer Anzahl von Varianten zur Verfügung steht. Als Beispiel eines Moduls denke man sich einen Fahrersitz mit Optionen für Farbe, Sitzbezug, Heizung, Belüftung, sowie für diverse mechanische oder elektrische Einstellungsmöglichkeiten. Jedes Fahrzeug wird dann als individuelle Konfiguration von Ausstattungsoptionen bestellt und als Zusammenbau der entsprechenden Modulvarianten gefertigt. Gemäß den Gesetzen der Kombinatorik liegt die Anzahl der einzelnen Fahrzeuge eines Modells (die Varianz) je nach Zählweise typischerweise in einer Größenordnung von 1020 bis 1030 und darüber hinaus (Astesana et al. 2010b; Kübler et al. 2010; Zengler und Küchlin 2013). In anderen Worten: Man kann für jeden Bewohner der Erde weit über eine Milliarde (109) verschiedene Fahrzeuge konfigurieren, ohne dabei eine einzige Konfiguration zu wiederholen.
Die Produktdokumentation hat zwei Kernaufgaben: Einerseits beschreibt sie die Produktvielfalt, die verkauft werden kann, und andererseits dokumentiert sie für jedes individuell konfigurierte Produkt, aus welchen Bestandteilen es gefertigt wird (Haag 1998). Einfach gesagt stellt der erste Teil, die Produkt- oder Modellbeschreibung (MB, bzw. model description – MD), das Produktangebot dar, das im Verkaufsprospekt erscheint. Der zweite Teil, die Stückliste (Bill-of-Materials – BoM), enthält alle Bauteile, die für den Zusammenbau der Fahrzeuge zur Verfügung stehen, seien sie mechanisch, elektronisch, oder Softwarebausteine. Etwas genauer kennt die Automobilindustrie sowohl eine Produktdokumentation auf der Entwicklungsebene als auch eine auf der Verkaufsebene, um das, was man im Prinzip bauen kann, von dem zu unterscheiden, was man tatsächlich anbieten möchte. Das Produktdokumentations-Management (Product Documentation Management – PDM) bzw. das Produktlebenszyklus-Management (Product Lifecycle Management – PLM) verwaltet die Produktdokumentation über den gesamten Lebenszyklus des Produkts, von Entwicklung und Verkauf über die Produktion bis zur Ersatzteilversorgung. Da Teile und ihre Lieferanten stetig erneuert werden, besteht auch ständiger Änderungsbedarf im PDM. Eine allgemeine Einführung ins PDM aus der Sicht des Verkaufskonfigurators der Firma SAP findet sich bei Haag (1998).
3 Logik-Codierung der Modellbeschreibung
Mit einer Varianz, die in die Trilliarden geht, ist es nicht mehr möglich, das Produktangebot explizit als Liste aller möglichen Bestellungen (Orders) und der für den Zusammenbau nötigen Teile aufzuschreiben. Stattdessen wird in der Automobilindustrie allgemein ein PDM Ansatz benutzt, der auf Symbolischer Logik beruht (Kaiser und Küchlin 2001b). Zwei häufig eingesetzte Formalismen sind das Modellieren des PDM als Menge Boolescher Randbedingungen (set-of-constraints), oder aber als etwas allgemeineres Bedingungserfüllungsproblem (Constraint Satisfaction Problem – CSP). Die Sicht eines CSP wird z. B. im SAP Konfigurator (Haag 1998) und im RENAULT Konfigurator und PDM System eingenommen (Astesana et al. 2010a, b). Der CSP Ansatz stammt aus der Forschung der Künstlichen Intelligenz (KI) und erlaubt allgemeinere als nur Boolesche Randbedingungen, wie etwa numerische Bedingungen, die im Beispiel von Haag bei der Konfiguration von Küchen als Längenmaße auftreten (Haag 1998). Komplexere Bedingungen ziehen jedoch den Preis komplexerer Lösungsalgorithmen und potenziell (sehr viel) längerer Laufzeiten nach sich.
Viele wichtige Probleme im automobilen PDM sind aber rein aussagenlogisch modellierbar, und viele sehr große Systeme Boolescher Formeln, die in speziellen Anwendungen auftreten, können von modernen CDCL SAT-Solvern sehr effizient gelöst werden. Eine ganze Reihe von Automobilherstellern, darunter DAIMLER, codieren ihre PDM Systeme direkt in Aussagenlogik, während z. B. RENAULT zunächst von einem CSP Modell mit Booleschen Bedingungen ausgeht. Die Grundideen des Booleschen Codierens sind, erstens, jede Ausstattungsoption durch einen Optionscode (eine Boolesche Variable) zu codieren, zweitens, die Modellbeschreibung als Menge Boolescher Konfigurationsbedingungen zu repräsentieren, und drittens, statt einer statischen Stückliste für jedes einzelne Fahrzeug zu einer einzigen dynamischen Varianten-Stückliste für eine ganze Fahrzeugklasse oder Baureihe überzugehen. Aus letzterer kann für jedes tatsächlich bestellte Fahrzeug die individuelle statische BoM durch aussagenlogische Evaluation berechnet werden.
Durch die Benutzung Boolescher Optionscodes ist jede beliebige Kombination von Ausstattungen nun über eine vollständige true/false Belegung der Codes gegeben, wobei true der Anwesenheit der Option und false ihrer Abwesenheit in einer klassischen Bestellung bzw. Konfiguration entspricht. Eine beliebige Kombination ist aber nur dann eine tatsächlich baubare oder valide Order, falls durch die Variablenbelegungen alle Konfigurationsbedingungen der Modellbeschreibung (im logischen Sinn) erfüllt werden. Aus der Sicht der Booleschen Algebra entspräche eine explizite Auflistung aller validen Orders einer Formel in Disjunktiver Normalform (DNF) bestehend aus Konjunktionsgliedern, die jeweils alle Ausstattungscodes positiv oder negativ enthalten (sog. Minterme). Bei 1020 Produkten bestünde die DNF also aus 1020 Mintermen und könnte in der Praxis nicht mehr dargestellt werden. Das logische Konzept einer solchen Produktübersichtsformel (Product Description Formula – PDF), deren Lösungen die validen Orders darstellen, erweist sich aber dennoch als extrem nützlich (Küchlin und Sinz 2000).
Abgesehen von Ausnahmen haben Formeln mit einer großen Anzahl von Lösungen (Modellen) üblicherweise eine wesentlich kompaktere Repräsentation in Form einer Menge von Bedingungen (set-of-constraints), d. h. als eine Menge von kleineren Booleschen Formeln, die von einem Modell alle gleichzeitig erfüllt sein müssen. Die Wahl einer solchen Form für eine Produktbeschreibung ist aber auch ganz natürlich. Bedingungen schränken die Art und Weise ein, in der Ausstattungsoptionen in einem Fahrzeug bzw. Optionscodes in einer Order kombiniert werden können. Die Einschränkungen können zahlreiche Gründe haben, insbesondere gesetzliche, technische oder vertriebliche.
Drei erfundene Konfigurationsbedingungen mit logischen Operatoren und Optionscodes in einer Notation ähnlich der von DAIMLER. ‚+‘ steht für ‚and‘, ‚/‘ für ‚or‘, ‚-‘ für ‚not‘. (Quelle: eigene Darstellung)
Die Menge dieser Bedingungen an alle Optionscodes entspricht in etwa der Modellbeschreibung von DAIMLER, genannt Produktübersicht (PÜ). Eine entsprechende Produktbeschreibungsformel (PDF) als Konjunktion aller Bedingungen, angereichert durch zusätzliche Logik zur Codierung einiger impliziter Annahmen, wurde erstmals in der zweiten Hälfte der 1990er-Jahre unter dem Namen Produktübersichtsformel (PÜF) eingeführt (Küchlin und Sinz 2000). Die ungefähre Größe einer solchen PDF für eine Baureihe beläuft sich typischerweise auf einige Hundert Kilobytes, wenn man von kompakten Codes aus wenigen Zeichen ausgeht.
Zum leichteren Verständnis kann man eine Modellbeschreibung zusätzlich in Familien verwandter Codes strukturieren. Eine Familie besteht jeweils aus einer Menge von Codes, von denen immer genau einer (exactly-one) in einer Order gewählt werden muss, wie z. B. eine Familie von Codes für Motoren, für Fahrersitze, für Getriebevarianten, etc. Die exactly-one Bedingungen aller Familien sind zunächst implizit gegeben und müssen in einer Booleschen PDF durch zusätzliche Constraints modelliert werden. Für Familien wie Anhängerkupplungen oder Schiebedächer wird ein zusätzlicher Null-Code vorgesehen, der gewählt wird, wenn keine Option dieser Familie verbaut werden soll. Damit einhergehend bietet sich eine weitere Strukturierung der Konfigurationsbedingungen an. Man dokumentiert dann, von welchen Kombinationen von fremden Codes die einzelnen Familienmitglieder impliziert werden. Die Coderegeln erhalten somit die Form (c1 ∧ …. ∧ cn → f1 ∨ … ∨ fm) wobei alle fi einer einzigen Familie angehören müssen. Diese Implikationen lassen sich unmittelbar als sogenannte Klauseln (¬c1 ∨ … ∨ ¬cn ∨ f1 ∨ … ∨ fm) darstellen und direkt in einen SAT-Solver eingeben.
Bei der eng verwandten CSP Modellierung hat man ebenfalls eine Familienstruktur, hier mit expliziten mehrwertigen Familienvariablen, deren Werte die einzelnen Familienmitglieder bezeichnen. Anforderungen an CSP-Solver aus Sicht der Automobilindustrie finden sich bei Astesana et al. (2010b). Falls ohnehin nur Boolesche Bedingungen vorkommen, bekommt man aber durch eine einfache Übersetzung in eine rein Boolesche PDF ein schnelles Lösungsverfahren mittels eines SAT-Solvers, wie etwa bei RENAULT (Pargamin 2002).
Es gibt auch gemischte Repräsentationen der MB, wo jede Bedingung wiederum aus einer DNF besteht, also konzeptionell aus einer Tabelle von baubaren Varianten (Variantentabelle). Die PDF besteht dann in erster Näherung aus der Konjunktion aller Tabellen, die über gemeinsame Variablen verbunden sind. Die Tabellen können wiederum einer Familienstruktur folgen. Man generiert durch geschickte Auswahl weniger Familien (z. B. Motoren und Getriebe) eine Tabelle aus Familienspalten und trägt jede baubare Kombination von Mitgliedern der Familien in jeweils eine Zeile ein. Diese Darstellung ähnelt traditionellen Papiertabellen, bei denen pro Zeile eine baubare Kombination durch Kreuze in den jeweiligen Spalten notiert wird. Für diese Darstellungsform wurde bei RENAULT Ende der 1990er-Jahre ein spezieller SAT-Solver entwickelt und zunächst für einen webbasierten Konfigurator verwendet (Pargamin 2002).
4 Logik-basierte Fahrzeugkonfiguration
Der unmittelbarste Nutzen einer PDF ergibt sich als logische Basis für einen Fahrzeugkonfigurator, denn die Bedingungen, die die Kombinationsmöglichkeiten von Optionen einschränken, können auch als Konfigurationsregeln interpretiert werden. Eine übliche Order auf Papier führt eine Menge S von Codes für Ausstattungen auf, die alle im Fahrzeug enthalten sein müssen. Ausstattungen, deren Codes fehlen, werden auch nicht in der Order enthalten sein. Damit ist die Order vollständig beschrieben und es ergibt sich in natürlicher Weise eine Variablenbelegung von true für alle Codes in S, und mit false für alle anderen Codes. Wir erhalten damit einen einfachen Prüfer für die Korrektheit einer so ergänzten vollständigen Order: Eine vollständige Order ist valide (bzw. als Fahrzeug baubar), wenn sie alle Bedingungen der PD erfüllt, bzw. wenn ihre Variablenbelegung ein logisches Modell der PDF darstellt. Dies kann ohne SAT-Solver über eine einfache Evaluation der PDF festgestellt werden.
Während eines Konfigurationsprozesses, also beim sukzessiven Aufbau einer Fahrzeugbestellung, hat man es aber nur mit einer partiellen Order zu tun, die in jeder Iteration um einen weiteren Code ergänzt wird. Eine partielle Order P legt lediglich die Variablenbelegung der dort enthaltenen Codes fest; die Belegung aller anderen Codes wird erst im weiteren Verlauf des Konfigurationsprozesses bestimmt. Der Begriff der Baubarkeit lässt sich nun wie folgt übertragen: Eine partielle Order P, bestehend aus einer Menge von Codes und deren Wahrheitsbelegungen (im einfachsten Fall ist dies jeweils true), heißt valide bzw. baubar, falls es eine vollständige valide Order gibt, deren Variablenbelegungen auf den entsprechenden Codes mit P übereinstimmen. Anders gesprochen: P ist baubar, falls P in geeigneter Weise zu einer vollständigen validen Order O ergänzt werden kann. Es lässt sich also aufgrund von O ein Fahrzeug bauen, das die gemäß P gewünschten Optionen enthält (und im Allgemeinen weitere andere). Falls P baubar ist, lässt sich eine solche Order O als Berechnungsergebnis eines SAT-Solvers finden (wobei das Ergebnis i. A. natürlich nicht eindeutig ist).
In offensichtlicher Weise lassen sich, ausgehend von P, auch alle insgesamt noch zur Verfügung stehenden Ausstattungen ermitteln: Für jeden noch nicht belegten Code C wird der Reihe nach geprüft, ob die um C erweiterte partielle Order immer noch baubar ist.
Der so entstehende Konfigurator hat einige Vorteile, die ihn besonders als Hilfsmittel der Dokumentationsabteilung wertvoll machen: er arbeitet unmittelbar auf der Modellbeschreibung ohne jede weitere Umcodierung in andere Konfigurationsregeln – er steht also nach jeder Regeländerung in der MB unmittelbar zur Verfügung; der Konfigurationsprozess ist außerdem unabhängig von einer festen Reihenfolge. Er ist in dem Sinn frei von Sackgassen, dass jedes valide P zu einer vollständigen Order ergänzt werden kann (falls gewünscht automatisch durch den SAT-Solver). Sackgassen können sich dennoch ergeben, wenn an einem Punkt nur eine andere als die gewünschte Order als Ergänzung möglich ist.
5 Die Varianten-Stückliste
Um das mit einer validen Fahrzeugorder bestellte Fahrzeug letztlich bauen zu können, muss man die dazu notwendigen Bauteile bestimmen; dies können z. B. mechanische, elektronische oder Softwarekomponenten sein, bis hin zu Klebeetiketten und Handbüchern in der passenden Sprache. Jede individuelle Order muss natürlich mit einer dazu genau passenden individuellen Menge von Bauteilen gefertigt werden; diese Liste von Teilen wird im Maschinenbau als Stückliste (Bill-of-Materials – BoM) bezeichnet. Bei herkömmlicher Fertigung mit wenigen Varianten kann die Stückliste für jede Maschine vor dem Verkauf bestimmt und gespeichert werden und steht dann für die Fertigung zur Verfügung. In der variantenreichen Massenfertigung des Automobilbaus ist dies nicht länger möglich. Die Stückliste enthält nun die Obermenge aller Teile, die für beliebige Fahrzeuge einer gesamten Baureihe gebraucht wird, sodass die individuelle Stückliste jedes Fahrzeugs als Teilmenge darin enthalten ist.
Diese Baureihen-Stückliste wird auch als Varianten-Stückliste (variant BoM) bezeichnet, da sie für jedes Teil alle seine Varianten enthält (z. B. alle Arten von Lenkrädern), die jemals für irgendeine Fahrzeugorder einer Baureihe gebraucht werden (z. B. Mercedes C-Klasse, BMW 3er, AUDI A4, etc.). Vereinfacht besteht die BoM nun aus einer Abfolge von Positionen (wie z. B. die Lenkrad-Position), die jeweils in eine Menge von Positions-Varianten aufgefächert sind. Jede Position korrespondiert idealisiert zu einer geometrischen Einbauposition im Fahrzeug, an der ein prototypisches Teil (z. B. ein Lenkrad) positioniert ist. Die Positionsvarianten und die Positionsvarianten dokumentieren die konkreten Varianten dieses Teils, die für die verschiedenen Fahrzeugvarianten zur Verfügung stehen (z. B. alle verschiedenen Lenkräder). Anders gesprochen ist die idealisierte Varianten-Stückliste eine Liste aller für eine Baureihe zur Verfügung stehenden Teile, gruppiert nach Positionen bestehend aus den Varianten eines jeden Teils. Die Gesamtlänge hängt natürlich von der Komplexität der Baureihe ab und auch von der herstellerspezifischen Ausprägung (z. B. mögen die Softwarevarianten oder die Farbvarianten ausgelagert sein). Aber typischerweise enthält sie Tausende von Positionen mit insgesamt Zehntausenden Positionsvarianten.
Fiktive BoM Position Nr. 20020 für drei Reifenvarianten und Auswahlbedingungen mit Optionscodes (vereinfachte Regelnotation im Stil von DAIMLER). (Quelle: eigene Darstellung)
6 Symbolische Analyse und Verifikation
- 1.
Die obere Ebene der Modellbeschreibung (MB) beschäftigt sich mit der Konfiguration einer Order als Kombination von Ausstattungsoptionen (gegeben durch Codes). Sie ist durch eine Menge Boolescher Bedingungen gegeben und kann samt aller impliziten Annahmen hinreichend kompakt als eine einzige Formel (PDF) codiert werden.
- 2.
Die untere Ebene der Variantenstückliste (BoM) beschäftigt sich mit der Konfiguration des bestellten Produkts aus Einzelteilen „bis hin zur letzten Schraube und dem letzten Byte“. Hierzu ist zu jeder Teilevariante deren Boolesche Auswahlbedingung hinterlegt.
Wegen der schieren Menge und Größe der Formeln (für jede Baureihe Tausende Bedingungen in der MB, Zehntausende Auswahlbedingungen in der BoM) und zusätzlich der permanenten Anpassungen entlang des gesamten Lebenszyklus des Produkts, von der Entwicklung und dem Verkauf über die Produktion bis zum Ende der Ersatzteilversorgung, ist es für Menschen praktisch unmöglich, Fehler zu vermeiden. Andererseits können Fehler sehr kostspielig werden: Auf der oberen Ebene könnte ein Auftrag abgelehnt werden, obwohl er gebaut werden könnte, oder er könnte akzeptiert werden, obwohl er nicht gebaut werden kann oder darf. Auf der unteren Ebene kann die Auswahl eines falschen Teils eine Vielzahl von schweren Problemen nach sich ziehen, von Unterbrechungen am Fließband bis hin zu Problemen bei der Sicherheit oder der Homologation (offizielle Zertifizierung). Da etwa alle 90 Sekunden ein Fahrzeug das Fließband verlässt, sind auch kurze Unterbrechungen kostspielig.
- 1.
Welche Fehler sind praxisrelevant, und wie können die Fehlerfälle symbolisch beschrieben werden, um deren Anwesenheit oder Abwesenheit zu beweisen?
- 2.
Welche Beweisverfahren sind praxistauglich, also effizient genug und stabil genug für den Dauerbetrieb, ohne dass sie von Spezialisten wie Logikern, Mathematikern, oder Informatikern beaufsichtigt werden müssen und ohne dass die Anwender durch die Berechnungszeit in der eigentlichen Arbeit behindert werden?
Diese Fragen waren Hauptgegenstand der frühen Forschung (Küchlin und Sinz 2000; Sinz et al. 2003; Astesana et al. 2010a, b). Noch in den 1990er-Jahren war nicht klar, welche Beweisverfahren den Anforderungen der Praxis außerhalb des Labors genügen würden. Zunächst wurden einige spezielle SAT-Solver (Pargamin 2002; Sinz et al. 2003) und auch andere Spezialverfahren entwickelt. Unabhängig von der herstellerspezifischen Modellierungsart der MB ist es aber immer effizient möglich, eine PDF in Konjunktiver Normalform (CNF), d. h. als Menge von Klauseln herzustellen (Schöning 1987), sodass sie als Eingabe für einen Standard SAT-Solver verwendet werden kann. Inzwischen haben sich „lernende“ SAT-Solver nach dem CDCL Prinzip (Marques-Silva und Sakallah 1999; Biere et al. 2009) in jeder Beziehung als vollständig praxistauglich erwiesen. Die Dauer einzelner Solver-Aufrufe liegt üblicherweise im einstelligen Millisekunden-Bereich, Analysen ganzer Baureihen können allerdings eine hohe sechsstellige Anzahl von Aufrufen erfordern. CDCL-Solver liefern außerdem für unerfüllbare Formeln einen klassischen (aussagenlogischen) Resolutionsbeweis, der eine nachvollziehbare Erklärung des Widerspruchs und somit eine Ursachenforschung ermöglicht. Erklärbarkeit ist in der Praxis ungemein wichtig, denn Erklärungen komplexer Zusammenhänge liefern einen wertvollen (und oft den einzigen) Ansatz für die Beseitigung von tief liegenden Fehlern. Mittlerweile haben sich einige Standard-Analysen für die Modellbeschreibung und die Stückliste herauskristallisiert, die von vielen Herstellern angewendet werden.
6.1 Logische Analyse der Modellbeschreibung
Eine formale Verifikation der Modellbeschreibung ist schon deshalb nicht möglich, da die Modellbeschreibung die einzige formale Spezifikation des Produktangebots ist. Allerdings ist es möglich, durch automatische Beweisverfahren gewisse verborgene Eigenschaften der MB ans Tageslicht zu fördern, die sich erst durch das Zusammenspiel der vielen Bedingungen ergeben. Als Beispiel sei ein Code C mit der einzigen Zusteuerbedingung (A → C) gegeben. Es kann nun durchaus sein, dass diese Zusteuerbedingung sich schon als logische Konsequenz der Baubarkeitsbedingungen der MB ergibt, oder dass sich implizit eine weitere Zusteuerbedingung (B → C) ergibt, die nicht explizit dokumentiert ist. Ebenso kann es sein, dass die Baubarkeitsbedingungen in ihrem Zusammenspiel verbieten, dass A und C überhaupt gleichzeitig in einer Order vorkommen, sodass als logische Konsequenz A=false folgt. Dadurch wäre einerseits „A“ als Bestelloption „ausgehebelt“, andererseits wäre (A → C) als Konfigurationsregel wirkungslos, da C ihretwegen nie zugesteuert würde. In jedem Fall wäre ein mögliches Missverständnis bei der Dokumentation zu vermuten, dem man nachgehen sollte.
Eine übliche Analyse der Modellbeschreibung untersucht jeden Code auf seinen Status (Kaiser und Küchlin 2001a): Der Status von C ist zwingend bzw. notwendig, wenn C in jeder validen Order (positiv) vorkommen muss; unmöglich bzw. überflüssig, wenn C in keiner validen Order (positiv) vorkommen kann; andernfalls optional. In heutiger Terminologie geht es um die Bestimmung des positiven und negativen Rückgrats (backbone) der MB und dessen möglichst effiziente Berechnung (Kaiser und Küchlin 2001a).
In der Praxis kommen Codes, die für Kunden sichtbar und wählbar sind, nur in Ausnahmefällen im Backbone der MB vor, z. B. als unmöglich kurz vor ihrer Freischaltung bei einem Modellwechsel. Fehlerfälle sind allerdings oftmals signifikant: Ein unmöglicher Landescode macht Orders für ein ganzes Land unmöglich, ein unabsichtlich zwingender oder unmöglicher Ausstattungscode schränkt die Wahlfreiheit des Kunden unnötig ein. Allerdings enthält die MB auch interne Herstellercodes (Zengler und Küchlin 2013); falls der interne Code für eine Batterieversion unmöglich ist, so wird diese nie verbaut. Die Typisierung der Codes ist besonders für Teilmengen des Produktangebots nützlich, z. B. für bestimmte Märkte oder Motor-Getriebe Kombinationen (sog. Baumuster innerhalb der Baureihe). Man möchte bzw. muss wissen, welche Codes im jeweiligen Kontext zwingend oder verboten sind, besonders wenn sie für die Homologation (Zertifizierung) relevant sind, wie z. B. Reifengrößen in Verbindung mit einem Motor.
6.2 Logische Analyse der Varianten-Stückliste
Wie bei der Modellbeschreibung gibt es auch bei der Stückliste keine weitere formale Spezifikation, gegen die man verifizieren könnte. Allerdings gibt es für eine idealisierte Stückliste eine zentrale Korrektheitsbedingung, die unabhängig vom Fahrzeughersteller gilt: Im Kern muss jede Fahrzeugkonfiguration an jeder Position der Stückliste genau eine Variante „treffen“ (auswählen). Diese Bedingung wird üblicherweise in die beiden Analysen auf Doppeltreffer und Fehltreffer aufgebrochen. Außerdem möchte man die Stückliste (und damit auch das Lager) um unnötige Teile bereinigen und analysiert daher auch das Vorkommen von Waisen (Küchlin und Sinz 2000; Sinz et al. 2003):
Doppeltreffer: Eine Fahrzeugkonfiguration erzeugt an einer Position einen Doppeltreffer, wenn sie dort zwei Positionsvarianten (und damit zwei alternative Teile) gleichzeitig trifft.
Fehltreffer: Eine Fahrzeugkonfiguration erzeugt an einer Position einen Fehltreffer, wenn sie dort keine der Varianten (und damit kein Teil) trifft. Eine Position zu der es Fehltreffer gibt, ist unvollständig, da sie nicht alle Orders abdeckt; andernfalls ist sie vollständig.
Waisen: Eine Teilevariante, die von keiner Fahrzeugkonfiguration getroffen werden kann, ist an dieser Position eine Waise (das Teil ist dort überflüssig).
Exemplarische Fehlerfälle an einer fiktiven BoM Position. (Quelle: eigene Darstellung)
Offensichtlich kommt es in allen Fällen nur auf valide Fahrzeugkonfigurationen an. Angesichts der astronomischen Varianz kann man sich für eine Validierung aber nicht damit begnügen, eine Modellbeschreibung nur bezüglich einer gegebenen (notwendigerweise kleinen) Menge von Orders zu überprüfen, z. B. bezüglich des Produktionsvolumens des letzten Jahres. Stattdessen muss man nach der Existenz von theoretisch möglichen Orders bezüglich der MB suchen. Dazu muss man das Regelwerk der MB mit dem Regelwerk der BoM in Beziehung setzen. Dies gelang erstmals ab etwa 1996 mit der Hilfe eines SAT-Solvers (Küchlin and Sinz 2000; Sinz et al. 2003).
7 Zusammenfassung
Das Management von Konfigurationsbedingungen, ihre Analyse und Verifikation, ist eine der großen Geschäftsanwendungen der klassischen symbolischen KI in Form von Aussagenlogik und Automatischem Beweisen mittels SAT-Solving. (Andere wichtige Anwendungen sind z. B. die Verifikation von mikroelektronischen Schaltungen und von Software.) Aus Sicht der KI geht es in allen Fällen darum, vollautomatisch Schlussfolgerungen aus den Gegebenheiten der Umwelt (hier der Produktvielfalt) zu ziehen bzw. auf intelligente Weise Fragen über die Umwelt beantworten zu können. In der Tat sind neue Anwender oft über die Intelligenz einer Antwort verblüfft, bis sie die logische Erklärung gesehen und Schritt für Schritt nachvollzogen haben.
Das Geschäftsmodell der individualisierten Massenfertigung verlangt konfigurierbare, aus austauschbaren Modulen aufgebaute Produkte. Das Konzept von Industrie 4.0 propagiert einen voll automatisierten Informationsfluss ausgehend von der Kundenseite, wo das Produkt im Internet konfiguriert und bestellt wird, über die Produktion und die Auslieferung bis zur Rechnungsstellung und Bezahlung. Dies bedeutet, dass die Konfiguration und die Herstellung des Produkts möglichst ohne menschliche Intervention erfolgen sollte. Modellbeschreibung und Stückliste müssen daher absolut fehlerfrei sein.
Obwohl die Automobilindustrie eben erst den Übergang zur Internet basierten Bestellung beginnt, perfektioniert sie bereits seit längerem die individualisierte Massenproduktion und hat daher eine starke Motivation für eine fehlerfreie Produktdokumentation. Dies gilt insbesondere für die deutschen Hersteller von Premiumfahrzeugen, die hoch konfigurierbare Fahrzeuge mit zahlreichen Sonderausstattungen in praktisch alle Länder der Erde verkaufen. Jeder Fehler in der Produktdokumentation schlägt sich hier früher oder später im Fahrzeug nieder und sorgt für teilweise hohe Kosten, sei es am Band oder bei Rückrufen.
Der Erfolg des symbolischen Ansatzes auf diesem Gebiet beruht auf der besonders glücklichen Kombination der relativ einfachen Aussagenlogik mit dem hocheffizienten Lösungsverfahren des CDCL SAT-Solving. Aussagenlogik („the rules of thought“ – George Boole) kann auch von Nicht-Logikern verstanden werden, ist aber gleichzeitig mächtig genug, um das Anwendungsproblem zu beschreiben. Daher kann die Modellierung im Wesentlichen bereits von Industrieseite erbracht werden. Die Ergebnisse der Beweisverfahren stehen daher im engen Bezug zur Anwendung und sind somit nicht nur rein mathematisch korrekt, sondern auch auf der Anwendungsseite bedeutungsvoll und nützlich. Die klassischen Analysen laufen bequem in der Komfortzone eines CDCL-Solvers. Überraschende Verzögerungen oder gar Abstürze kommen nicht vor. Außerdem gibt es ein reiches Ökosystem an weiteren Methoden, Algorithmen und Implementierungen, sowie an Forschung und Erfahrung im Umfeld des SAT-Solving, was neue Anwendungen erleichtert (Biere et al. 2009).
Weitere wichtige Themenkreise für den Einsatz automatischer Beweis- und Berechnungsverfahren in diesem Umfeld sind u. a. die automatische Berechnung von Ursachen und Erklärungen für die Ergebnisse (Kaiser und Küchlin 2001c; Walter et al. 2017), die Unterstützung für den Aufbau nachweislich korrekter Modellbeschreibungen und Stücklisten, sowie Optimierungsverfahren für die Konfiguration (Walter et al. 2013; Walter und Küchlin 2014) und für die Planung (Walter et al. 2015).
Die hier beschriebenen Methoden sind so oder in ähnlicher Weise im täglichen Produktiveinsatz bei mindestens 8 Automobilmarken in Deutschland, Frankreich und den USA. Dieser Artikel reflektiert im Wesentlichen unsere Tübinger Forschungsergebnisse, Entwicklungen und Erfahrungen aus dem Technologietransfer seit etwa 1996, aus dem die Erstausrüstung der Software für bislang 4 Automobilhersteller hervorging. Eine umfassendere Behandlung von alternativen Entwicklungen im Automobilbereich sowie von Konfigurationsproblemen in anderen Kontexten war im Rahmen dieses Beitrags nicht möglich.
Die Erforschung, Entwicklung und Anwendung der beschriebenen Methoden am Arbeitsbereich für Symbolisches Rechnen und am Steinbeis Transferzentrum STZ OIT an der Universität Tübingen wäre nicht möglich gewesen ohne eine Vielzahl von engagierten Doktoranden, Mitarbeitern und Kunden. Besonderer Dank gilt der damaligen DaimlerChrysler AG für die Förderung des initialen universitären Forschungsprojekts.