CSP Solver

A CSP solver (Constraint Satisfaction Problem solver) is an algorithm that finds assignments of values to variables such that all defined constraints are simultaneously satisfied. CSP stands for Constraint Satisfaction Problem. In variant management, CSP solvers extend the capabilities of Boolean SAT solvers SAT Solver (ˌes-ˌā-ˈtē ˈsäl-vər) n. A SAT solver determines whether a Boolean formula is satisfiable — used in variant management to validate configurations and navigate large variant spaces. by handling richer constraint types — numeric ranges, set membership, and ordering conditions — making them suitable for configuration Configuration (kən-ˌfi-gyə-ˈrā-shən) n. Configuration has three distinct meanings in PLM: variant configuration, configuration management, and parameterization — each describing a different kind of joining. problems that go beyond simple option compatibility rules.

How CSP solving works

A Constraint Satisfaction Problem is defined by three elements:

• Variables — the unknowns to be assigned values (e.g., engine power, frame size, color).
• Domains — the set of allowed values for each variable (e.g., engine power: 100 kW, 150 kW, or 200 kW).
• Constraints — conditions that valid assignments must satisfy (e.g., “if engine power = 200 kW, then cooling system = heavy-duty”).

A CSP solver searches for an assignment that satisfies all constraints simultaneously, using techniques such as backtracking search, arc consistency propagation, and look-ahead to prune the search space efficiently. If no valid assignment exists, the solver reports infeasibility — which in a product context means the selected combination cannot be built.

CSP solvers and SAT solvers

Boolean satisfiability (SAT) is a special case of constraint satisfaction: a SAT problem is a CSP where all variables are Boolean (true/false) and all constraints are expressed as Boolean clauses. SAT solvers are highly optimised for this restricted case and typically outperform general CSP solvers on purely Boolean problems. CSP solvers handle the more general case where variables can take integer, real, or enumerated values.

In variant management practice:

• SAT solvers are most common in feature-model-based tools and product configurators where all rules are Boolean — option A requires option B; option C excludes option D.
• CSP solvers are applied when configuration rules involve numeric conditions — weight budgets, price constraints Constraint (kən-ˈstrānt) n. A constraint is a rule that restricts valid option combinations in a variant configuration model, turning a theoretical variant space into a set of buildable configurations. , geometric compatibility — as encountered in configure-to-order or engineer-to-order contexts.

SMT solvers (Satisfiability Modulo Theories) combine Boolean SAT with CSP-style numeric reasoning in a single engine and are increasingly used in complex variant management scenarios.

Examples

• Industrial machinery — A configure-to-order tool uses a CSP solver to enforce constraints such as “motor output must not exceed frame load capacity” and “if conveyor speed exceeds 2 m/s, motor power must be at least 15 kW” — conditions that cannot be expressed in pure Boolean logic.
• Embedded software configuration — During variant-specific software builds, a CSP solver checks that the combined memory footprint of selected software components does not exceed the available flash memory on the target hardware variant.

Frequently asked questions