Search papers, labs, and topics across Lattice.
This paper presents a comparative analysis of five state-of-the-art backbone algorithms on 2,371 formulas derived from real-world configurable software systems, contrasting with prior evaluations focused on SAT competition formulas. The study reveals that variability model formulas exhibit distinct structural properties, specifically higher clause density but greater clause simplicity, compared to SAT competition formulas. The authors recommend Algorithm 2/3 for smaller formulas (<=1,000 variables) and Algorithm 5 with adaptive chunk size for larger formulas, while also noting the ineffectiveness of filtering heuristics for variability models.
Algorithms used in product line tools are only half as fast as the best alternative for finding backbones in configurable software systems, but picking the right algorithm requires predicting the optimal chunk size, which remains an open problem.
The backbone of a Boolean formula is the set of literals that must be true in every assignment that satisfies the formula. This concept is fundamental to key operations on variability models, including propagating user configuration decisions to identify implied feature selections, detecting dead features and dead code blocks, and preprocessing formulas to accelerate knowledge compilation into tractable representations such as binary decision diagrams. Despite its importance, previous empirical studies have evaluated backbone algorithms solely on SAT competition formulas (typically engineered to test the limits of SAT solvers), leading to inconsistent conclusions about their performance. This study provides the first comprehensive evaluation of formulas derived from real-world variability models, analyzing 21 configurations of 5 state-of-the-art algorithms on 2,371 formulas from configurable systems ranging from 100 variables and 179 clauses to 186,059 variables and 527,240 clauses. The results indicate that variability model formulas are structurally distinct, with higher clause density but greater clause simplicity. Our research provides clear algorithm selection guidelines: Algorithm 2/3 (iterative with solution filtering) is recommended for formulas with 1,000 or fewer variables, while Algorithm 5 (chunked core-based) with adaptive chunk size selection provides the best practical performance for larger formulas. Also, the results show that filtering heuristics have negligible or negative effects on performance for variability models. Finally, the study identifies a research gap: while Algorithm 5 with optimal chunk size can achieve runtime reductions exceeding 50\% compared to Algorithm 2/3 (the one that product line tools implement), the optimal chunk size varies unpredictably across formulas and cannot currently be estimated, opening directions for future research.
