Wofür sind SAT-Solver im Variantenmanagement gut?

SAT-Solving ist die vielleicht wichtigste Basistechnologie für Variantenmanagement, die kaum einer kennt. In Produktkonfiguratoren und Variantenmanagement-Tools werkeln diese Algorithmen unter der Haube — oft ohne dass die Nutzer ahnen, was da eigentlich passiert. Das möchte ich ändern.

Was steckt hinter “SAT”?

SAT steht für Satisfiability — auf Deutsch: Erfüllbarkeit. Ein SAT-Problem fragt im Kern: Gibt es eine Belegung von Wahrheitswerten (wahr/falsch) für eine Menge von Variablen, die eine vorgegebene logische Formel erfüllt?

Das klingt abstrakt, ist aber erschreckend nützlich. Denn viele Probleme aus dem echten Leben lassen sich in genau diese Form übersetzen — auch das Variantenmanagement.

Variantenmanagement hat viele Facetten

Ich beschäftige mich viel mit variantenreichen Produkten. Das ist ein weites Feld — von der Produktarchitektur über Konfigurationsregeln bis hin zu Tools, die all das verwalten. Und wenn man sich diese Tools näher anschaut, stolpert man früher oder später über den Begriff SAT-Solving.

Ohne Informatik-Hintergrund ist das erst einmal ein Fremdwort. Trotzdem ist es die technische Grundlage vieler Produktkonfiguratoren und anderer Werkzeuge für Variantenmanagement.

Vereinfacht gesagt: Man kann einem SAT-Solver alle Regeln übergeben, die den Variantenraum eines Produkts aufspannen. Also zum Beispiel, dass es Cabrios nur ohne Schiebedach gibt — oder dass die Sportausführung eines Autos eine größere Bremsscheibe braucht. Der Solver kann dann prüfen, ob es bei all diesen Regeln überhaupt gültige (also „erfüllbare”) Varianten gibt — oder ob die Regeln sich so widersprechen, dass nichts mehr baubar wäre.

Wie der SAT-Solver denkt

Ein SAT-Solver bekommt eine Liste von Constraints — logische Ausdrücke — und sucht dann nach einer Belegung, die alle gleichzeitig erfüllt. Im Variantenmanagement sehen diese Constraints zum Beispiel so aus:

• „Wenn Cabrio, dann kein Schiebedach”
• „Wenn Sportpaket, dann Bremsscheibe Größe XL”
• „Lederausstattung nur bei 4-Sitzern”

Wenn ich jetzt frage: „Gibt es Cabrios mit Lederausstattung?”, muss der Solver prüfen, ob eine Variante existiert, die gleichzeitig „Cabrio” und „Lederausstattung” erfüllt. Das ist nicht trivial — denn eine solche direkte Regel gibt es vielleicht gar nicht.

Aber über Bande könnte es eine geben: Leder nur bei 4-Sitzern, Cabrio nur als 2-Sitzer — ergo: kein Cabrio mit Leder. Der SAT-Solver findet das auch ohne eine direkte Regel, weil er das gesamte Constraint-Netz im Blick hat.

In diesem Fall würde ich dann mit dem verantwortlichen Produktmanager mal ein Wörtchen reden wollen 😉 — aber der Solver hat zuverlässig eine unmögliche Kombination identifiziert.

SAT-Solver ermöglichen viele Anwendungsfälle

Über geschickt formulierte Anfragen lassen sich mit SAT-Solvern deutlich mehr Fragen beantworten als nur „gibt es diese Variante?”:

• Validierung: Ist der gesamte Variantenraum widerspruchsfrei? Gibt es tote Varianten, die durch sich widersprechende Regeln nie baubar werden?
• Konfigurationsführung: Wenn ein Kunde „Cabrio” gewählt hat, welche Optionen sind jetzt noch wählbar, und welche scheiden automatisch aus?
• Impact-Analyse: Wenn eine neue Regel hinzukommt — was ändert sich am Variantenraum?
• Produktportfolio-Analyse: Wie viele gültige Varianten gibt es überhaupt? Welche Kombinationen sind nie vergeben?

Diese Analysen sind bei komplexen Produkten mit Dutzenden oder Hunderten von Variationspunkten von Hand schlicht nicht durchführbar. Ein SAT-Solver erledigt sie in Millisekunden.

Wo SAT-Solver im Einsatz sind

Viele kommerzielle Tools für Variantenmanagement und Produktkonfiguration setzen auf SAT-Solving: ConfigIt, SAP Variantenkonfiguration, pure::variants — und auch in spezialisierten Automotive-Tools ist diese Technologie verbreitet. Die meisten Nutzer bekommen davon gar nichts mit, weil der Solver tief im System arbeitet.

Wer selbst mit einem SAT-Solver experimentieren möchte, muss nicht gleich ein Software-Projekt aufsetzen. MiniZinc ist ein freies Werkzeug, das SAT-Solver in eine eigene Modellierungssprache einbettet — und sogar im Browser läuft. Wie das genau funktioniert, zeige ich im Folgeartikel über MiniZinc und erste Schritte mit SAT-Solvern.