A dataset of DIMACS formulas derived from Kconfig models for research on highly configurable software

Translating Kconfig models into DIMACS-encoded Boolean formulas enables automated reasoning over configurable software systems. However, a complete translation encompassing the entire Kconfig language is still lacking. KconfigReader and KMax are two of the most widely adopted translators, yet no large-scale dataset has previously been available to systematically compare their outputs, evaluate the implications of their translations for reasoning tasks, or benchmark reasoning algorithms on extensive DIMACS files derived from Kconfig models. The dataset presented here consists of 5,476 DIMACS files, representing the KconfigReader and KMax encodings of 2,738 Kconfig models from nine open-source systems (axTLS, Buildroot, BusyBox, EmbToolkit, Freetz-NG, L4Re, the Linux kernel across 43 architectures, Toybox, and uClibc), covering multiple releases and a wide range of complexity. This dual-translation design supports three primary research tasks: (i) comparing KconfigReader and KMax to identify translation gaps; (ii) benchmarking complex reasoning operations, such as backbone solving, model counting, and configuration sampling across varying levels of complexity; and (iii) tracking the evolution of Kconfig across software releases.