[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ skip to main content
research-article

Evaluating state-of-the-art # SAT solvers on industrial configuration spaces

Published: 13 January 2023 Publication History

Abstract

Product lines are widely used to manage families of products that share a common base of features. Typically, not every combination (configuration) of features is valid. Feature models are a de facto standard to specify valid configurations and allow standardized analyses on the variability of the underlying system. A large variety of such analyses depends on computing the number of valid configurations. To analyze feature models, they are typically translated to propositional logic. This allows to employ # SAT solvers that compute the number of satisfying assignments of the propositional formula translated from a feature model. However, the # SAT problem is generally assumed to be even harder than SAT and its scalability when applied to feature models has only been explored sparsely. Our main contribution is an investigation of the performance of off-the-shelf # SAT solvers on computing the number of valid configurations for industrial feature models. We empirically evaluate 21 publicly available # SAT solvers on 130 feature models from 15 subject systems. Our results indicate that current solvers master a majority of the evaluated systems (13/15) with the fastest solvers requiring less than one second for each successfully evaluated feature model. However, there are two complex systems for which none of the evaluated solvers scales. For the given experiment design, the solvers that consumed the least runtime are sharpSAT (2.5 seconds in sum for the 13 systems) and Ganak (3.5 seconds).

References

[1]
Acher M, Collet P, Lahire P, and France RB Familiar: a domain-specific language for large scale management of feature models Sci Comput Program (SCP) 2013 78 6 657-681
[2]
Ananieva S, Kowal M, Thüm T, Schaefer I (2016) Implicit constraints in partial feature models. In: Proc. int’l workshop on feature-oriented software development (FOSD), ACM, pp 18–27
[3]
Ansótegui C, Bonet ML, Levy J (2009) On the structure of industrial SAT instances. In: Proc. int’l conf.on principles and practice of constraint programming (CP), Springer, pp 127–141
[4]
Apel S, Batory D, Kästner C, Saake G (2013) Feature-Oriented Software Product Lines. Springer
[5]
Artusi R, Verderio P, and Marubini E Bravais-Pearson and spearman correlation coefficients: meaning, test of hypothesis and confidence interval Int J Biol Markers (IJBM) 2002 17 2 148-151
[6]
Bagheri E and Gasevic D Assessing the maintainability of software product line feature models using structural metrics Softw Qual J (SQJ) 2011 19 3 579-612
[7]
Bagheri E, Noia TD, Gasevic D, and Ragone A Formalizing interactive staged feature model configuration J Softw Evol Process 2012 24 4 375-400
[8]
Baranov E, Legay A, Meel KS (2020) Baital: an adaptive weighted sampling approach for improved t-wise coverage. In: Proc. Europ. Software engineering conf./foundations of software engineering (ESEC/FSE), ACM, pp 1114–1126
[9]
Batory D (2005) Feature models, grammars, and propositional formulas. In: Proc. int’l systems and software product line conf. (SPLC), Springer, pp 7–20
[10]
Bayardo Jr RJ, Pehoushek JD (2000) Counting models using connected components. In: Proc. Conf. on artificial intelligence (AAAI), AAAI press, pp 157–162
[11]
Benavides D, Segura S, and Ruiz-Cortés A Automated analysis of feature models 20 years later a literature review Inf Syst 2010 35 6 615-708
[12]
Benavides D, Segura S, Trinidad P, Ruiz-Cortés A (2006) Using java CSP solvers in the automated analyses of feature models. In: Proc. generative and transformational techniques in software engineering, Springer, pp 399–408
[13]
Benavides D, Segura S, Trinidad P, Ruiz-Cortés A (2007) FAMA: Tooling a framework for the automated analysis of feature models. In: Proc. int’l workshop on variability modelling of software-intensive systems (VaMoS), lero, pp 129–134. Technical report 2007-01
[14]
Benavides D, Trinidad P, Ruiz-Cortés A (2005) Using constraint programming to reason on feature models. In: Proc. Int’l conf. on software engineering and knowledge engineering (SEKE), pp 677–682
[15]
Bezerra CIM, Andrade RMC, Monteiro JMS (2014) Measures for quality evaluation of feature models. In: Proc. Int’l conf. on software reuse (ICSR), Springer, pp 282–297
[16]
Biere A PicoSAT Essentials J. Satisfiability Boolean Model Comput 2008 4 75-97
[17]
Biere A, Heule M, van Maaren H, Walsh T (2009) Handbook of satisfiability: volume 185 frontiers in artificial intelligence and applications. IOS press
[18]
Bosch J, Florijn G, Greefhorst D, Kuusela J, Obbink JH, Pohl K (2001) Variability issues in software product lines. In: Proc. int’l workshop on software product-family engineering (PFE), Springer, pp 13–21
[19]
Bryant RE Graph-Based Algorithms for boolean function manipulation IEEE Trans Comput 1986 C-35 8 677-691
[20]
Bryant RE (2018) Binary decision diagrams. In: Handbook of model checking, Springer, pp 191–217
[21]
Burchard J, Schubert T, Becker B (2015) Laissez-Faire caching for parallel# SAT solving. In: Proc. Int’l conf. on theory and applications of satisfiability testing (SAT), Springer, pp 46–61
[22]
Chakraborty S, Meel KS, Vardi MY (2013) A scalable approximate model counter. In: Schulte C (ed) Proc. Int’l Conf. on Principles and Practice of Constraint Programming (CP), Springer, pp 200–216
[23]
Chen S, Erwig M (2011) Optimizing the product derivation process. In: Proc. Int’l systems and software product line conf. (SPLC), IEEE, pp 35–44
[24]
Conover WJ and Iman RL Rank transformations as a bridge between parametric and nonparametric statistics Am Stat 1981 35 3 124-129
[25]
Czarnecki K, Wȧsowski A (2007) Feature diagrams and logics: There and back again. In: Proc. Int’l systems and software product line conf. (SPLC), IEEE, pp 23–34
[26]
Darwiche A On the tractable counting of theory models and its application to truth maintenance and belief revision J Appl Non-Class Logics 2001 11 1-2 11-34
[27]
Darwiche A (2002) A compiler for deterministic, decomposable negation normal form. In: Proc. Conf. on artificial intelligence (AAAI), AAAI press, pp 627–634
[28]
Darwiche A (2004) New advances in compiling CNF to decomposable negation normal form. In: Proc. Europ. Conf. on artificial intelligence, IOS press, pp 318–322
[29]
Darwiche A (2011) SDD: a new canonical representation of propositional knowledge bases. AAAI Press, pp 819–826
[30]
Darwiche A and Marquis P A knowledge compilation map J Artif Intell Res (JAIR) 2002 17 1 229-264
[31]
Fernández-Amorós D, Heradio R, Cerrada JA, and Cerrada C A scalable approach to exact model and commonality counting for extended feature models IEEE Trans Softw Eng (TSE) 2014 40 9 895-910
[32]
Fichte JK, Hecher M, and Hamiti F The model counting competition 2020 ACM J Exp Algorithmics (JEA) 2021 26 1-26, 13:1–26
[33]
Fichte JK, Hecher M, Zisser M (2019) An Improved GPU-based SAT Model Counter. In: Proc. Int’l conf. on principles and practice of constraint programming (CP), Springer, pp 491–509
[34]
Fritsch C, Abt R, Renz B (2020) The benefits of a feature model in banking. In: Proc. Int’l systems and software product line conf. (SPLC). ACM
[35]
Galindo JA, Acher M, Tirado JM, Vidal C, Baudry B, Benavides D (2016) Exploiting the enumeration of all feature model configurations a new perspective with distributed computing. In: Proc. Int’l systems and software product line conf. (SPLC), ACM, pp 74–78
[36]
Gomes CP, Sabharwal A, Selman B (2006) Model counting: a new strategy for obtaining good bounds. In: Proc. Conf. on artificial intelligence (AAAI), AAAI press, pp 54–61
[37]
Hadzic T, Subbarayan S, Jensen RM, Andersen HR, Møller J, Hulgaard H (2004) Fast backtrack-free product configuration using a precompiled solution space representation. In: Proc. Int’l conf. on economic, technical and organisational aspects of product configuration systems, Gamez publishing, pp 131–138
[38]
Heradio R, Fernández-Amorós D, Cerrada JA, and Abad I A literature review on feature diagram product counting and its usage in software product line economic models Int J Softw Eng Knowl Eng (IJSEKE) 2013 23 08 1177-1204
[39]
Heradio R, Fernández-Amorós D, Mayr-Dorn C, Egyed A (2019) Supporting the statistical analysis of variability models. In: Proc. Int’l conf. on software engineering (ICSE), IEEE, pp 843–853
[40]
Heradio R, Pérez-Morago HJ, Fernández-Amorós D, Bean R, Cabrerizo FJ, Cerrada C, Herrera-Viedma E (2016) Binary decision diagram algorithms to perform hard analysis operations on variability models. In: Proc. Int’l Conf. on Intelligent Software Methodologies, Tools and Techniques (SOMET), IOS Press, pp 139–154
[41]
Heradio-Gil R, Fernández-Amorós D, Cerrada JA, and Cerrada C Supporting commonality-based analysis of software product lines IET Softw 2011 5 6 496-509
[42]
Heß T, Sundermann C, Thüm T (2021) On the scalability of building binary decision diagrams for current feature models. In: Proc. Int’l systems and software product line conf. (SPLC), ACM, pp 131–135
[43]
Huang J, Darwiche A (2005) DPLL with a trace: from SAT to knowledge compilation. In: Proc. Int’l joint conf. on artificial intelligence (IJCAI), vol 5. Professional book center, pp 156–162
[44]
Huth M, Ryan M (2004) Logic in computer science: modelling and reasoning about systems. Cambridge University Press
[45]
Israeli A and Feitelson DG The linux kernel as a case study in software evolution J. Syst Softw (JSS) 2010 83 3 485-501
[46]
Kästner C, Apel S, Batory D (2007) A case study implementing features using aspectJ. In: Proc. Int’l systems and software product line conf. (SPLC), IEEE, pp 223–232
[47]
Kästner C, Thüm T, Saake G, Feigenspan J, Leich T, Wielgorz F (2009) FeatureIDE: a tool framework for feature-oriented software development. In: Proc. Int’l Conf. on Software Engineering (ICSE), IEEE, pp 611–614. Formal demonstration paper
[48]
Klebanov V, Manthey N, Muise C (2013) SAT-based analysis and quantification of information flow in programs. In: Proc. Int’l conf. on quantitative evaluation of systems (QEST), Springer, pp 177–192
[49]
Knüppel A, Thüm T, Mennicke S, Meinicke J, Schaefer I (2017) Is there a mismatch between Real-World feature models and Product-Line research?. In: Proc. Europ. software engineering conf. Foundations of software engineering (ESEC/FSE), ACM, pp 291–302
[50]
Koriche F, Lagniez J-M, Marquis P, Thomas S (2013) Knowledge compilation for model counting affine decision trees. In: Proc. Int’l joint conf. on artificial intelligence (IJCAI), AAAI press
[51]
Kowal M, Ananieva S, Thüm T (2016) Explaining anomalies in feature models. In: Proc. Int’l conf. on generative programming: concepts & experiences (GPCE), ACM, pp 132–143
[52]
Krieter S, Pinnecke M, Krüger J, Sprey J, Sontag C, Thüm T, Leich T, Saake G (2017) Feature IDE empowering third-party developers. In: Proc. Int’l systems and software product line conf. (SPLC), ACM, pp 42–45
[53]
Krieter S, Thüm T, Schulze S, Schröter R, Saake G (2018) Propagating configuration decisions with modal implication graphs. In: Proc. Int’l conf. on software engineering (ICSE), ACM, pp 898–909
[54]
Kübler A, Zengler C, Küchlin W (2010) Model counting in product configuration. In: Proc. Int’l workshop on logics for component configuration (lococo), Open publishing association, pp 44–53
[55]
Lagniez J-M, Marquis P (2017) An improved decision-DNNF compiler. In: Proc. Int’l joint conf. on artificial intelligence (IJCAI), pages 667–673. International joint conferences on artificial intelligence
[56]
Lagniez J-M, Marquis P, Szczepanski N (2018) DMC: a distributed model counter. In: Proc. Int’l joint conf. on artificial intelligence (IJCAI), pp 1331–1338. International joint conferences on artificial intelligence
[57]
Le Berre D and Parrain A The sat4j library, release 2.2 J Satisfiability Boolean Model Comput 2010 7 2-3 59-64
[58]
McKnight PE, Najab J (2010) Mann-Whitney U test. Corsini Encycl Psychol 1–1
[59]
Mendonca M and Cowan D Decision-making coordination and efficient reasoning techniques for Feature-Based configuration Sci Comput Program (SCP) 2010 75 5 311-332
[60]
Mendonça M Efficient reasoning techniques for large scale feature models 2009 PhD thesis University of Waterloo
[61]
Mendonça M, Branco M, Cowan D (2009) S.P.L.O.T.: software product lines online tools. In: Proc. Conf. on object-oriented programming, systems, languages and applications (OOPSLA), ACM, pp 761–762
[62]
Mendonça M, Wȧsowski A, Czarnecki K (2009) SAT-Based analysis of feature models is easy. In: Proc. Int’l systems and software product line conf. (SPLC), Software engineering institute, pp 231–240
[63]
Muise C, McIlraith S, Beck JC, Hsu E (2010) Fast d-DNNF Compilation with sharpSAT. In: Proc. Conf. on artificial intelligence (AAAI). AAAI press
[64]
Munoz D-J, Oh J, Pinto M, Fuentes L, Batory D (2019) Uniform random sampling product configurations of feature models that have numerical features. In: Proc. Int’l systems and software product line conf. (SPLC), ACM, pp 289–301
[65]
Nieke M, Mauro J, Seidl C, Thüm T, Yu IC, Franzke F (2018) Anomaly analyses for Feature-Model evolution. In: Proc. Int’l conf. on generative programming: Concepts & experiences (GPCE), ACM, pp 188–201
[66]
Oh J, Batory D, Myers M, Siegmund N (2016) Sampling: finding product line configurations with high performance by random technical report University of Texas at Austin
[67]
Oh J, Batory D, Myers M, Siegmund N (2017) Finding Near-Optimal configurations in product lines by random sampling. In: Proc. Int’l symposium on foundations of software engineering (FSE), pp 61–71
[68]
Oh J, Gazzillo P, Batory D, Heule M, Myers M (2019) Uniform Sampling from Kconfig Feature Models. Technical Report TR-19-02, The university of texas at austin department of computer science
[69]
Oztok U, Darwiche A (2014) On compiling CNF into decision-DNNF. In: Proc. Int’l conf. on principles and practice of constraint programming (CP), Springer, pp 42–57
[70]
Oztok U, Darwiche A (2015) A Top-Down compiler for sentential decision diagrams. In: Proc. Int’l joint conf. on artificial intelligence (IJCAI), AAAI press, pp 3141–3148
[71]
Pérez Morago HJ BDD Algorithms to perform hard analysis operations on variability models 2016 PhD thesis Universidad Nacional de Educación a Distancia
[72]
Perrouin G, Sen S, Klein J, Baudry B, Le Traon Y (2010) Automated and scalable T-Wise test case generation strategies for software product lines. In: Proc. Int’l conf. on software testing, verification and validation (ICST), IEEE, pp 459–468
[73]
Pett T, Krieter S, Runge T, Thüm T, Lochau M, Schaefer I (2021) Stability of Product-Line sampling in continuous integration. In: Proc. Int’l working conf. on variability modelling of software-intensive systems (VaMoS). ACM
[74]
Pett T, Thüm T, Runge T, Krieter S, Lochau M, Schaefer I (2019) Product sampling for product lines the scalability challenge. In: Proc. Int’l systems and software product line conf. (SPLC), ACM, pp 78–83
[75]
Plazar Q, Acher M, Perrouin G, Devroey X, Cordy M (2019) Uniform sampling of SAT solutions for configurable systems are we there yet?. In: Proc. Int’l conf. on software testing, verification and validation (ICST), IEEE, pp 240–251
[76]
Pohl R, Lauenroth K, Pohl K (2011) A performance comparison of contemporary algorithmic approaches for automated analysis operations on feature models. In: Proc. Int’l conf. on automated software engineering (ASE), IEEE, pp 313–322
[77]
Rudell R (1993) Dynamic variable ordering for ordered binary decision diagrams. In: Proc. Int’l conf. on computer-aided design (ICCAD), IEEE, pp 42–47
[78]
Sang T, Bacchus F, Beame P, Kautz HA, Pitassi T (2004) Combining component caching and clause learning for effective model counting. In: Proc. Int’l conf. on theory and applications of satisfiability testing (SAT), Springer, pp 20–28
[79]
Sang T, Beame P, Kautz H (2005) Heuristics for fast exact model counting. In: Proc. Int’l conf. on theory and applications of satisfiability testing (SAT), Springer, pp 226–240
[80]
Schröter R, Krieter S, Thüm T, Benduhn F, Saake G (2016) Feature-model interfaces: the highway to compositional analyses of Highly-Configurable systems. In: Proc. Int’l conf. on software engineering (ICSE), ACM, pp 667–678
[81]
Segura S (2008) Automated analysis of feature models using atomic sets. In: Proc. Int’l systems and software product line conf. (SPLC), vol 2. IEEE, pp 201–207
[82]
Sharma S, Gupta R, Roy S, Meel KS (2018) Knowledge compilation meets uniform sampling. In: Proc. Int’l conf. on logic for programming, artificial intelligence, and reasoning, Easy chair, pp 620–636
[83]
Sharma S, Roy S, Soos M, Meel KS (2019) GANAK: a scalable probabilistic exact model counter. In: Proc. Int’l joint conf. on artificial intelligence (IJCAI), vol 19. AAAI press, pp 1169–1176
[84]
Sobernig S, Apel S, Kolesnikov S, and Siegmund N Quantifying structural attributes of system decompositions in 28 Feature-Oriented software product lines Empir Softw Eng (EMSE) 2016 21 4 1670-1705
[85]
Sprey J, Sundermann C, Krieter S, Nieke M, Mauro J, Thüm T, Schaefer I (2020) SMT-based variability analyses in featureIDE. In: Proc. Int’l working conf. on variability modelling of software-intensive systems (VaMoS). ACM
[86]
Sullivan GM and Feinn R Using effect size—or why the P value is not enough J Grad Med Educ 2012 4 3 279-282
[87]
Sundermann C, Nieke M, Bittner PM, Heß T, Thüm T, Schaefer I (2021) Applications of #SAT solvers on feature models. In: Proc. Int’l working conf. on variability modelling of software-intensive systems (VaMoS). ACM
[88]
Sundermann C, Thüm T, Schaefer I (2020) Evaluating #SAT solvers on industrial feature models. In: Proc. Int’l working conf. on variability modelling of software-intensive systems (VaMoS). ACM
[89]
Svahnberg M and Bosch J Evolution in software product lines two cases J Softw Maint (JSM) 1999 11 6 391-422
[90]
Thüm T, Kästner C, Erdweg S, Siegmund N (2011) Abstract features in feature modeling. In: Proc. Int’l systems and software product line conf. (SPLC), IEEE, pp 191–200
[91]
Thurley M (2006) SharpSAT - counting models with advanced component caching and implicit BCP. In: Proc. Int’l conf. on theory and applications of satisfiability testing (SAT), Springer pp 424–429
[92]
Toda T and Soh T Implementing efficient all solutions SAT solvers ACM J Exp Algorithmics (JEA) 2016 21 1 1.12:1-1.12:44
[93]
Valiant LG The complexity of computing the permanent Theor Comput Sci 1979 8 2 189-201
[94]
Wei W, Selman B (2005) A new approach to model counting. In: Proc. Int’l conf. on theory and applications of satisfiability testing (SAT), Springer, pp 324–339
[95]
Xu L, Hutter F, Hoos HH, and Leyton-Brown K SATzilla: portfolio-based algorithm selection for SAT J Artif Intell Res (JAIR) 2008 32 565-606
[96]
Zar JH Significance testing of the spearman rank correlation coefficient J Am Stat Assoc 1972 67 339 578-580

Cited By

View all
  • (2024)On the Expressive Power of Languages for Static VariabilityProceedings of the ACM on Programming Languages10.1145/36897478:OOPSLA2(1018-1050)Online publication date: 8-Oct-2024
  • (2024)Variability-Aware Differencing with DiffDetectiveCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663813(632-636)Online publication date: 10-Jul-2024
  • (2024)On the Use of Multi-valued Decision Diagrams to Count Valid Configurations of Feature ModelsProceedings of the 28th ACM International Systems and Software Product Line Conference10.1145/3646548.3672594(96-106)Online publication date: 2-Sep-2024
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Empirical Software Engineering
Empirical Software Engineering  Volume 28, Issue 2
Mar 2023
1389 pages

Publisher

Kluwer Academic Publishers

United States

Publication History

Published: 13 January 2023
Accepted: 25 November 2022

Author Tags

  1. Configurable systems
  2. Feature models
  3. Product lines
  4. Model counting
  5. Configuration counting
  6. #SAT
  7. Benchmark

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)0
  • Downloads (Last 6 weeks)0
