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:
|||Carsten Sinz, Andreas Kaiser, and Wolfgang Küchlin. Formal methods for the validation of automotive product configuration data. Artificial Intelligence for Engineering Design, Analysis and Manufacturing, 17(2), April 2003. Special issue on configuration. To appear. (pdf)|
|||Wolfgang Küchlin and Carsten Sinz. Proving consistency assertions for automotive product data management. J. Automated Reasoning, 24(1-2):145-163, February 2000. (pdf)|