What Are SAT Solvers Good For in Variant Management?

SAT solving is perhaps the most important core technology in variant management that hardly anyone has heard of. These algorithms work under the hood of product configurators and variant management tools, often without users having any idea what is actually going on. I’d like to change that.

What’s behind “SAT”?

SAT stands for satisfiability. At its core, a SAT problem asks: is there an assignment of truth values (true/false) to a set of variables that satisfies a given logical formula?

That sounds abstract, but it is surprisingly useful. Many real-life problems can be translated into exactly this form, and variant management is one of them.

Variant management has many facets

I spend a lot of time on variant-rich products. It’s a broad field, from product architecture and configuration rules to the tools that manage all of it. And if you look at these tools more closely, sooner or later you run into the term SAT solving.

Without a computer science background, it’s an unfamiliar term at first. Still, it is the technical foundation of many product configurators and other variant management tools.

In simple terms: you can hand a SAT solver all the rules that span a product’s variant space. For example, that convertibles only come without a sunroof, or that the sport version of a car needs a larger brake disc. The solver can then check whether any valid (that is, “satisfiable”) variants exist under all of these rules, or whether the rules contradict each other so much that nothing could be built anymore.

How the SAT solver thinks

A SAT solver receives a list of constraints (logical expressions) and then searches for an assignment that satisfies all of them at the same time. In variant management, these constraints look like this, for example:

• “If convertible, then no sunroof”
• “If sport package, then brake disc size XL”
• “Leather upholstery only on 4-seaters”

If I now ask, “Are there convertibles with leather upholstery?”, the solver has to check whether a variant exists that satisfies both “convertible” and “leather upholstery” at the same time. That isn’t trivial, because there may be no direct rule for it.

But there could be one indirectly: leather only on 4-seaters, convertibles only as 2-seaters, so no convertible with leather. The SAT solver finds this even without a direct rule, because it sees the entire constraint network at once.

In this case I’d want to have a word with the responsible product manager 😉, but the solver has reliably identified an impossible combination.

SAT solvers enable many use cases

With cleverly formulated queries, SAT solvers can answer far more questions than just “does this variant exist?”:

• Validation: Is the entire variant space free of contradictions? Are there dead variants that can never be built because of conflicting rules?
• Configuration guidance: If a customer has chosen “convertible”, which options are still available, and which are ruled out automatically?
• Impact analysis: When a new rule is added, what changes in the variant space?
• Product portfolio analysis: How many valid variants are there in total? Which combinations are never used?

For complex products with dozens or hundreds of variation points, these analyses simply can’t be done by hand. A SAT solver does them in milliseconds.

Where SAT solvers are used

Many commercial tools for variant management and product configuration rely on SAT solving: ConfigIt, SAP variant configuration, pure::variants, and this technology is also widespread in specialised automotive tools. Most users never notice, because the solver works deep inside the system.

If you want to experiment with a SAT solver yourself, you don’t need to set up a software project right away. MiniZinc is a free tool that embeds SAT solvers in its own modelling language, and it even runs in the browser. I’ll show how exactly that works in the follow-up article on MiniZinc and first steps with SAT solvers.