Symbolic Reasoning for Industrial-Scale Variant Configuration

Configuration is omnipresent, whether by tweaking settings in applications or by customizing car equipment packages in an online configurator—naturally, an increasing number of options also increases the complexity as the possible number of combinations grows exponentially. Therefore, strong measures are needed to deal with this complexity. Decision modelling is a common approach to deal with this complexity and can be used as a base for configuration systems and for building configurators. This work originates from a research project with an industry partner, selling highly customizeable machines with many configuration options. It describes the development and results of the DMalizer framework, a framework to transform, analyze, and execute decision models. DMalizer provides an interactive configuration interface based on Satisfiability Modulo Theories formulas (SMT), which make a (linear) decision model usable for non-linear configuration. Evaluation of industry-sized decision models shows that the developed SMT encoding works satisfactorily for parts of the configuration.