Interactive product configurator based on satisfiability modulo theories solver

Abstract

The process of product configuration is about finding a specific product consisting of components, predefined in advance. The set of all available components, their properties, and interconnection constraints define the domain of product family. The number of specific products (or product variants) directly depends on the number of members and constraints in the domain. The manual management of documentation for product family is a complex, error prone and time consuming process. So the product configurator is a software tool, assisting the user in selection of product, satisfying his requirements. This article shows how information of product domain could be expressed as first order logical formulas with linear integer and real arithmetic. The methodology and interactive feedback algorithm is provided utilizing the satisfiability modulo theories solver for interactive evaluation of product configuration.