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.