一句话：通过历史特征模型与历史 SAT 求解器的实证分析，发现 SAT 求解器整体跟不上 Linux 内核特征模型的增长。
Linux 内核高度可配置，其可配置性由特征模型定义，记录特性及依赖关系，许多产品线分析在底层依赖 SAT 求解器。然而内核复杂度持续增长，可能妨碍高效分析，而 SAT 求解器性能也在长期改进。本文实证研究 SAT 求解器能否跟上 Linux 内核特征模型的发展。作者使用 Linux 的历史特征模型和来自多个来源的历史 SAT 求解器进行跨时间分析。结果显示，SAT 求解器总体上无法跟上 Linux 的增长；即使最优 SAT 求解器也以每年约 10% 的速度变慢，意味着性能约每七年减半。作者据此认为，若不抑制内核增长，其分析将越来越困难。
The Linux kernel is a highly relevant, yet also highly configurable software system. Kernel developers keep track of this configurability in a feature model, which defines the features of Linux and their dependencies. To support kernel developers in various activities, many (semi-)automated product-line analyses have been proposed over the years. Under the hood, these analyses can often be computed with SAT solvers. Yet, the Linux kernel has constantly been growing in complexity for decades, which increasingly hampers its efficient analysis. At the same time, SAT solvers have been improving in performance for decades, which eases analysis. In this paper, we investigate empirically whether SAT solvers can keep up with the Linux kernel’s feature model. To this end, we analyze historic feature models of Linux with historic SAT solvers from several sources. We find that SAT solvers are generally not able to keep up with Linux. Even the optimal SAT solver is slowing down by 10% every year, meaning that its performance halves every seven years. We conclude that the Linux kernel will become increasingly difficult to analyze if its growth is not counteracted.
@inproceedings{paperbot11627,
title = {Can SAT Solvers Keep Up With the Linux Kernel's Feature Model?},
author = {Elias Kuiter and Urs-Benedict Braun and Thomas Thüm and Sebastian Krieter and Gunter Saake},
booktitle = {ICSE},
year = {2026},
doi = {10.1145/3744916.3787823}
}