El SAT-solving es quizás la tecnología básica más importante de la gestión de variantes, y casi nadie la conoce. En los configuradores de producto y las herramientas de gestión de variantes, estos algoritmos trabajan por debajo del capó, muchas veces sin que los usuarios sospechen lo que realmente está pasando. Eso es lo que quiero cambiar.
¿Qué hay detrás de “SAT”?
SAT significa Satisfiability — en español: satisfacibilidad. Un problema SAT pregunta, en esencia: ¿existe una asignación de valores de verdad (verdadero/falso) para un conjunto de variables que satisfaga una fórmula lógica dada?
Suena abstracto, pero es sorprendentemente útil. Porque muchos problemas de la vida real se pueden traducir exactamente a esta forma, y la gestión de variantes no es la excepción.
La gestión de variantes tiene muchas facetas
Trabajo mucho con productos con gran variedad de variantes. Es un campo amplio, que va desde la arquitectura de producto y las reglas de configuración hasta las herramientas que gestionan todo eso. Y cuando se analizan estas herramientas de cerca, tarde o temprano se topa uno con el término SAT-solving.
Sin formación en informática, al principio es una palabra extraña. Aun así, es la base técnica de muchos configuradores de producto y otras herramientas de gestión de variantes.
Dicho de forma simplificada: a un SAT-solver se le pueden entregar todas las reglas que delimitan el espacio de variantes de un producto. Por ejemplo, que los descapotables solo existen sin techo corredizo, o que la versión deportiva de un coche necesita un disco de freno más grande. El solver puede entonces comprobar si, con todas esas reglas, existen variantes válidas (es decir, “satisfacibles”), o si las reglas se contradicen de tal forma que ya no se podría fabricar nada.
Cómo piensa el SAT-solver
Un SAT-solver recibe una lista de restricciones — expresiones lógicas — y busca una asignación que las satisfaga todas a la vez. En la gestión de variantes, estas restricciones se ven, por ejemplo, así:
- “Si descapotable, entonces sin techo corredizo”
- “Si paquete deportivo, entonces disco de freno talla XL”
- “Tapicería de cuero solo en versiones de 4 plazas”
Si ahora pregunto: “¿Existen descapotables con tapicería de cuero?”, el solver debe comprobar si existe una variante que cumpla simultáneamente “descapotable” y “tapicería de cuero”. Esto no es trivial, porque puede que no exista ninguna regla directa de ese tipo.
Pero de forma indirecta sí podría haberla: cuero solo en versiones de 4 plazas, descapotable solo como 2 plazas — por lo tanto: ningún descapotable con cuero. El SAT-solver encuentra esto incluso sin una regla directa, porque tiene a la vista toda la red de restricciones.
En ese caso, querría tener una conversación con el responsable de producto 😉 — pero el solver ha identificado de forma fiable una combinación imposible.
Los SAT-solvers permiten muchos casos de uso
Con consultas bien formuladas, los SAT-solvers permiten responder muchas más preguntas que solo “¿existe esta variante?”:
- Validación: ¿Es el espacio de variantes completo libre de contradicciones? ¿Hay variantes muertas que nunca se podrán fabricar por reglas que se contradicen entre sí?
- Guiado de configuración: Si un cliente ha elegido “descapotable”, ¿qué opciones siguen estando disponibles y cuáles quedan automáticamente excluidas?
- Análisis de impacto: Si se añade una nueva regla, ¿qué cambia en el espacio de variantes?
- Análisis de la cartera de producto: ¿Cuántas variantes válidas existen en total? ¿Qué combinaciones nunca se han asignado?
Estos análisis, en productos complejos con decenas o cientos de puntos de variación, sencillamente no se pueden realizar a mano. Un SAT-solver los resuelve en milisegundos.
Dónde se usan los SAT-solvers
Muchas herramientas comerciales de gestión de variantes y configuración de producto se apoyan en SAT-solving: ConfigIt, la configuración de variantes de SAP, pure::variants — y esta tecnología también está muy extendida en herramientas especializadas del sector automotriz. La mayoría de los usuarios no se dan cuenta de nada, porque el solver trabaja en lo más profundo del sistema.
Quien quiera experimentar por su cuenta con un SAT-solver no necesita montar todo un proyecto de software. MiniZinc es una herramienta libre que integra SAT-solvers en su propio lenguaje de modelado, y que incluso funciona en el navegador. Cómo funciona esto exactamente lo muestro en el artículo de seguimiento sobre MiniZinc y los primeros pasos con SAT-solvers.
Los SAT-solvers no son un juego académico: son el fundamento técnico de los configuradores de producto modernos. Quien entiende cómo trabajan, entiende mejor por qué las reglas de configuración deben formularse como se formulan, y por qué algunas preguntas sobre el espacio de variantes se pueden responder sorprendentemente rápido.