Reflects downloads up to 02 Mar 2025

Other Metrics

Citations

Cited By

View all
  • (2024)On the Expressive Power of Languages for Static VariabilityProceedings of the ACM on Programming Languages10.1145/36897478:OOPSLA2(1018-1050)Online publication date: 8-Oct-2024
  • (2024)Variability-Aware Differencing with DiffDetectiveCompanion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering10.1145/3663529.3663813(632-636)Online publication date: 10-Jul-2024
  • (2024)On the Use of Multi-valued Decision Diagrams to Count Valid Configurations of Feature ModelsProceedings of the 28th ACM International Systems and Software Product Line Conference10.1145/3646548.3672594(96-106)Online publication date: 2-Sep-2024
  • (2024)UnWise: High T-Wise Coverage from Uniform SamplingProceedings of the 18th International Working Conference on Variability Modelling of Software-Intensive Systems10.1145/3634713.3634716(37-45)Online publication date: 7-Feb-2024
  • (2023)Elimination of constraints for parallel analysis of feature modelsProceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A10.1145/3579027.3608981(99-110)Online publication date: 28-Aug-2023
  • (2023)Quantum Computing for Feature Model AnalysisProceedings of the 27th ACM International Systems and Software Product Line Conference - Volume A10.1145/3579027.3608971(1-7)Online publication date: 28-Aug-2023
  • (2023)On the benefits of knowledge compilation for feature-model analysesAnnals of Mathematics and Artificial Intelligence10.1007/s10472-023-09906-692:5(1013-1050)Online publication date: 6-Nov-2023

View Options

View options

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media