{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,27]],"date-time":"2026-06-27T12:04:39Z","timestamp":1782561879177,"version":"3.54.5"},"reference-count":96,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2023,1,13]],"date-time":"2023-01-13T00:00:00Z","timestamp":1673568000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,1,13]],"date-time":"2023-01-13T00:00:00Z","timestamp":1673568000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["TH 2387\/1-1"],"award-info":[{"award-number":["TH 2387\/1-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100008977","name":"Universit\u00e4t Ulm","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100008977","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Empir Software Eng"],"published-print":{"date-parts":[[2023,3]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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 (2.5 seconds in sum for the 13 systems) and (3.5 seconds).<\/jats:p>","DOI":"10.1007\/s10664-022-10265-9","type":"journal-article","created":{"date-parts":[[2023,1,13]],"date-time":"2023-01-13T12:05:00Z","timestamp":1673611500000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":23,"title":["Evaluating state-of-the-art # SAT solvers on industrial configuration spaces"],"prefix":"10.1007","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5239-3307","authenticated-orcid":false,"given":"Chico","family":"Sundermann","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Tobias","family":"He\u00df","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Nieke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Paul Maximilian","family":"Bittner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jeffrey M.","family":"Young","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Thomas","family":"Th\u00fcm","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ina","family":"Schaefer","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2023,1,13]]},"reference":[{"issue":"6","key":"10265_CR1","doi-asserted-by":"publisher","first-page":"657","DOI":"10.1016\/j.scico.2012.12.004","volume":"78","author":"M Acher","year":"2013","unstructured":"Acher M, Collet P, Lahire P, France RB (2013) Familiar: a domain-specific language for large scale management of feature models. Sci Comput Program (SCP) 78(6):657\u2013681","journal-title":"Sci Comput Program (SCP)"},{"key":"10265_CR2","doi-asserted-by":"crossref","unstructured":"Ananieva S, Kowal M, Th\u00fcm T, Schaefer I (2016) Implicit constraints in partial feature models. In: Proc. int\u2019l workshop on feature-oriented software development (FOSD), ACM, pp 18\u201327","DOI":"10.1145\/3001867.3001870"},{"key":"10265_CR3","doi-asserted-by":"crossref","unstructured":"Ans\u00f3tegui C, Bonet ML, Levy J (2009) On the structure of industrial SAT instances. In: Proc. int\u2019l conf.on principles and practice of constraint programming (CP), Springer, pp 127\u2013141","DOI":"10.1007\/978-3-642-04244-7_13"},{"key":"10265_CR4","doi-asserted-by":"crossref","unstructured":"Apel S, Batory D, K\u00e4stner C, Saake G (2013) Feature-Oriented Software Product Lines. Springer","DOI":"10.1007\/978-3-642-37521-7"},{"issue":"2","key":"10265_CR5","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1177\/172460080201700213","volume":"17","author":"R Artusi","year":"2002","unstructured":"Artusi R, Verderio P, Marubini E (2002) Bravais-Pearson and spearman correlation coefficients: meaning, test of hypothesis and confidence interval. Int J Biol Markers (IJBM) 17(2):148\u2013151","journal-title":"Int J Biol Markers (IJBM)"},{"issue":"3","key":"10265_CR6","doi-asserted-by":"publisher","first-page":"579","DOI":"10.1007\/s11219-010-9127-2","volume":"19","author":"E Bagheri","year":"2011","unstructured":"Bagheri E, Gasevic D (2011) Assessing the maintainability of software product line feature models using structural metrics. Softw Qual J (SQJ) 19(3):579\u2013612","journal-title":"Softw Qual J (SQJ)"},{"issue":"4","key":"10265_CR7","doi-asserted-by":"publisher","first-page":"375","DOI":"10.1002\/smr.534","volume":"24","author":"E Bagheri","year":"2012","unstructured":"Bagheri E, Noia TD, Gasevic D, Ragone A (2012) Formalizing interactive staged feature model configuration. J Softw Evol Process 24(4):375\u2013400","journal-title":"J Softw Evol Process"},{"key":"10265_CR8","doi-asserted-by":"crossref","unstructured":"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\u20131126","DOI":"10.1145\/3368089.3409744"},{"key":"10265_CR9","doi-asserted-by":"crossref","unstructured":"Batory D (2005) Feature models, grammars, and propositional formulas. In: Proc. int\u2019l systems and software product line conf. (SPLC), Springer, pp 7\u201320","DOI":"10.1007\/11554844_3"},{"key":"10265_CR10","unstructured":"Bayardo Jr RJ, Pehoushek JD (2000) Counting models using connected components. In: Proc. Conf. on artificial intelligence (AAAI), AAAI press, pp 157\u2013162"},{"issue":"6","key":"10265_CR11","doi-asserted-by":"publisher","first-page":"615","DOI":"10.1016\/j.is.2010.01.001","volume":"35","author":"D Benavides","year":"2010","unstructured":"Benavides D, Segura S, Ruiz-Cort\u00e9s A (2010) Automated analysis of feature models 20 years later a literature review. Inf Syst 35(6):615\u2013708","journal-title":"Inf Syst"},{"key":"10265_CR12","doi-asserted-by":"crossref","unstructured":"Benavides D, Segura S, Trinidad P, Ruiz-Cort\u00e9s 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\u2013408","DOI":"10.1007\/11877028_16"},{"key":"10265_CR13","unstructured":"Benavides D, Segura S, Trinidad P, Ruiz-Cort\u00e9s A (2007) FAMA: Tooling a framework for the automated analysis of feature models. In: Proc. int\u2019l workshop on variability modelling of software-intensive systems (VaMoS), lero, pp 129\u2013134. Technical report 2007-01"},{"key":"10265_CR14","unstructured":"Benavides D, Trinidad P, Ruiz-Cort\u00e9s A (2005) Using constraint programming to reason on feature models. In: Proc. Int\u2019l conf. on software engineering and knowledge engineering (SEKE), pp 677\u2013682"},{"key":"10265_CR15","doi-asserted-by":"crossref","unstructured":"Bezerra CIM, Andrade RMC, Monteiro JMS (2014) Measures for quality evaluation of feature models. In: Proc. Int\u2019l conf. on software reuse (ICSR), Springer, pp 282\u2013297","DOI":"10.1007\/978-3-319-14130-5_20"},{"key":"10265_CR16","doi-asserted-by":"publisher","first-page":"75","DOI":"10.3233\/SAT190039","volume":"4","author":"A Biere","year":"2008","unstructured":"Biere A (2008) PicoSAT Essentials. J. Satisfiability Boolean Model Comput 4:75\u201397","journal-title":"J. Satisfiability Boolean Model Comput"},{"key":"10265_CR17","unstructured":"Biere A, Heule M, van Maaren H, Walsh T (2009) Handbook of satisfiability: volume 185 frontiers in artificial intelligence and applications. IOS press"},{"key":"10265_CR18","doi-asserted-by":"crossref","unstructured":"Bosch J, Florijn G, Greefhorst D, Kuusela J, Obbink JH, Pohl K (2001) Variability issues in software product lines. In: Proc. int\u2019l workshop on software product-family engineering (PFE), Springer, pp 13\u201321","DOI":"10.1007\/3-540-47833-7_3"},{"issue":"8","key":"10265_CR19","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE (1986) Graph-Based Algorithms for boolean function manipulation. IEEE Trans Comput C-35(8):677\u2013691","journal-title":"IEEE Trans Comput"},{"key":"10265_CR20","doi-asserted-by":"crossref","unstructured":"Bryant RE (2018) Binary decision diagrams. In: Handbook of model checking, Springer, pp 191\u2013217","DOI":"10.1007\/978-3-319-10575-8_7"},{"key":"10265_CR21","doi-asserted-by":"crossref","unstructured":"Burchard J, Schubert T, Becker B (2015) Laissez-Faire caching for parallel# SAT solving. In: Proc. Int\u2019l conf. on theory and applications of satisfiability testing (SAT), Springer, pp 46\u201361","DOI":"10.1007\/978-3-319-24318-4_5"},{"key":"10265_CR22","doi-asserted-by":"crossref","unstructured":"Chakraborty S, Meel KS, Vardi MY (2013) A scalable approximate model counter. In: Schulte C (ed) Proc. Int\u2019l Conf. on Principles and Practice of Constraint Programming (CP), Springer, pp 200\u2013216","DOI":"10.1007\/978-3-642-40627-0_18"},{"key":"10265_CR23","doi-asserted-by":"crossref","unstructured":"Chen S, Erwig M (2011) Optimizing the product derivation process. In: Proc. Int\u2019l systems and software product line conf. (SPLC), IEEE, pp 35\u201344","DOI":"10.1109\/SPLC.2011.47"},{"issue":"3","key":"10265_CR24","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1080\/00031305.1981.10479327","volume":"35","author":"WJ Conover","year":"1981","unstructured":"Conover WJ, Iman RL (1981) Rank transformations as a bridge between parametric and nonparametric statistics. Am Stat 35(3):124\u2013129","journal-title":"Am Stat"},{"key":"10265_CR25","doi-asserted-by":"crossref","unstructured":"Czarnecki K, Wa\u0307sowski A (2007) Feature diagrams and logics: There and back again. In: Proc. Int\u2019l systems and software product line conf. (SPLC), IEEE, pp 23\u201334","DOI":"10.1109\/SPLINE.2007.24"},{"issue":"1-2","key":"10265_CR26","doi-asserted-by":"publisher","first-page":"11","DOI":"10.3166\/jancl.11.11-34","volume":"11","author":"A Darwiche","year":"2001","unstructured":"Darwiche A (2001) On the tractable counting of theory models and its application to truth maintenance and belief revision. J Appl Non-Class Logics 11 (1-2):11\u201334","journal-title":"J Appl Non-Class Logics"},{"key":"10265_CR27","unstructured":"Darwiche A (2002) A compiler for deterministic, decomposable negation normal form. In: Proc. Conf. on artificial intelligence (AAAI), AAAI press, pp 627\u2013634"},{"key":"10265_CR28","unstructured":"Darwiche A (2004) New advances in compiling CNF to decomposable negation normal form. In: Proc. Europ. Conf. on artificial intelligence, IOS press, pp 318\u2013322"},{"key":"10265_CR29","unstructured":"Darwiche A (2011) SDD: a new canonical representation of propositional knowledge bases. AAAI Press, pp 819\u2013826"},{"issue":"1","key":"10265_CR30","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche A, Marquis P (2002) A knowledge compilation map. J Artif Intell Res (JAIR) 17(1):229\u2013264","journal-title":"J Artif Intell Res (JAIR)"},{"issue":"9","key":"10265_CR31","doi-asserted-by":"publisher","first-page":"895","DOI":"10.1109\/TSE.2014.2331073","volume":"40","author":"D Fern\u00e1ndez-Amor\u00f3s","year":"2014","unstructured":"Fern\u00e1ndez-Amor\u00f3s D, Heradio R, Cerrada JA, Cerrada C (2014) A scalable approach to exact model and commonality counting for extended feature models. IEEE Trans Softw Eng (TSE) 40(9):895\u2013910","journal-title":"IEEE Trans Softw Eng (TSE)"},{"key":"10265_CR32","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3459080","volume":"26","author":"JK Fichte","year":"2021","unstructured":"Fichte JK, Hecher M, Hamiti F (2021) The model counting competition 2020. ACM J Exp Algorithmics (JEA) 26:1\u201326 , 13:1\u201326","journal-title":"ACM J Exp Algorithmics (JEA)"},{"key":"10265_CR33","doi-asserted-by":"crossref","unstructured":"Fichte JK, Hecher M, Zisser M (2019) An Improved GPU-based SAT Model Counter. In: Proc. Int\u2019l conf. on principles and practice of constraint programming (CP), Springer, pp 491\u2013509","DOI":"10.1007\/978-3-030-30048-7_29"},{"key":"10265_CR34","doi-asserted-by":"crossref","unstructured":"Fritsch C, Abt R, Renz B (2020) The benefits of a feature model in banking. In: Proc. Int\u2019l systems and software product line conf. (SPLC). ACM","DOI":"10.1145\/3382025.3414946"},{"key":"10265_CR35","doi-asserted-by":"crossref","unstructured":"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\u2019l systems and software product line conf. (SPLC), ACM, pp 74\u201378","DOI":"10.1145\/2934466.2934478"},{"key":"10265_CR36","unstructured":"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\u201361"},{"key":"10265_CR37","unstructured":"Hadzic T, Subbarayan S, Jensen RM, Andersen HR, M\u00f8ller J, Hulgaard H (2004) Fast backtrack-free product configuration using a precompiled solution space representation. In: Proc. Int\u2019l conf. on economic, technical and organisational aspects of product configuration systems, Gamez publishing, pp 131\u2013138"},{"issue":"08","key":"10265_CR38","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1142\/S0218194013500368","volume":"23","author":"R Heradio","year":"2013","unstructured":"Heradio R, Fern\u00e1ndez-Amor\u00f3s D, Cerrada JA, Abad I (2013) A literature review on feature diagram product counting and its usage in software product line economic models. Int J Softw Eng Knowl Eng (IJSEKE) 23(08):1177\u20131204","journal-title":"Int J Softw Eng Knowl Eng (IJSEKE)"},{"key":"10265_CR39","doi-asserted-by":"crossref","unstructured":"Heradio R, Fern\u00e1ndez-Amor\u00f3s D, Mayr-Dorn C, Egyed A (2019) Supporting the statistical analysis of variability models. In: Proc. Int\u2019l conf. on software engineering (ICSE), IEEE, pp 843\u2013853","DOI":"10.1109\/ICSE.2019.00091"},{"key":"10265_CR40","unstructured":"Heradio R, P\u00e9rez-Morago HJ, Fern\u00e1ndez-Amor\u00f3s 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\u2019l Conf. on Intelligent Software Methodologies, Tools and Techniques (SOMET), IOS Press, pp 139\u2013154"},{"issue":"6","key":"10265_CR41","doi-asserted-by":"publisher","first-page":"496","DOI":"10.1049\/iet-sen.2010.0022","volume":"5","author":"R Heradio-Gil","year":"2011","unstructured":"Heradio-Gil R, Fern\u00e1ndez-Amor\u00f3s D, Cerrada JA, Cerrada C (2011) Supporting commonality-based analysis of software product lines. IET Softw 5(6):496\u2013509","journal-title":"IET Softw"},{"key":"10265_CR42","doi-asserted-by":"crossref","unstructured":"He\u00df T, Sundermann C, Th\u00fcm T (2021) On the scalability of building binary decision diagrams for current feature models. In: Proc. Int\u2019l systems and software product line conf. (SPLC), ACM, pp 131\u2013135","DOI":"10.1145\/3461001.3474452"},{"key":"10265_CR43","unstructured":"Huang J, Darwiche A (2005) DPLL with a trace: from SAT to knowledge compilation. In: Proc. Int\u2019l joint conf. on artificial intelligence (IJCAI), vol 5. Professional book center, pp 156\u2013162"},{"key":"10265_CR44","doi-asserted-by":"crossref","unstructured":"Huth M, Ryan M (2004) Logic in computer science: modelling and reasoning about systems. Cambridge University Press","DOI":"10.1017\/CBO9780511810275"},{"issue":"3","key":"10265_CR45","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1016\/j.jss.2009.09.042","volume":"83","author":"A Israeli","year":"2010","unstructured":"Israeli A, Feitelson DG (2010) The linux kernel as a case study in software evolution. J. Syst Softw (JSS) 83(3):485\u2013501","journal-title":"J. Syst Softw (JSS)"},{"key":"10265_CR46","doi-asserted-by":"crossref","unstructured":"K\u00e4stner C, Apel S, Batory D (2007) A case study implementing features using aspectJ. In: Proc. Int\u2019l systems and software product line conf. (SPLC), IEEE, pp 223\u2013232","DOI":"10.1109\/SPLINE.2007.12"},{"key":"10265_CR47","doi-asserted-by":"crossref","unstructured":"K\u00e4stner C, Th\u00fcm T, Saake G, Feigenspan J, Leich T, Wielgorz F (2009) FeatureIDE: a tool framework for feature-oriented software development. In: Proc. Int\u2019l Conf. on Software Engineering (ICSE), IEEE, pp 611\u2013614. Formal demonstration paper","DOI":"10.1109\/ICSE.2009.5070568"},{"key":"10265_CR48","doi-asserted-by":"crossref","unstructured":"Klebanov V, Manthey N, Muise C (2013) SAT-based analysis and quantification of information flow in programs. In: Proc. Int\u2019l conf. on quantitative evaluation of systems (QEST), Springer, pp 177\u2013192","DOI":"10.1007\/978-3-642-40196-1_16"},{"key":"10265_CR49","doi-asserted-by":"crossref","unstructured":"Kn\u00fcppel A, Th\u00fcm 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\u2013302","DOI":"10.1145\/3106237.3106252"},{"key":"10265_CR50","unstructured":"Koriche F, Lagniez J-M, Marquis P, Thomas S (2013) Knowledge compilation for model counting affine decision trees. In: Proc. Int\u2019l joint conf. on artificial intelligence (IJCAI), AAAI press"},{"key":"10265_CR51","doi-asserted-by":"crossref","unstructured":"Kowal M, Ananieva S, Th\u00fcm T (2016) Explaining anomalies in feature models. In: Proc. Int\u2019l conf. on generative programming: concepts & experiences (GPCE), ACM, pp 132\u2013143","DOI":"10.1145\/3093335.2993248"},{"key":"10265_CR52","doi-asserted-by":"crossref","unstructured":"Krieter S, Pinnecke M, Kr\u00fcger J, Sprey J, Sontag C, Th\u00fcm T, Leich T, Saake G (2017) Feature IDE empowering third-party developers. In: Proc. Int\u2019l systems and software product line conf. (SPLC), ACM, pp 42\u201345","DOI":"10.1145\/3109729.3109751"},{"key":"10265_CR53","doi-asserted-by":"crossref","unstructured":"Krieter S, Th\u00fcm T, Schulze S, Schr\u00f6ter R, Saake G (2018) Propagating configuration decisions with modal implication graphs. In: Proc. Int\u2019l conf. on software engineering (ICSE), ACM, pp 898\u2013909","DOI":"10.1145\/3180155.3180159"},{"key":"10265_CR54","doi-asserted-by":"crossref","unstructured":"K\u00fcbler A, Zengler C, K\u00fcchlin W (2010) Model counting in product configuration. In: Proc. Int\u2019l workshop on logics for component configuration (lococo), Open publishing association, pp 44\u201353","DOI":"10.4204\/EPTCS.29.5"},{"key":"10265_CR55","doi-asserted-by":"crossref","unstructured":"Lagniez J-M, Marquis P (2017) An improved decision-DNNF compiler. In: Proc. Int\u2019l joint conf. on artificial intelligence (IJCAI), pages 667\u2013673. International joint conferences on artificial intelligence","DOI":"10.24963\/ijcai.2017\/93"},{"key":"10265_CR56","doi-asserted-by":"crossref","unstructured":"Lagniez J-M, Marquis P, Szczepanski N (2018) DMC: a distributed model counter. In: Proc. Int\u2019l joint conf. on artificial intelligence (IJCAI), pp 1331\u20131338. International joint conferences on artificial intelligence","DOI":"10.24963\/ijcai.2018\/185"},{"issue":"2-3","key":"10265_CR57","doi-asserted-by":"publisher","first-page":"59","DOI":"10.3233\/SAT190075","volume":"7","author":"D Le Berre","year":"2010","unstructured":"Le Berre D, Parrain A (2010) The sat4j library, release 2.2. J Satisfiability Boolean Model Comput 7(2-3):59\u201364","journal-title":"J Satisfiability Boolean Model Comput"},{"key":"10265_CR58","doi-asserted-by":"crossref","unstructured":"McKnight PE, Najab J (2010) Mann-Whitney U test. Corsini Encycl Psychol 1\u20131","DOI":"10.1002\/9780470479216.corpsy0524"},{"issue":"5","key":"10265_CR59","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/j.scico.2009.12.004","volume":"75","author":"M Mendonca","year":"2010","unstructured":"Mendonca M, Cowan D (2010) Decision-making coordination and efficient reasoning techniques for Feature-Based configuration. Sci Comput Program (SCP) 75(5):311\u2013332","journal-title":"Sci Comput Program (SCP)"},{"key":"10265_CR60","volume-title":"Efficient reasoning techniques for large scale feature models","author":"M Mendon\u00e7a","year":"2009","unstructured":"Mendon\u00e7a M (2009) Efficient reasoning techniques for large scale feature models. University of Waterloo, PhD thesis"},{"key":"10265_CR61","doi-asserted-by":"crossref","unstructured":"Mendon\u00e7a 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\u2013762","DOI":"10.1145\/1639950.1640002"},{"key":"10265_CR62","unstructured":"Mendon\u00e7a M, Wa\u0307sowski A, Czarnecki K (2009) SAT-Based analysis of feature models is easy. In: Proc. Int\u2019l systems and software product line conf. (SPLC), Software engineering institute, pp 231\u2013240"},{"key":"10265_CR63","unstructured":"Muise C, McIlraith S, Beck JC, Hsu E (2010) Fast d-DNNF Compilation with sharpSAT. In: Proc. Conf. on artificial intelligence (AAAI). AAAI press"},{"key":"10265_CR64","doi-asserted-by":"crossref","unstructured":"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\u2019l systems and software product line conf. (SPLC), ACM, pp 289\u2013301","DOI":"10.1145\/3336294.3336297"},{"key":"10265_CR65","doi-asserted-by":"crossref","unstructured":"Nieke M, Mauro J, Seidl C, Th\u00fcm T, Yu IC, Franzke F (2018) Anomaly analyses for Feature-Model evolution. In: Proc. Int\u2019l conf. on generative programming: Concepts & experiences (GPCE), ACM, pp 188\u2013201","DOI":"10.1145\/3278122.3278123"},{"key":"10265_CR66","unstructured":"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"},{"key":"10265_CR67","doi-asserted-by":"crossref","unstructured":"Oh J, Batory D, Myers M, Siegmund N (2017) Finding Near-Optimal configurations in product lines by random sampling. In: Proc. Int\u2019l symposium on foundations of software engineering (FSE), pp 61\u201371","DOI":"10.1145\/3106237.3106273"},{"key":"10265_CR68","unstructured":"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"},{"key":"10265_CR69","doi-asserted-by":"crossref","unstructured":"Oztok U, Darwiche A (2014) On compiling CNF into decision-DNNF. In: Proc. Int\u2019l conf. on principles and practice of constraint programming (CP), Springer, pp 42\u201357","DOI":"10.1007\/978-3-319-10428-7_7"},{"key":"10265_CR70","unstructured":"Oztok U, Darwiche A (2015) A Top-Down compiler for sentential decision diagrams. In: Proc. Int\u2019l joint conf. on artificial intelligence (IJCAI), AAAI press, pp 3141\u20133148"},{"key":"10265_CR71","volume-title":"BDD Algorithms to perform hard analysis operations on variability models","author":"HJ P\u00e9rez Morago","year":"2016","unstructured":"P\u00e9rez Morago HJ (2016) BDD Algorithms to perform hard analysis operations on variability models. Universidad Nacional de Educaci\u00f3n a Distancia, PhD thesis"},{"key":"10265_CR72","doi-asserted-by":"crossref","unstructured":"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\u2019l conf. on software testing, verification and validation (ICST), IEEE, pp 459\u2013468","DOI":"10.1109\/ICST.2010.43"},{"key":"10265_CR73","doi-asserted-by":"crossref","unstructured":"Pett T, Krieter S, Runge T, Th\u00fcm T, Lochau M, Schaefer I (2021) Stability of Product-Line sampling in continuous integration. In: Proc. Int\u2019l working conf. on variability modelling of software-intensive systems (VaMoS). ACM","DOI":"10.1145\/3442391.3442410"},{"key":"10265_CR74","doi-asserted-by":"crossref","unstructured":"Pett T, Th\u00fcm T, Runge T, Krieter S, Lochau M, Schaefer I (2019) Product sampling for product lines the scalability challenge. In: Proc. Int\u2019l systems and software product line conf. (SPLC), ACM, pp 78\u201383","DOI":"10.1145\/3336294.3336322"},{"key":"10265_CR75","doi-asserted-by":"crossref","unstructured":"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\u2019l conf. on software testing, verification and validation (ICST), IEEE, pp 240\u2013251","DOI":"10.1109\/ICST.2019.00032"},{"key":"10265_CR76","doi-asserted-by":"crossref","unstructured":"Pohl R, Lauenroth K, Pohl K (2011) A performance comparison of contemporary algorithmic approaches for automated analysis operations on feature models. In: Proc. Int\u2019l conf. on automated software engineering (ASE), IEEE, pp 313\u2013322","DOI":"10.1109\/ASE.2011.6100068"},{"key":"10265_CR77","doi-asserted-by":"crossref","unstructured":"Rudell R (1993) Dynamic variable ordering for ordered binary decision diagrams. In: Proc. Int\u2019l conf. on computer-aided design (ICCAD), IEEE, pp 42\u201347","DOI":"10.1109\/ICCAD.1993.580029"},{"key":"10265_CR78","unstructured":"Sang T, Bacchus F, Beame P, Kautz HA, Pitassi T (2004) Combining component caching and clause learning for effective model counting. In: Proc. Int\u2019l conf. on theory and applications of satisfiability testing (SAT), Springer, pp 20\u201328"},{"key":"10265_CR79","doi-asserted-by":"crossref","unstructured":"Sang T, Beame P, Kautz H (2005) Heuristics for fast exact model counting. In: Proc. Int\u2019l conf. on theory and applications of satisfiability testing (SAT), Springer, pp 226\u2013240","DOI":"10.1007\/11499107_17"},{"key":"10265_CR80","doi-asserted-by":"crossref","unstructured":"Schr\u00f6ter R, Krieter S, Th\u00fcm T, Benduhn F, Saake G (2016) Feature-model interfaces: the highway to compositional analyses of Highly-Configurable systems. In: Proc. Int\u2019l conf. on software engineering (ICSE), ACM, pp 667\u2013678","DOI":"10.1145\/2884781.2884823"},{"key":"10265_CR81","unstructured":"Segura S (2008) Automated analysis of feature models using atomic sets. In: Proc. Int\u2019l systems and software product line conf. (SPLC), vol 2. IEEE, pp 201\u2013207"},{"key":"10265_CR82","unstructured":"Sharma S, Gupta R, Roy S, Meel KS (2018) Knowledge compilation meets uniform sampling. In: Proc. Int\u2019l conf. on logic for programming, artificial intelligence, and reasoning, Easy chair, pp 620\u2013636"},{"key":"10265_CR83","doi-asserted-by":"crossref","unstructured":"Sharma S, Roy S, Soos M, Meel KS (2019) GANAK: a scalable probabilistic exact model counter. In: Proc. Int\u2019l joint conf. on artificial intelligence (IJCAI), vol 19. AAAI press, pp 1169\u20131176","DOI":"10.24963\/ijcai.2019\/163"},{"issue":"4","key":"10265_CR84","doi-asserted-by":"publisher","first-page":"1670","DOI":"10.1007\/s10664-014-9336-6","volume":"21","author":"S Sobernig","year":"2016","unstructured":"Sobernig S, Apel S, Kolesnikov S, Siegmund N (2016) Quantifying structural attributes of system decompositions in 28 Feature-Oriented software product lines. Empir Softw Eng (EMSE) 21(4):1670\u20131705","journal-title":"Empir Softw Eng (EMSE)"},{"key":"10265_CR85","doi-asserted-by":"crossref","unstructured":"Sprey J, Sundermann C, Krieter S, Nieke M, Mauro J, Th\u00fcm T, Schaefer I (2020) SMT-based variability analyses in featureIDE. In: Proc. Int\u2019l working conf. on variability modelling of software-intensive systems (VaMoS). ACM","DOI":"10.1145\/3377024.3377036"},{"issue":"3","key":"10265_CR86","doi-asserted-by":"publisher","first-page":"279","DOI":"10.4300\/JGME-D-12-00156.1","volume":"4","author":"GM Sullivan","year":"2012","unstructured":"Sullivan GM, Feinn R (2012) Using effect size\u2014or why the P value is not enough. J Grad Med Educ 4(3):279\u2013282","journal-title":"J Grad Med Educ"},{"key":"10265_CR87","doi-asserted-by":"crossref","unstructured":"Sundermann C, Nieke M, Bittner PM, He\u00df T, Th\u00fcm T, Schaefer I (2021) Applications of #SAT solvers on feature models. In: Proc. Int\u2019l working conf. on variability modelling of software-intensive systems (VaMoS). ACM","DOI":"10.1145\/3442391.3442404"},{"key":"10265_CR88","doi-asserted-by":"crossref","unstructured":"Sundermann C, Th\u00fcm T, Schaefer I (2020) Evaluating #SAT solvers on industrial feature models. In: Proc. Int\u2019l working conf. on variability modelling of software-intensive systems (VaMoS). ACM","DOI":"10.1145\/3377024.3377025"},{"issue":"6","key":"10265_CR89","doi-asserted-by":"publisher","first-page":"391","DOI":"10.1002\/(SICI)1096-908X(199911\/12)11:6<391::AID-SMR199>3.0.CO;2-8","volume":"11","author":"M Svahnberg","year":"1999","unstructured":"Svahnberg M, Bosch J (1999) Evolution in software product lines two cases. J Softw Maint (JSM) 11(6):391\u2013422","journal-title":"J Softw Maint (JSM)"},{"key":"10265_CR90","doi-asserted-by":"crossref","unstructured":"Th\u00fcm T, K\u00e4stner C, Erdweg S, Siegmund N (2011) Abstract features in feature modeling. In: Proc. Int\u2019l systems and software product line conf. (SPLC), IEEE, pp 191\u2013200","DOI":"10.1109\/SPLC.2011.53"},{"key":"10265_CR91","doi-asserted-by":"crossref","unstructured":"Thurley M (2006) SharpSAT - counting models with advanced component caching and implicit BCP. In: Proc. Int\u2019l conf. on theory and applications of satisfiability testing (SAT), Springer pp 424\u2013429","DOI":"10.1007\/11814948_38"},{"issue":"1","key":"10265_CR92","first-page":"1.12:1","volume":"21","author":"T Toda","year":"2016","unstructured":"Toda T, Soh T (2016) Implementing efficient all solutions SAT solvers. ACM J Exp Algorithmics (JEA) 21(1):1.12:1\u20131.12:44","journal-title":"ACM J Exp Algorithmics (JEA)"},{"issue":"2","key":"10265_CR93","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1016\/0304-3975(79)90044-6","volume":"8","author":"LG Valiant","year":"1979","unstructured":"Valiant LG (1979) The complexity of computing the permanent. Theor Comput Sci 8(2):189\u2013201","journal-title":"Theor Comput Sci"},{"key":"10265_CR94","doi-asserted-by":"crossref","unstructured":"Wei W, Selman B (2005) A new approach to model counting. In: Proc. Int\u2019l conf. on theory and applications of satisfiability testing (SAT), Springer, pp 324\u2013339","DOI":"10.1007\/11499107_24"},{"key":"10265_CR95","doi-asserted-by":"publisher","first-page":"565","DOI":"10.1613\/jair.2490","volume":"32","author":"L Xu","year":"2008","unstructured":"Xu L, Hutter F, Hoos HH, Leyton-Brown K (2008) SATzilla: portfolio-based algorithm selection for SAT. J Artif Intell Res (JAIR) 32:565\u2013606","journal-title":"J Artif Intell Res (JAIR)"},{"issue":"339","key":"10265_CR96","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1080\/01621459.1972.10481251","volume":"67","author":"JH Zar","year":"1972","unstructured":"Zar JH (1972) Significance testing of the spearman rank correlation coefficient. J Am Stat Assoc 67(339):578\u2013580","journal-title":"J Am Stat Assoc"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-022-10265-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10664-022-10265-9\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-022-10265-9.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,12]],"date-time":"2024-10-12T05:08:16Z","timestamp":1728709696000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10664-022-10265-9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,13]]},"references-count":96,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["10265"],"URL":"https:\/\/doi.org\/10.1007\/s10664-022-10265-9","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"value":"1382-3256","type":"print"},{"value":"1573-7616","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,13]]},"assertion":[{"value":"25 November 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 January 2023","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no conflicts of interest to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"<!--Emphasis Type='Bold' removed-->Conflict of Interests"}}],"article-number":"29"}}