Maximilian Heisinger, Florian Piminger, Martina Seidl,
"From Decision Models To User-Guiding Configurators Using SMT"
: VaMoS 2024: 18th International Working Conference on Variability Modelling of Software-Intensive Systems, Seite(n) 11-16, 2-2024
Original Titel:
From Decision Models To User-Guiding Configurators Using SMT
Sprache des Titels:
Englisch
Original Buchtitel:
VaMoS 2024: 18th International Working Conference on Variability Modelling of Software-Intensive Systems
Original Kurzfassung:
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.