Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet? - Inria - Institut national de recherche en sciences et technologies du numérique Accéder directement au contenu
Communication Dans Un Congrès Année : 2019

Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet?

Résumé

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.
Fichier principal
Vignette du fichier
Uniform_Sampling_of_SAT_Solutions_for_Configurable_Systems__Are_We_There_Yet____footnotesize_textsuperscript__ (3).pdf (498.85 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01991857 , version 1 (24-01-2019)

Identifiants

Citer

Quentin Plazar, Mathieu Acher, Gilles Perrouin, Xavier Devroey, Maxime Cordy. Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet?. ICST 2019 - 12th IEEE International Conference on Software Testing, Verification, and Validation, Apr 2019, Xian, China. pp.240-251, ⟨10.1109/ICST.2019.00032⟩. ⟨hal-01991857⟩
379 Consultations
1009 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More