An SMT-based approach to automated configuration

An SMT-based approach to automated configuration

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 des systèmes IT complexes 

A propos du projet: CALiPro 

Auteur : Raphaël Michel

In this paper, we explore a novel application domain for SMT solvers : configuration problems. Configuration 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 configuration problems. This is mostly due to their high efficiency and expressiveness which have already proved useful in a variety of practical applications. In this paper, we recall what configuration problems are, describe a language to represent them, and map from configuration problems to the satisfiability problem over SMT theories.