SAT benchmarks from Automotive Product Configuration

Introduction

This page contains SAT benchmarks obtained from the validation and verification of automotive product configuration data.

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:

All of the SAT instances reveal surprisingly short search times for state-of-the-art SAT checkers (e.g. PaSAT, chaff). The reason for this is not clearly understood so far.

Downloads


References

[1] 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)
[2] 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)

Carsten Sinz
Last modified: Sat Apr 5 15:14:05 MEST 2003