SAT-Based Consistency Checking of Automotive Electronic Product Data
Carsten Sinz, Wolfgang Küchlin · 2006
Abstract. Complex products such as motor vehicles or comput-ers need to be configured as part of the sales process [3, 8]. If the sale is electronic, then the configuration and some validity check-ing of the order must be done electronically as part of an electronic product data management system (EPDMS). The EPDMS typically maintains a data base of sales options and parts together with a set of logical constraints expressing valid combinations of sales options and their transformation into manufacturable products. Due to the complexity of these constraints, creation and maintenance of the con-figuration data base is a nontrivial task and error-prone. We present our system BIS which is commercially used to check global consis-tency assertions about the product data base used by the EPDMS of a major car and truck manufacturer. The EPDMS uses Boolean logic to encode the constraints, and BIS translates the consistency asser-tions into problems which it solves using a propositional satisfiability checker. We expect our approach to be especially suited for rapidly changing complex products as they increasingly appear in electronic commerce.