Di recente ho pubblicato un articolo su cosa sia un SAT-Solver e perché sia una tecnologia di base importante per la gestione delle varianti. In molti tool per la gestione delle varianti, quindi anche nei configuratori di prodotto, sotto il cofano lavorano proprio questi SAT-Solver. Un buon motivo per approfondire questa tecnologia 👍🙂
Esistono addirittura diversi SAT-Solver disponibili gratuitamente… solo che sono librerie di codice da integrare nei propri progetti software. Per «sperimentare» con questi, quindi, queste librerie sono adatte solo a chi ama programmare. E i configuratori di prodotto o i tool per la gestione delle varianti utilizzabili commercialmente (ad esempio ConfigIt, pure::variants o anche la configurazione delle varianti SAP) di solito costano, e non poco. Questi tool ne valgono il prezzo, ma per imparare e sperimentare va benissimo anche qualcosa di più economico 😉
MiniZinc, il kit per sperimentare con i SAT-Solver
Ok, forse il titolo lo semplifica un po’ troppo. In realtà MiniZinc è un vero e proprio linguaggio di modellazione dichiarativo. Con questo si possono modellare diversi «problemi» (ad esempio spazi di variante…) che poi vengono passati a dei «risolutori». Tra i «risolutori» ci sono i SAT-Solver, ma anche altri. La cosa decisiva per noi: MiniZinc si può scaricare e porta con sé tutto quello che serve per sperimentare. Un editor, diversi SAT-Solver, praticamente tutto installato con un clic. E per chi preferisce evitare il download, ora esiste anche una versione web: https://play.minizinc.dev/
Per eseguire l’esempio del mio video devi solo fare questo:
- Scarica e installa MiniZinc (link al download sopra) oppure vai sulla versione web
- Copia il codice qui sotto negli appunti (oppure scarica il file di esempio qui sotto)
- Incolla il codice in MiniZinc e clicca su «Run»
… voilà. Tutto qui 😉
Il codice contiene già i due vincoli per il caso d’uso: verificare se si possono costruire cabriolet con sedili in pelle. Se vuoi ottenere lo spazio di variante «puro», basta rimuovere queste due righe o commentarle (in MiniZinc con % a inizio riga).
Codice di esempio commentato dal 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;
