Maximilian Heisinger, Florian Piminger, Martina Seidl
Technical Track
 | Haus der Universität, Schlösslistrasse 5, 3008 Bern, Switzerland |
 | 7 February 2024, 13:30 CET |
 | Maximilian Heisinger |
 | Leopoldo Teixeira |
 | https://dl.acm.org/doi/10.1145/3634713.3634718 |
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.