What actually is a SAT solver?

Explore how SAT solvers underpin today’s variant management tools. This article explains how SAT solvers process complex product rules and enable advanced configuration analyses. Discover why SAT solvers are essential for building feasible product variants and how they can be applied in practical scenarios.

TOOLS

Julian Weyer

The many sides of variant management

Variant management is a complex field with a wide range of applications. When you start exploring the tools used in this area, one concept appears again and again: SAT solving.

If your background is not in computer science, SAT solvers might not be familiar territory. Still, they serve as the technological backbone for many product configurators and other variant management solutions.

In a nutshell, a SAT solver takes all the rules that define the possible variants of a product and processes them. For instance, you might have a rule that says convertibles cannot have a sunroof, or that the sports model of a car requires larger brake discs.

By analyzing these rules, the SAT solver can determine whether any valid (or “satisfyable”) product variants exist at all.

Unlocking Possibilities with SAT Solvers

SAT solvers are not just about checking if something is possible. They can also answer more advanced questions, provided you know how to frame your queries. For example, you might want to know whether it is possible to configure a convertible with leather upholstery. Even if there is no direct rule connecting “convertible” and “leather upholstery”, indirect rules might still apply.

Suppose one rule says leather upholstery is only available in four-seaters, while another specifies that convertibles are only made as two-seaters. In this scenario, the SAT solver would conclude that convertibles with leather upholstery are not possible (at which point you might want to discuss this limitation with the product manager).

There are many SAT solvers available as libraries, making it easy to integrate them into your own projects. If you are interested in experimenting with SAT solvers without any programming, you might find this article at JUWY.de helpful: Understanding variant spaces - First steps with MiniZinc (in German, English version coming soon).

VehicleType = Convertible -> Sunroof = false;

VehicleType = Convertible -> SeatConfiguration = Seats2;