I recently wrote a post about what a SAT solver is and why it is an important foundational technology for variant management. Under the hood of many variant management tools, including product configurators, there are SAT solvers at work. A good reason to take a closer look at this technology 👍🙂
In fact, there is a whole range of freely available SAT solvers,… but only as code libraries for use in your own software projects. So for “experimenting”, these libraries are only suitable for people who enjoy programming. And commercially usable product configurators or variant management tools (e.g. ConfigIt, pure::variants or SAP variant configuration) mostly cost money, and not a little. The tools are worth it, but for learning and experimenting something cheaper will do just fine 😉
MiniZinc, the SAT solver experimentation kit
Okay, maybe the heading is a bit of a simplification. MiniZinc is actually a declarative modeling language of its own. With it you can model various “problems” (e.g. variant spaces…), which can then be handed to “problem solvers”. These “problem solvers” include SAT solvers, but also several others. What matters for us: MiniZinc is available for download and comes with everything we need for experimenting. An editor, various SAT solvers, all installed with a single click, practically. And if you would rather not download anything, there is now also a web version: https://play.minizinc.dev/
To run the example from my video, all you really have to do is the following:
- Download and install MiniZinc (download here) or go to the web version
- Copy the code below to your clipboard (or download the example file below)
- Paste the code into MiniZinc and click “Run”
… voilà. That’s it 😉
The code already contains the two constraints for the use case of whether convertibles with leather seats can be built. If you want the “pure” variant space, simply remove those two lines or comment them out (in MiniZinc with % at the start of the line).
Commented example code from the video
/*****************************************
* Definition des baubaren Variantenraums *
*****************************************/
% Für jeden Variationspunkt müssen wir eine Variable deklarieren
% Variationspunkte sind die Eigenschaften der Baureihe, die je
% Fahrzeug unterschiedlich sein können.
%
% Jede Variable benötigt einen Datentyp. Es gibt vordefinierte
% Datentypen, wie z.B. Integer oder Boolean. Benötigen wir eigene
% Datentypen, müssen wir diese erst definieren.
% Typen definieren
enum eFahrzeugtyp = {Cabrio, Coupe, Kombi};
enum eAusstattungspaket = {Standard, Business, Sport};
enum eBremsscheibe = {BrStandard, BrGross};
enum eSitzkonfiguration = {Sitze2, Sitze4};
enum eSitzbezug = {Stoff, Leder};
% Variablen deklarieren
var eFahrzeugtyp: Fahrzeugtyp;
var eAusstattungspaket: Ausstattungspaket;
var eBremsscheibe: Bremsscheibe;
var eSitzkonfiguration: Sitzkonfiguration;
var eSitzbezug: Sitzbezug;
var bool: Schiebedach;
% Variantenraum beschreiben
% Nun beschreiben wir, wie die Variationspunkte zueinander in Be-
% ziehung stehen (in SAP würde man deshalb "Beziehungswissen"
% sagen. In MiniZinc erfolgt das mit dem Schlüsselwort "constraint"
% Wenn es ein Cabrio ist, kann es kein Schiebedach haben, und
% außerdem muss es ein 2-Sitzer sein
constraint Fahrzeugtyp = Cabrio -> Schiebedach = false;
constraint Fahrzeugtyp = Cabrio -> Sitzkonfiguration = Sitze2;
% Beim Ausstattungspaket "Sport" ist die große Bremsscheibe drin
constraint Ausstattungspaket = Sport -> Bremsscheibe = BrGross;
% Der Produktmanager hat wohl entschieden, dass es Ledersitze nur
% beim 4-Sitzer geben darf
constraint Sitzbezug = Leder -> Sitzkonfiguration = Sitze4;
/*******************************************************
* Usecase: kann es Cabrios mit Lederausstattung geben? *
********************************************************/
constraint Fahrzeugtyp = Cabrio;
constraint Sitzbezug = Leder;
% Schließlich sagen wir noch dem Solver, dass wir auf Erfüllbarkeit
% prüfen wollen
solve satisfy;