An SMT-based approach to automated configuration

Abstract

We present a novel use of SMT solvers: configuration problems. Configuration problems are everywhere and particularly in product lines, where different yet similar products can be built from a common set of assets, which are then chosen, specialized and combined to form a product. Designing a product line boils down to enumerate the different parts of the products and the rules for combining them. These rules are often expressed as constraints. Various categories of constraint solvers exist, but SMT-solvers appear to be a solution of choice for configuration problem. In this paper, we present the configuration problem, we briefly introduce how we represent this type of problem and we map this representation to the input language of an STP solver able to support the various types of constraints found in configuration problems.