An SMT-based approach to automated configuration

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.