From Decision Models To User-Guiding Configurators Using SMT

As decision models for the correct derivation of customizable products grow ever more complex, user-facing configurators are developed to manage this complexity by emulating the models as closely as possible. By design, decision models closely resemble the structures of configurators. Therefore, a classical configurator that implements a decision model often copies the model’s (linear) ordering of decisions. To enable users to jump into arbitrary points of a decision model, non-linear analysis is necessary. We present a novel way of automatically encoding a complex decision model into Satisfiability Modulo Theories (SMT) formulas, which are then solved by an SMT solver. Users interact with a configurator front-end, which internally calls an incremental SMT solver that returns open choices. In this paper, we present the architecture of our framework, introduce a general direct SMT encoding of decision models, and illustrate with a small case study the potential of our approach for product configuration and reconfiguration. Our approach successfully converts a legacy ordered decision model from an industrial application into a fully interactive configurator.