Raphaël Michel, Vijay Ganesh, Arnaud Hubaux and Patrick Heymans, An SMT-based approach to automated configuration,
10th International Workshop on Satisfiability Modulo Theories, (Affiliated with IJCAR 2012), Manchester, UK, June 30-July 1, 2012
Date: 30 juin 2012
Publication: Publications scientifiques ⊕
Ingénierie de systèmes IT complexes ⊕
A propos du projet: CALIPro ⊕
In this paper, we explore a novel application domain for SMT solvers : conﬁguration problems. Conﬁguration problems are everywhere and particularly in product lines, where different yet similar products (e.g., cars or customizable software) are built from a shared set of assets. Designing a product line requires enumerating the different product features and the constraints that determine their valid combinations. Various categories of constraint solvers exist, but SMT solvers appear to be a solution of choice for conﬁguration problems. This is mostly due to their high efﬁciency and expressiveness which have already proved useful in a variety of practical applications. In this paper, we recall what conﬁguration problems are, describe a language to represent them, and map from conﬁguration problems to the satisﬁability problem over SMT theories.