Uniform Sampling of SAT Solutions for Configurable Systems

Are We There Yet?

Conference paper (2019)

Authors

Quentin Plazar Inria, Université de Rennes
Mathieu Acher Inria, Université de Rennes
GILLES PERROUIN University of Namur
Xavier Devroey Software Engineering - EEMCS
Maxime Cordy University of Luxembourg
Research Group
Software Engineering (EEMCS) (TU Delft)
Copyright: © 2019 Quentin Plazar, Mathieu Acher, Gilles Perrouin, Xavier Devroey, Maxime Cordy
DOI
help_outline
https://doi.org/10.1109/ICST.2019.00032
SAT Configurable-systems Software-product-lines Software-testing Uniform-sampling Variability-modeling
More Info
expand_more

Published Date

2019

Language

English

Reuse Rights

Other than for strictly personal use, it is not permitted to download, forward or distribute the text or part of it, without the consent of the author(s) and/or copyright holder(s), unless the work is under an open content license such as Creative Commons.

Faculty

Electrical Engineering, Mathematics and Computer Science

Department

Software Technology

Research Group

Software Engineering

Abstract

Uniform or near-uniform generation of solutions for large satisfiability formulas is a problem of theoretical and practical interest for the testing community. Recent works proposed two algorithms (namely UniGen and QuickSampler) for reaching a good compromise between execution time and uniformity guarantees, with empirical evidence on SAT benchmarks. In the context of highly-configurable software systems (e.g., Linux), it is unclear whether UniGen and QuickSampler can scale and sample uniform software configurations. In this paper, we perform a thorough experiment on 128 real-world feature models. We find that UniGen is unable to produce SAT solutions out of such feature models. Furthermore, we show that QuickSampler does not generate uniform samples and that some features are either never part of the sample or too frequently present. Finally, using a case study, we characterize the impacts of these results on the ability to find bugs in a configurable system. Overall, our results suggest that we are not there: more research is needed to explore the cost-effectiveness of uniform sampling when testing large configurable systems.