Raw DIMACS Formulas Derived from Kconfig Models for Research on Highly Configurable Software

A Dataset of DIMACS Formulas Derived from Kconfig Models This repository contains 5,476 raw DIMACS-encoded Boolean formulas derived from Kconfig variability models of nine open-source systems. Each model is translated by two state-of-the-art tools, KconfigReader and KMax, yielding two DIMACS files per model (2,738 models x 2 translators = 5,476 files). All formulas are provided without any preprocessing (no backbone simplification, no atomic-set reduction, no unit propagation, etc.). This makes the dataset suitable for benchmarking preprocessing algorithms themselves, as well as for evaluating how raw formula complexity affects downstream reasoning tasks such as SAT solving, model counting, and configuration sampling. Systems System Description axTLS Embedded TLS library Buildroot Embedded Linux build system BusyBox Unix utilities for embedded systems EmbToolkit Embedded systems toolkit Freetz-NG Fritz!Box firmware modification L4Re L4 Runtime Environment microkernel Linux kernel 43 architectures (Alpha, Arc, ARM, ARM64, i386, x86_64, ...) Toybox Command-line utilities uClibc Embedded C library The dataset covers multiple tagged releases per system. Formulas range from 22 to 73,719 variables and from 18 to 7,406,667 clauses. Repository Structure . ├── dimacs/ # 5,476 DIMACS files │ ├── Axtls__1-0-0__KConfigReader.dimacs │ ├── Axtls__1-0-0__KMax.dimacs │ ├── ... │ └── LinuxX8664__6-5__KMax.dimacs ├── features_and_variable_ids/ # Per-pair feature–ID mapping CSVs (one per model version) │ ├── Axtls__1-0-0.csv │ ├── ... │ └── LinuxX8664__6-5.csv ├── summary.csv # Per-formula metrics ├── mapping_between_features_and_ids.py # Generates features_and_variable_ids/ ├── replication.sh # Bash script to regenerate the dataset └── README.md File Naming Convention Each DIMACS file follows the pattern: {System}__{Version}__{Translator}.dimacs System: system name, with architecture appended for Linux (e.g., LinuxArm64) Version: release tag with dots replaced by hyphens (e.g., 6-5 for version 6.5) Translator: KConfigReader or KMax Example: LinuxArm64__6-5__KMax.dimacs summary.csv A CSV file with one row per DIMACS file and the following columns: Column Description Name File name NumberOfVariables Number of Boolean variables NumberOfClauses Number of clauses NumberOfCoreFeatures Variables that must be true in every satisfying assignment NumberOfDeadFeatures Variables that must be false in every satisfying assignment MedianLiteralsPerClause Median number of literals per clause Inf95CovIntLitsPerClause Lower bound of the 95% coverage interval for literals per clause Sup95CovIntLitsPerClause Upper bound of the 95% coverage interval for literals per clause Version System version (with dots) ToolToGetTheFormula Translator used (KConfigReader or KMax) DIMACS Format Each file encodes a Boolean formula in Conjunctive Normal Form (CNF). The format is: Lines starting with c are comments mapping variable numbers to Kconfig option names. The line p cnf <variables> <clauses> declares the number of variables and clauses. Each subsequent line is a clause: a space-separated list of non-zero integers terminated by 0. Positive integers denote affirmed literals; negative integers denote negations. features_and_variable_ids/ Each DIMACS file assigns integer IDs to its variables independently: the same Kconfig feature (e.g., CONFIG_SSL_SERVER_ONLY) will typically have a different ID in the KconfigReader file and the KMax file for the same model version. The features_and_variable_ids/ directory contains one CSV file per model version that maps every shared feature name to its integer ID in each translator's DIMACS file: Column Description Feature Kconfig feature name (e.g., CONFIG_SSL_SERVER_ONLY) KConfigReaderId Variable ID assigned by KconfigReader KMaxId Variable ID assigned by KMax Only semantic feature variables are included. Tseitin auxiliary variables (k!N) are excluded because, although both tools emit variables with those names, they represent unrelated sub-formula nodes introduced by Z3's tseitin-cnf tactic and carry no shared semantics. These CSVs are generated by mapping_between_features_and_ids.py, which is called automatically at the end of replication.sh. To regenerate them independently: python3 mapping_between_features_and_ids.py Replication The replication.sh script regenerates all DIMACS files from scratch using torte. It requires Docker or Podman: bash replication.sh torte clones each system's source repository at every tagged version, runs KconfigReader and KMax inside containers, transforms the output to SMT-LIB 2 format with FeatJAR, and converts it to DIMACS using the Z3 solver. Authors Ruben Heradio, Cristina Cerrada, Ismael Abad, Ernesto Aranda-Escolastico, Juan Jose Escribano, David Fernandez-Amoros Universidad Nacional de Educacion a Distancia (UNED), Madrid, Spain Citation If you use this dataset in your research, please cite: @article{heradio26_dimacs_kconfig, title = {{A dataset of DIMACS formulas derived from Kconfig models for research on highly configurable software}}, journal = {Data in Brief}, volume = {66}, pages = {112747}, year = {2026}, doi = {https://doi.org/10.1016/j.dib.2026.112747}, author = {Ruben Heradio and Cristina Cerrada and Ismael Abad and Ernesto Aranda and Juan Jose Escribano and David Fernandez-Amoros}, keywords = {Software product line, Configurable system, Linux, SAT solver, Knowledge compilation}, abstract = {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.} } Acknowledgements We thank Elias Kuiter for his help and support in using torte. This work has been funded by FEDER/Spanish Ministry of Science, Innovation and Universities (MCIN)/Agencia Estatal de Investigacion (AEI) under project COSY (PID2022-142043NB-I00). License MIT License.