SAT benchmarks from Automotive Product Configuration

Introduction

The CNF files encode different consistency properties of the configuration data base which is used to configure DaimlerChrysler's Mercedes car lines [1,2]. The base CNF files encode the set of all possible constructible (and completely supplemented) orders for a certain model class, and thus are all satisfiable. Most of the consistency tests ask for the validity of a formula of the form B -> F, where B is one of the (large) base formulae describing a model line and F is the (small) property to be checked. For each B there are usually thousands of properties F to be checked.

The SAT files obtained from encoding consistency properties are separated into satisfiable and unsatisfiable instances. The files are indexed by the kind of consistency test performed and by a sequence number. The test may be one of:

• NC: necessary codes
• UC: inadmissible codes
• SZ: stability of the order completion process
• RZ: order independence of the completion process
• UT: superfluous parts
• MT: ambiguities in the parts list

Downloads

• base: CNF files encoding the product overview (all possible constructible car variants) of different Mercedes model classes (DC_base.zip).
• sat: Satisfiable instances of some consistency checks (DC_sat.zip).
• unsat: Unsatisfiable instances of some consistency checks (DC_unsat.zip).
• all: All of the above in one ZIP archive (DC_all.zip).

References