Il SAT-solving è forse la tecnologia di base più importante per la gestione delle varianti, eppure quasi nessuno la conosce. Nei configuratori di prodotto e negli strumenti per la gestione delle varianti questi algoritmi lavorano sotto il cofano — spesso senza che gli utenti si rendano conto di cosa stia realmente succedendo. È quello che voglio cambiare.
Cosa significa «SAT»?
SAT sta per Satisfiability — in italiano: soddisfacibilità. Un problema SAT pone in sostanza questa domanda: esiste un’assegnazione di valori di verità (vero/falso) a un insieme di variabili che soddisfi una formula logica data?
Sembra astratto, ma è sorprendentemente utile. Perché molti problemi della vita reale si possono tradurre esattamente in questa forma — anche la gestione delle varianti.
La gestione delle varianti ha molte facce
Mi occupo molto di prodotti ricchi di varianti. È un campo vasto — dall’architettura di prodotto alle regole di configurazione, fino ai tool che gestiscono tutto questo. E se si guardano questi tool più da vicino, prima o poi ci si imbatte nel termine SAT-solving.
Senza un background informatico, all’inizio è un termine estraneo. Eppure è il fondamento tecnico di molti configuratori di prodotto e di altri strumenti per la gestione delle varianti.
In parole semplici: si possono passare a un SAT-Solver tutte le regole che delimitano lo spazio di variante di un prodotto. Per esempio, che i cabriolet esistono solo senza tettuccio apribile — oppure che la versione sportiva di un’auto richiede un disco freno più grande. Il solver può quindi verificare se, con tutte queste regole, esistono varianti valide (cioè «soddisfacibili») — oppure se le regole si contraddicono in modo tale che non sarebbe più possibile costruire nulla.
Come pensa il SAT-Solver
Un SAT-Solver riceve un elenco di vincoli — espressioni logiche — e cerca poi un’assegnazione che li soddisfi tutti simultaneamente. Nella gestione delle varianti questi vincoli si presentano ad esempio così:
- «Se cabriolet, allora nessun tettuccio apribile»
- «Se pacchetto sportivo, allora disco freno taglia XL»
- «Interni in pelle solo nelle versioni a 4 posti»
Se ora chiedo: «Esistono cabriolet con interni in pelle?», il solver deve verificare se esiste una variante che soddisfa contemporaneamente «cabriolet» e «interni in pelle». Non è banale — perché una regola diretta di questo tipo magari non esiste affatto.
Ma indirettamente potrebbe esisterne una: pelle solo nelle versioni a 4 posti, cabriolet solo a 2 posti — quindi: nessun cabriolet con pelle. Il SAT-Solver lo scopre anche senza una regola diretta, perché ha una visione d’insieme di tutta la rete di vincoli.
In questo caso vorrei proprio scambiare due parole con il product manager responsabile 😉 — ma il solver ha individuato in modo affidabile una combinazione impossibile.
I SAT-Solver abilitano molti casi d’uso
Con richieste formulate in modo intelligente, i SAT-Solver permettono di rispondere a molte più domande che il semplice «esiste questa variante?»:
- Validazione: lo spazio di variante nel suo insieme è privo di contraddizioni? Esistono varianti morte, mai costruibili a causa di regole che si contraddicono?
- Guida alla configurazione: se un cliente ha scelto «cabriolet», quali opzioni restano selezionabili, e quali vengono automaticamente escluse?
- Analisi d’impatto: quando si aggiunge una nuova regola — cosa cambia nello spazio di variante?
- Analisi del portafoglio prodotti: quante varianti valide esistono in totale? Quali combinazioni non vengono mai assegnate?
Per prodotti complessi con decine o centinaia di punti di variazione, queste analisi semplicemente non sono realizzabili a mano. Un SAT-Solver le esegue in millisecondi.
Dove vengono usati i SAT-Solver
Molti tool commerciali per la gestione delle varianti e la configurazione di prodotto si basano sul SAT-solving: ConfigIt, la configurazione delle varianti SAP, pure::variants — e anche negli strumenti specializzati per l’automotive questa tecnologia è diffusa. La maggior parte degli utenti non se ne accorge affatto, perché il solver lavora in profondità nel sistema.
Chi vuole sperimentare in prima persona con un SAT-Solver non deve subito avviare un progetto software. MiniZinc è uno strumento libero che integra i SAT-Solver in un proprio linguaggio di modellazione — e funziona persino nel browser. Come funziona esattamente lo mostro nell’articolo successivo su MiniZinc e i primi passi con i SAT-Solver.
I SAT-Solver non sono un gioco accademico — sono il fondamento tecnico dei configuratori di prodotto moderni. Chi capisce come lavorano, capisce meglio perché le regole di configurazione devono essere formulate come sono formulate, e perché alcune domande sullo spazio di variante possono ricevere una risposta sorprendentemente rapida.
