{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T13:19:28Z","timestamp":1770297568393,"version":"3.49.0"},"reference-count":114,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2022,11,28]],"date-time":"2022-11-28T00:00:00Z","timestamp":1669593600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,11,28]],"date-time":"2022-11-28T00:00:00Z","timestamp":1669593600000},"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,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Incremental satisfiability (SAT) solving is an extension of classic SAT solving that enables solving a set of related SAT problems by identifying and exploiting shared terms. However, using incremental solvers effectively is hard since performance is sensitive to the input order of subterms and results must be tracked manually. For analyses that generate sets of related SAT problems, such as those in software product lines, incremental solvers are either not used or their use is not clearly described in the literature. This paper translates the ordering problem to an encoding problem and automates the use of incremental solving. We introduce <jats:italic>variational<\/jats:italic> SAT solving, which differs from incremental solving by accepting all related problems as a single variational input and returning all results as a single variational output. Variational solving syntactically encodes differences in related SAT problems as local points of variation. With this syntax, our approach automates the interaction with the incremental solver and enables a method to automatically optimize sharing in the input. To evaluate these ideas, we formalize a variational SAT algorithm, construct a prototype variational solver, and perform an empirical analysis on two real-world datasets that applied incremental solvers to software evolution scenarios. We show, assuming a variational input, that the prototype solver scales better for these problems than four off-the-shelf incremental solvers while also automatically tracking individual results.<\/jats:p>","DOI":"10.1007\/s10664-022-10217-3","type":"journal-article","created":{"date-parts":[[2022,11,28]],"date-time":"2022-11-28T09:08:54Z","timestamp":1669626534000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Variational satisfiability solving: efficiently solving lots of related SAT problems"],"prefix":"10.1007","volume":"28","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2935-772X","authenticated-orcid":false,"given":"Jeffrey M.","family":"Young","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9388-0649","authenticated-orcid":false,"given":"Paul Maximilian","family":"Bittner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1214-0791","authenticated-orcid":false,"given":"Eric","family":"Walkingshaw","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8069-9584","authenticated-orcid":false,"given":"Thomas","family":"Th\u00fcm","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,11,28]]},"reference":[{"key":"10217_CR1","doi-asserted-by":"crossref","unstructured":"Acher M, Collet P, Lahire P, France RB (2011) slicing feature models. In: Proceeding Int\u2019l conference on automated software engineering (ASE). IEEE, pp 424\u2013427","DOI":"10.1109\/ASE.2011.6100089"},{"key":"10217_CR2","doi-asserted-by":"publisher","unstructured":"Aloul FA, Ramani A, Markov IL, Sakallah KA (2002) Generic ilp versus specialized 0-1 ilp: an update. In: Proceedings of the 2002 IEEE\/ACM international conference on computer-aided design, association for computing machinery, New York, ICCAD \u201902, pp 450\u2013457, https:\/\/doi.org\/10.1145\/774572.774638","DOI":"10.1145\/774572.774638"},{"key":"10217_CR3","doi-asserted-by":"crossref","unstructured":"Ananieva S, Kowal M, Th\u00fcm T, Schaefer I (2016) Implicit constraints in partial feature models. In: Int work on feature-oriented software development (FOSD), ACM, pp 18\u201327","DOI":"10.1145\/3001867.3001870"},{"key":"10217_CR4","doi-asserted-by":"crossref","unstructured":"Apel S, Scholz W, Lengauer C, K\u00e4stner C (2010) Language-independent reference checking in software product lines. In: Int work on feature-oriented software development (FOSD), ACM, pp 65\u201371","DOI":"10.1145\/1868688.1868698"},{"key":"10217_CR5","doi-asserted-by":"crossref","unstructured":"Ataei P, Termehchy A, Walkingshaw E (2017) Variational Databases. In: International Symp on database programming languages (DBPL), ACM, pp 11:1\u201311:4","DOI":"10.1145\/3122831.3122839"},{"key":"10217_CR6","doi-asserted-by":"crossref","unstructured":"Ataei P, Termehchy A, Walkingshaw E (2018) Managing structurally heterogeneous databases in software product lines. In: VLDB workshop: polystores and other systems for heterogeneous data (Poly)","DOI":"10.1007\/978-3-030-14177-6_6"},{"key":"10217_CR7","doi-asserted-by":"crossref","unstructured":"Ataei P, Khan F, Walkingshaw E (2021) A variational database management system. In: ACM SIGPLAN int Conf on Generative Programming: concepts and Experiences (GPCE), to appear","DOI":"10.1145\/3486609.3487197"},{"key":"10217_CR8","doi-asserted-by":"crossref","unstructured":"Ataei P, Li Q, Walkingshaw E (2021) Should variation be encoded explicitly in databases?. In: Int working conf on variability modelling of software-intensive systems (VaMoS), pp 3:1\u20133:9","DOI":"10.1145\/3442391.3442395"},{"key":"10217_CR9","doi-asserted-by":"crossref","unstructured":"Austin TH, Flanagan C (2012) Multiple facets for dynamic information flow. In: Proceedings of the 39th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, pp 165\u2013178","DOI":"10.1145\/2103656.2103677"},{"key":"10217_CR10","doi-asserted-by":"publisher","unstructured":"Austin TH, Yang J, Flanagan C, Solar-Lezama A (2013) Faceted execution of policy-agnostic programs. In: Proceedings of the eighth ACM SIGPLAN workshop on programming languages and analysis for security, association for computing machinery, New York, PLAS \u201913, pP 15\u201326, https:\/\/doi.org\/10.1145\/2465106.2465121","DOI":"10.1145\/2465106.2465121"},{"key":"10217_CR11","doi-asserted-by":"crossref","unstructured":"Balyo T, Froleyks N, Heule M, Iser M, J\u00e4rvisalo M, Suda M (eds) (2020) Proceedings of SAT Competition 2020: solver and benchmark descriptions. Department of computer science report series b department of computer science. University of Helsinki, Finland","DOI":"10.1016\/j.artint.2021.103572"},{"key":"10217_CR12","doi-asserted-by":"crossref","unstructured":"Barrett C, Tinelli C (2018) Satisfiability modulo theories. In: Handbook of Model Checking. Springer, pp 305\u2013343","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"10217_CR13","unstructured":"Barrett C, Stump A, Tinelli C (2010) The SMT-LIB standard: version 2.0 Tech rep, Department of Computer Science. The University of Iowa, available at www.SMT-LIB.org"},{"key":"10217_CR14","doi-asserted-by":"crossref","unstructured":"Barrett C, Conway CL, Deters M, Hadarean L, Jovanovi\u0107 D, King T, Reynolds A, Tinelli C (2011) cvc4. In: Gopalakrishnan G, Qadeer S (eds) Computer aided verification. springer, Heidelberg, pp 171\u2013177","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"10217_CR15","unstructured":"Barrett C, Fontaine P, Tinelli C (2016) The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org"},{"key":"10217_CR16","doi-asserted-by":"crossref","unstructured":"Batory D (2005) Feature models, grammars, and propositional formulas. In: ACM SIGSOFT int systems and software product line conf (SPLC). Springer, pp 7\u201320","DOI":"10.1007\/11554844_3"},{"key":"10217_CR17","doi-asserted-by":"crossref","unstructured":"Benavides D, Ruiz-Cort\u00e9s A, Trinidad P (2005) Automated reasoning on feature models. In: Proceeding int\u2019l conference on advanced information systems engineering (CAiSE), pp 491\u2013503","DOI":"10.1007\/11431855_34"},{"issue":"6","key":"10217_CR18","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. Inform Syst 35(6):615\u2013708","journal-title":"Inform Syst"},{"key":"10217_CR19","unstructured":"Biere A, Biere A, Heule M, Van Maaren H, Walsh T (2009) Handbook of satisfiability: vol 185 frontiers in artificial intelligence and applications. IOS Press"},{"key":"10217_CR20","doi-asserted-by":"crossref","unstructured":"Bittner PM, Th\u00fcm T, Schaefer I (2019) Sat encodings of the at-most-k constraint. In: \u00d6lveczky PC, Sala\u00fcn G (eds) Software engineering and formal methods. Springer International Publishing, Cham, pp 127\u2013144","DOI":"10.1007\/978-3-030-30446-1_7"},{"key":"10217_CR21","doi-asserted-by":"crossref","unstructured":"Bodden E, Tol\u00eado T, Ribeiro M, Brabrand C, Borba P, Mezini M (2013 ) SPLLIFT: statically analyzing software product lines in minutes instead of years. In: Proceeding ACM SIGPLAN conf on programming language design and implementation (PLDI), ACM, pp 355\u2013364","DOI":"10.1145\/2499370.2491976"},{"key":"10217_CR22","doi-asserted-by":"publisher","unstructured":"Brummayer R, Biere A (2009) Boolector: an efficient SMT solver for bit-vectors and arrays. In: Kowalewski S, Philippou A (eds) Tools and algorithms for the construction and analysis of systems, 15th international conference, TACAS 2009, held as part of the joint european conferences on theory and practice of software, ETAPS 2009, York, UK, 22-29 March 2009. Proceedings, Springer, lecture notes in computer science, vol 5505, pp 174\u2013177, https:\/\/doi.org\/10.1007\/978-3-642-00768-2_16","DOI":"10.1007\/978-3-642-00768-2_16"},{"key":"10217_CR23","unstructured":"Brummayer R, Biere A (2021) Boolector: a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions. https:\/\/boolector.github.io\/ Accessed at 12 Sept 2021"},{"key":"10217_CR24","first-page":"15:1","volume":"2","author":"IIIJP Campora","year":"2018","unstructured":"Campora IIIJP, Chen S, Erwig M, Walkingshaw E (2018) Migrating gradual types. Proc of the ACM on Program Languages (PACMPL) Issue, ACM SIGPLAN Sympon Principles of Program Languages (POPL) 2:15:1\u201315:29","journal-title":"Proc of the ACM on Program Languages (PACMPL) Issue, ACM SIGPLAN Sympon Principles of Program Languages (POPL)"},{"key":"10217_CR25","first-page":"98:1","volume":"2","author":"IIIJP Campora","year":"2018","unstructured":"Campora IIIJP, Chen S, Walkingshaw E (2018) Casts and costs: harmonizing safety and performance in gradual typing. Proc of the ACM on Program Languages (PACMPL) issue, ACM SIGPLAN IntConfon Functional Program (ICFP) 2:98:1\u201398:30","journal-title":"Proc of the ACM on Program Languages (PACMPL) issue, ACM SIGPLAN IntConfon Functional Program (ICFP)"},{"issue":"10","key":"10217_CR26","doi-asserted-by":"publisher","first-page":"1183","DOI":"10.1016\/j.infsof.2014.04.002","volume":"56","author":"ID Carmo Machado","year":"2014","unstructured":"Carmo Machado ID, McGregor JD, Cavalcanti YaC, De Almeida ES (2014) On strategies for testing software product lines: a systematic literature review. JInform Softw Technol (IST) 56(10):1183\u20131199","journal-title":"JInform Softw Technol (IST)"},{"key":"10217_CR27","doi-asserted-by":"crossref","unstructured":"Chen S, Erwig M (2014) Counter-factual typing for debugging type errors. In: ACM SIGPLAN-SIGACT Symp on Principles of Program Languages, pp 583\u2013594","DOI":"10.1145\/2578855.2535863"},{"key":"10217_CR28","doi-asserted-by":"crossref","unstructured":"Chen S, Erwig M, Walkingshaw E (2012) An error-tolerant type system for variational lambda calculus. In: ACM SIGPLAN Int Conf on Functional Program (ICFP), pp 29\u201340","DOI":"10.1145\/2398856.2364535"},{"key":"10217_CR29","doi-asserted-by":"crossref","unstructured":"Chen S, Erwig M, Smeltzer K (2014) Let\u2019s hear both sides: on combining type-error reporting tools. In: IEEE int symp on visual languages and human-centric computing, pp 145\u2013152","DOI":"10.1109\/VLHCC.2014.6883038"},{"issue":"1","key":"10217_CR30","doi-asserted-by":"publisher","first-page":"1:1","DOI":"10.1145\/2518190","volume":"36","author":"S Chen","year":"2014","unstructured":"Chen S, Erwig M, Walkingshaw E (2014) Extending Type Inference to Variational Programs. ACM Trans Program Languages Syst 36(1):1:1\u20131:54","journal-title":"ACM Trans Program Languages Syst"},{"key":"10217_CR31","unstructured":"Chen S, Erwig M, Walkingshaw E (2016) A calculus for variational programming. In: European conference on object-oriented programming (ECOOP), LIPIcs, vol 56, pp 6:1\u20136:26"},{"key":"10217_CR32","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1016\/j.jvlc.2016.07.001","volume":"39","author":"S Chen","year":"2017","unstructured":"Chen S, Erwig M, Smeltzer K (2017) Exploiting diversity in type checkers for better error messages. J Vis Languages Comput 39:10\u201321","journal-title":"J Vis Languages Comput"},{"key":"10217_CR33","doi-asserted-by":"publisher","unstructured":"Claessen K, Hughes J (2000) Quickcheck: a lightweight tool for random testing of haskell programs. In: Proceedings of the fifth ACM SIGPLAN international conference on functional programming, association for computing machinery, New York, ICFP \u201900, pp 268\u2013279, https:\/\/doi.org\/10.1145\/351240.351266","DOI":"10.1145\/351240.351266"},{"issue":"2","key":"10217_CR34","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"EM Clarke","year":"1986","unstructured":"Clarke EM, Emerson EA, Sistla AP (1986) Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans Program Lang Syst 8(2):244\u2013263. https:\/\/doi.org\/10.1145\/5397.5399","journal-title":"ACM Trans Program Lang Syst"},{"issue":"8","key":"10217_CR35","doi-asserted-by":"publisher","first-page":"1069","DOI":"10.1109\/TSE.2012.86","volume":"39","author":"A Classen","year":"2013","unstructured":"Classen A, Cordy M, Schobbens PY, Heymans P, Legay A, Raskin JF (2013) Featured transition systems: foundations for verifying variability-intensive systems and their application to ltl model checking. IEEE Transon Softw Eng 39 (8):1069\u20131089","journal-title":"IEEE Transon Softw Eng"},{"key":"10217_CR36","doi-asserted-by":"publisher","unstructured":"Coudert O, Madre JC (1995) New ideas for solving covering problems. In: Proceedings of the 32nd Annual ACM\/IEEE design automation conference, association for computing machinery, New York, DAC \u201995, pp 641\u2013646. https:\/\/doi.org\/10.1145\/217474.217603","DOI":"10.1145\/217474.217603"},{"key":"10217_CR37","doi-asserted-by":"crossref","unstructured":"Czarnecki K, Pietroszek K (2006) Verifying feature-based model templates against well-formedness ocl constraints. In: ACM SIGPLAN conf on generative programming and component engineering. ACM, pp 211\u2013220","DOI":"10.1145\/1173706.1173738"},{"key":"10217_CR38","doi-asserted-by":"crossref","unstructured":"Czarnecki K, Wa\u0307sowski A (2007) Feature diagrams and logics: there and back again. In: ACM SIGSOFT Int systems and software product line conf (SPLC). IEEE, pp 23\u201334","DOI":"10.1109\/SPLINE.2007.24"},{"key":"10217_CR39","doi-asserted-by":"crossref","unstructured":"Dutertre B (2014) Yices 2.2. In: Biere A, Bloem R (eds) Computer-aided verification (CAV\u20192014), Springer, lecture notes in computer science, vol 8559, pp 737\u2013744","DOI":"10.1007\/978-3-319-08867-9_49"},{"issue":"4","key":"10217_CR40","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","volume":"89","author":"N E\u00e9n","year":"2003","unstructured":"E\u00e9n N, S\u00f6rensson N (2003) Temporal induction by incremental sat solving. Electr Notes Theoretical Comput Sci 89(4):543\u2013560","journal-title":"Electr Notes Theoretical Comput Sci"},{"key":"10217_CR41","doi-asserted-by":"crossref","unstructured":"E\u00e9n N, S\u00f6rensson N (2004) An extensible sat-solver. In: Giunchiglia E, Tacchella A (eds) Theory and applications of satisfiability testing. Springer, Heidelberg, pp 502\u2013518","DOI":"10.1007\/978-3-540-24605-3_37"},{"key":"10217_CR42","unstructured":"Erkok L (2011) SBV: SMT Based Verification: Symbolic Haskell Theorem prover using SMT solving. Website available online at https:\/\/hackage.haskell.org\/package\/sbv-8.10; visited on 14th Feb 2020"},{"key":"10217_CR43","doi-asserted-by":"crossref","unstructured":"Erwig M, Smeltzer K (2018) Variational Pictures. In: International conference on the theory and application of diagrams, LNAI 10871, pp 55\u201370","DOI":"10.1007\/978-3-319-91376-6_9"},{"issue":"1","key":"10217_CR44","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/2063239.2063245","volume":"21","author":"M Erwig","year":"2011","unstructured":"Erwig M, Walkingshaw E (2011) The choice calculus: a representation for software variation. ACM Trans Softw Eng Method (TOSEM) 21(1):6:1\u20136:27","journal-title":"ACM Trans Softw Eng Method (TOSEM)"},{"key":"10217_CR45","doi-asserted-by":"crossref","unstructured":"Erwig M, Walkingshaw E, Chen S (2013) An abstract representation of variational graphs. In: Int work on feature-oriented software development (FOSD), ACM, pp 25\u201332","DOI":"10.1145\/2528265.2528270"},{"key":"10217_CR46","doi-asserted-by":"crossref","unstructured":"Fenske W, Meinicke J, Schulze S, Schulze S, Saake G (2017) Variant-preserving refactorings for migrating cloned products to a product line. In: ProcEEDING int\u2019l conference on software analysis, evolution and reengineering (SANER). IEEE, pp 316\u2013326","DOI":"10.1109\/SANER.2017.7884632"},{"issue":"5","key":"10217_CR47","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/s00607-018-0646-1","volume":"101","author":"JA Galindo","year":"2019","unstructured":"Galindo JA, Benavides D, Trinidad P, Guti\u00e9rrez-Fern\u00e1ndez AM, Ruiz-Cort\u00e9s A (2019) Automated analysis of feature models: quo vadis? Computing 101(5):387\u2013433","journal-title":"Computing"},{"key":"10217_CR48","unstructured":"Garson J (2018) Modal logic. In: Zalta EN (ed) The stanford encyclopedia of philosophy, fall 2018 edn., Metaphysics Research Lab, Stanford University"},{"key":"10217_CR49","unstructured":"Gent IP, Walsh T (1994) The sat phase transition. In: In proceeding ECAI-94, pp 105\u2013109"},{"issue":"2","key":"10217_CR50","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1002\/j.1538-7305.1950.tb00463.x","volume":"29","author":"RW Hamming","year":"1950","unstructured":"Hamming RW (1950) Error detecting and error correcting codes. Bell Syst Tech J 29(2):147\u2013160","journal-title":"Bell Syst Tech J"},{"key":"10217_CR51","doi-asserted-by":"crossref","unstructured":"Harper R (2016) Practical foundations for programming languages. Cambridge University Press","DOI":"10.1017\/CBO9781316576892"},{"issue":"2","key":"10217_CR52","first-page":"65","volume":"6","author":"S Holm","year":"1979","unstructured":"Holm S (1979) A simple sequentially rejective multiple test procedure. Scandinavian J Stat 6(2):65\u201370. http:\/\/www.jstor.org\/stable\/4615733","journal-title":"Scandinavian J Stat"},{"key":"10217_CR53","doi-asserted-by":"publisher","unstructured":"Hooker JN (1993) Solving the incremental satisfiability problem. https:\/\/doi.org\/10.1184\/R1\/6708044.v1, https:\/\/kilthub.cmu.edu\/articles\/journal_contribution\/Solving_the_Incremental_Satisfiability_Problem\/6708044\/1","DOI":"10.1184\/R1\/6708044.v1"},{"issue":"5","key":"10217_CR54","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1016\/j.scico.2008.09.007","volume":"76","author":"SS Huang","year":"2011","unstructured":"Huang SS, Zook D, Smaragdakis Y (2011) Statically Safe Program Generation with SafeGen. Sci Comput Program (SCP) 76(5):376\u2013391","journal-title":"Sci Comput Program (SCP)"},{"issue":"5","key":"10217_CR55","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/130697.130699","volume":"27","author":"P Hudak","year":"1992","unstructured":"Hudak P, Peyton Jones S, Wadler P, Boutel B, Fairbairn J, Fasel J, Guzm\u00e1n MM, Hammond K, Hughes J, Johnsson T, Kieburtz D, Nikhil R, Partain W, Peterson J (1992) Report on the programming language haskell: a non-strict. Purely Functional Lang Version 1.2. SIGPLAN Not 27(5):1\u2013164. https:\/\/doi.org\/10.1145\/130697.130699","journal-title":"Purely Functional Lang Version 1.2. SIGPLAN Not"},{"issue":"5","key":"10217_CR56","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1017\/S0956796897002864","volume":"7","author":"G Huet","year":"1997","unstructured":"Huet G (1997) The zipper. J Functional Program 7(5):549\u2013554. https:\/\/doi.org\/10.1017\/S0956796897002864","journal-title":"J Functional Program"},{"key":"10217_CR57","doi-asserted-by":"crossref","unstructured":"K\u00e4stner C, Giarrusso PG, Rendel T, Erdweg S, Ostermann K, Berger T (2011) Variability-Aware parsing in the presence of lexical macros and conditional compilation. In: Proceeding conference on object-oriented programming, systems, languages and applications (OOPSLA), ACM, pp 805\u2013824","DOI":"10.1145\/2076021.2048128"},{"key":"10217_CR58","doi-asserted-by":"crossref","unstructured":"K\u00e4stner C, Ostermann K, Erdweg S (2012) A variability-Aware module system. In: Proceeding conference on object-oriented programming, systems, languages and applications(OOPSLA), ACM, pp 773\u2013792","DOI":"10.1145\/2398857.2384673"},{"key":"10217_CR59","doi-asserted-by":"publisher","unstructured":"Kim J, Whittemore J, Marques-Silva J, Sakallah K (2000) On applying incremental satisfiability to delay fault testing. In: Proceedings of the conference on design, automation and test in europe, association for computing machinery, New York, Date \u201900, pp 380\u2013384, https:\/\/doi.org\/10.1145\/343647.343801","DOI":"10.1145\/343647.343801"},{"key":"10217_CR60","unstructured":"Kim J, Whittemore JP, Marques-Silva J, Sakallah KA (2000) On solving Stack-Based incremental satisfiability problems. In: Proceeding of IEEE international conference on computer design (ICCD). Austin, Texas, pp 379\u2013382"},{"key":"10217_CR61","unstructured":"Kleene SC (1968) Introduction to metamathematics. Ishi Press"},{"key":"10217_CR62","doi-asserted-by":"crossref","unstructured":"Kocher P, Horn J, Fogh A, Genkin D, Gruss D, Haas W, Hamburg M, Lipp M, Mangard S, Prescher T, Schwarz M, Yarom Y (2019) Spectre attacks: exploiting speculative execution. In: 40th IEEE symposium on security and privacy (S&P\u201919)","DOI":"10.1109\/SP.2019.00002"},{"key":"10217_CR63","doi-asserted-by":"crossref","unstructured":"Kowal M, Ananieva S, Th\u00fcm T (2016) Explaining anomalies in feature models. In: Proceeding int\u2019l conference on generative programming: concepts & experiences (GPCE), ACM, pp 132\u2013143","DOI":"10.1145\/3093335.2993248"},{"key":"10217_CR64","doi-asserted-by":"crossref","unstructured":"Krieter S, Schr\u00f6ter R, Th\u00fcm T, Fenske W, Saake G (2016) Comparing algorithms for efficient feature-model slicing. In: ACM SIGSOFT Int systems and software product line conf.(SPLC), ACM, pp 60\u201364","DOI":"10.1145\/2934466.2934477"},{"key":"10217_CR65","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":"10217_CR66","doi-asserted-by":"crossref","unstructured":"K\u00e4stner C, Giarrusso PG, Ostermann K (2011) Partial preprocessing c code for variability analysis. In: In Proceeding 5th ACM workshop on variability modeling of software-intensive systems, pp 127\u2013136","DOI":"10.1145\/1944892.1944908"},{"key":"10217_CR67","unstructured":"Labs R (2020) Redis. https:\/\/redis.io\/, Accessed at 4th May 2020"},{"key":"10217_CR68","unstructured":"Larabel M (2020) A global switch to kill linux\u2019s CPU spectre\/meltdown workarounds?. https:\/\/www.phoronix.com\/scan.php?page=news_item&px=Global-Switch-Skip-Spectre-Melt, Accessed at 25th March 2020"},{"issue":"2-3","key":"10217_CR69","first-page":"59","volume":"7","author":"D Le Berre","year":"2010","unstructured":"Le Berre D, Parrain A (2010) The Sat4j Library. Release 2.2 7 (2-3):59\u201364","journal-title":"Release 2.2"},{"issue":"8","key":"10217_CR70","first-page":"707","volume":"10","author":"VI Levenshtein","year":"1966","unstructured":"Levenshtein VI (1966) Binary codes capable of correcting deletions, insertions and reversals. Soviet Physics Doklady 10(8):707\u2013710. doklady Akademii Nauk SSSR, V163 No4 845-848 1965","journal-title":"Soviet Physics Doklady"},{"key":"10217_CR71","doi-asserted-by":"crossref","unstructured":"Liebig J, K\u00e4stner C, Apel S (2011) Analyzing the discipline of preprocessor annotations in 30 million lines of c code. In: Int. conf. on aspect-oriented software development, pp 191\u2013202","DOI":"10.1145\/1960275.1960299"},{"key":"10217_CR72","doi-asserted-by":"crossref","unstructured":"Liebig J, von Rhein A, K\u00e4stner C, Apel S, D\u00f6rre J, Lengauer C (2013) Scalable analysis of variable software, ACM","DOI":"10.1145\/2491411.2491437"},{"key":"10217_CR73","doi-asserted-by":"crossref","unstructured":"Lin C L (1994) Hardness of approximating graph transformation problem. In: Du DZ, Zhang XS (eds) Algorithms and computation. Springer, Berlin, pp 74\u201382","DOI":"10.1007\/3-540-58325-4_168"},{"key":"10217_CR74","unstructured":"Lipp M, Schwarz M, Gruss D, Prescher T, Haas W, Fogh A, Horn J, Mangard S, Kocher P, Genkin D, Yarom Y, Hamburg M (2018) Meltdown: Reading kernel memory from user space. In: 27th USENIX security symposium (USENIX Security 18)"},{"key":"10217_CR75","doi-asserted-by":"publisher","unstructured":"Mauro J (2021) Anomaly detection in context-aware feature models. In: 15th international working conference on variability modelling of software-intensive systems. VaMoS\u201921, https:\/\/doi.org\/10.1145\/3442391.3442405. Association for Computing Machinery, New York","DOI":"10.1145\/3442391.3442405"},{"key":"10217_CR76","doi-asserted-by":"crossref","unstructured":"Mauro J, Nieke M, Seidl C, Yu IC (2017) Anomaly detection and explanation in context-aware software product lines. In: ACM SIGSOFT int. systems and software product line conf. (SPLC). ACM, pp 18\u201321","DOI":"10.1145\/3109729.3109752"},{"key":"10217_CR77","doi-asserted-by":"crossref","unstructured":"Medeiros F, K\u00e4stner C, Ribeiro M, Gheyi R, Apel S (2016) A comparison of 10 sampling algorithms for configurable systems. In: Proc. int\u2019l conf. on software engineering (ICSE). ACM, pp 643\u2013654","DOI":"10.1145\/2884781.2884793"},{"key":"10217_CR78","unstructured":"Meinicke J (2014) Varexj: a variability-aware interpreter for java applications. Master\u2019s thesis, University of Magdeburg"},{"key":"10217_CR79","unstructured":"Meinicke J (2019) Variational debugging: understanding differences among executions. PhD dissertation, University of Magdeburg"},{"key":"10217_CR80","doi-asserted-by":"crossref","unstructured":"Mendon\u00e7a M, Wa\u0327sowski A, Czarnecki K, Cowan D (2008) Efficient compilation techniques for large scale feature models. In: ACM SIGPLAN conf. on generative programming and component engineering. ACM, pp 13\u201322","DOI":"10.1145\/1449913.1449918"},{"key":"10217_CR81","doi-asserted-by":"crossref","unstructured":"Meng M, Meinicke J, Wong CP, Walkingshaw E, K\u00e4stner C (2017) A choice of variational stacks: exploring variational data structures. In: Int. work. on variability modelling of software-intensive systems (VaMoS). ACM, pp 28\u201335","DOI":"10.1145\/3023956.3023966"},{"key":"10217_CR82","doi-asserted-by":"publisher","unstructured":"Micinski K., Darais D., Gilray T (2020) Abstracting faceted execution. In: 2020 IEEE 33rd computer security foundations symposium (CSF). pp 184\u2013198. https:\/\/doi.org\/10.1109\/CSF49147.2020.00021","DOI":"10.1109\/CSF49147.2020.00021"},{"key":"10217_CR83","doi-asserted-by":"publisher","unstructured":"Moskewicz MW, Madigan CF, Zhao Y, Zhang L, Malik S (2001) Chaff: Engineering an efficient sat solver. In: Proceedings of the 38th annual design automation conference, DAC \u201901. ACM, New York, pp 530\u2013535. https:\/\/doi.org\/10.1145\/378239.379017","DOI":"10.1145\/378239.379017"},{"key":"10217_CR84","doi-asserted-by":"crossref","unstructured":"de Moura L, Bj\u00f8rner N (2008) Z3: an efficient smt solver. In: Ramakrishnan CR, Rehof J (eds) Tools and algorithms for the construction and analysis of systems. Springer, Heidelberg, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10217_CR85","doi-asserted-by":"crossref","unstructured":"Nadel A, Ryvchin V, Strichman O (2014) Ultimately incremental sat. In: Sinz C, Egly U (eds) Theory and applications of satisfiability testing \u2013 SAT 2014. Springer International Publishing, Cham, pp 206\u2013218","DOI":"10.1007\/978-3-319-09284-3_16"},{"key":"10217_CR86","unstructured":"National Institute of Standards and Technology (2020) NIST e-handbook of statistical methods. https:\/\/www.itl.nist.gov\/div898\/handbook\/index.htm, Accessed at 7th May 2020"},{"key":"10217_CR87","doi-asserted-by":"crossref","unstructured":"Nguyen H V, K\u00e4stner C, Nguyen TN (2014) Exploring Variability-Aware execution for testing Plugin-Based web applications. In: Proc. int\u2019l conf. on software engineering (ICSE), ACM, pp 907\u2013918","DOI":"10.1145\/2568225.2568300"},{"key":"10217_CR88","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: ACM SIGPLAN Conf. on generative programming and component engineering, ACM, pp 188\u2013201","DOI":"10.1145\/3278122.3278123"},{"key":"10217_CR89","unstructured":"O\u2019Sullivan B (2009) Criterian: a Haskell Microbenchmarking library. Website available online at https:\/\/hackage.haskell.org\/package\/gauge-0.2.5; visited on 7th May 2020"},{"key":"10217_CR90","unstructured":"R Core Team (2020) R: a language and environment for statistical computing. R foundation for statistical computing, Vienna, Austria, https:\/\/www.R-project.org\/"},{"key":"10217_CR91","volume-title":"Many-Valued Logic","author":"N Rescher","year":"1969","unstructured":"Rescher N (1969) Many-Valued Logic. Mcgraw-Hill, New York"},{"key":"10217_CR92","doi-asserted-by":"crossref","unstructured":"von Rhein A, Grebhahn A, Apel S, Siegmund N, Beyer D, Berger T (2015) Presence-Condition simplification in highly configurable systems. In: Proc. int\u2019l conf. on software engineering (ICSE). IEEE, pp 178\u2013188","DOI":"10.1109\/ICSE.2015.39"},{"key":"10217_CR93","volume-title":"Artificial Intelligence: A Modern Approach. 3rd edn","author":"S Russell","year":"2009","unstructured":"Russell S, Norvig P (2009) Artificial Intelligence: A Modern Approach. 3rd edn. Prentice Hall Press, USA"},{"key":"10217_CR94","unstructured":"Competition SAT (2021) SAT Competition 2021: incremental library track. https:\/\/satcompetition.github.io\/2021\/track_incremental.html. Accessed at 21 May 2022"},{"key":"10217_CR95","doi-asserted-by":"crossref","unstructured":"Sayyad AS, Ingram J, Menzies T, Ammar H (2013) Scalable Product line configuration: a straw to break the camel\u2019s back. In: Proc.int\u2019l conf.on automated software engineering (ASE). IEEE, pp 465\u2013474","DOI":"10.1109\/ASE.2013.6693104"},{"key":"10217_CR96","doi-asserted-by":"crossref","unstructured":"Schmitz T, Algehed M, Flanagan C, Russo A (2018) Faceted secure multi execution. In: CCS \u201918","DOI":"10.1145\/3243734.3243806"},{"key":"10217_CR97","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"},{"issue":"3-4","key":"10217_CR98","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1007\/s11219-011-9152-9","volume":"20","author":"N Siegmund","year":"2012","unstructured":"Siegmund N, Rosenm\u00fcller M, Kuhlemann M, K\u00e4stner C, Apel S, Saake G (2012) SPL Conqueror: toward optimization of non-functional properties in software product lines. Softw Quality J (SQJ) 20(3-4):487\u2013517","journal-title":"Softw Quality J (SQJ)"},{"key":"10217_CR99","doi-asserted-by":"crossref","unstructured":"Smeltzer K, Erwig M (2017) Variational Lists: comparisons and design guidelines. In: ACM SIGPLAN Int. workshop on feature-oriented software development, pp 31\u201340","DOI":"10.1145\/3141848.3141852"},{"key":"10217_CR100","doi-asserted-by":"crossref","unstructured":"Tartler R, Lohmann D, Sincero J, Schr\u00f6der-Preikschat W (2011) Feature consistency in compile-time-configurable system software: facing the linux 10,000 feature problem. In: Proc. europ. conf. on computer systems (EuroSys), ACM, pp 47\u201360","DOI":"10.1145\/1966445.1966451"},{"key":"10217_CR101","doi-asserted-by":"crossref","unstructured":"Thaker S, Batory D, Kitchin D, Cook W (2007) Safe composition of product lines. In: ACM SIGPLAN conf. on generative programming and component engineering, ACM, pp 95\u2013104","DOI":"10.1145\/1289971.1289989"},{"issue":"1","key":"10217_CR102","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/2580950","volume":"47","author":"T Th\u00fcm","year":"2014","unstructured":"Th\u00fcm T, Apel S, K\u00e4stner C, Schaefer I, Saake G (2014) A classification and survey of analysis strategies for software product lines. ACM Comput Surveys 47(1):6:1\u20136:45","journal-title":"ACM Comput Surveys"},{"key":"10217_CR103","unstructured":"Tinelli C (2003) The smt-lib format: an initial proposal. https:\/\/smtlib.cs.uiowa.edu\/papers\/pdpar-proposal.pdf, Accessed 28 September 2021"},{"key":"10217_CR104","doi-asserted-by":"crossref","unstructured":"Varshosaz M, Al-Hajjaji M, Th\u00fcm T, Runge T, Mousavi MR, Schaefer I (2018) A classification of product sampling for software product lines. In: ACM SIGSOFT int. systems and software product line conf.(SPLC), ACM, pp 1\u201313","DOI":"10.1145\/3233027.3233035"},{"key":"10217_CR105","doi-asserted-by":"crossref","unstructured":"Visser W, Geldenhuys J, Dwyer MB (2012) Green: reducing, reusing and recycling constraints in program analysis. In: Proc. Int\u2019l symposium on foundations of software engineering (FSE), ACM, pp 58:1\u201358:11","DOI":"10.1145\/2393596.2393665"},{"key":"10217_CR106","unstructured":"Walkingshaw E (2013) The choice calculus: a formal language of variation. PhD thesis, Oregon State University, http:\/\/hdl.handle.net\/1957\/40652"},{"key":"10217_CR107","doi-asserted-by":"crossref","unstructured":"Walkingshaw E, K\u00e4stner C, Erwig M, Apel S, Bodden E (2014) Variational data structures: exploring trade-offs in computing with variability. In: ACM SIGPLAN Symp. on new ideas in programming and reflections on software (Onward!), pp 213\u2013226","DOI":"10.1145\/2661136.2661143"},{"key":"10217_CR108","doi-asserted-by":"publisher","unstructured":"Whittemore J, Kim J, Sakallah K (2001) Satire: A new incremental satisfiability engine. In: Proceedings of the 38th annual design automation conference, association for computing machinery, New York, DAC \u201901, pp 542\u2013545, https:\/\/doi.org\/10.1145\/378239.379019","DOI":"10.1145\/378239.379019"},{"issue":"6","key":"10217_CR109","doi-asserted-by":"publisher","first-page":"80","DOI":"10.2307\/3001968","volume":"1","author":"F Wilcoxon","year":"1945","unstructured":"Wilcoxon F (1945) Individual comparisons by ranking methods. Biometrics Bulletin 1(6):80\u201383. http:\/\/www.jstor.org\/stable\/3001968","journal-title":"Biometrics Bulletin"},{"key":"10217_CR110","volume-title":"Beyond configurable systems","author":"CP Wong","year":"2021","unstructured":"Wong CP (2021) Beyond configurable systems. Carnegie Mellon University, Applying variational execution to tackle large search spaces. PhD dissertation"},{"key":"10217_CR111","doi-asserted-by":"publisher","unstructured":"Wong CP, Meinicke J, Lazarek L, K\u00e4stner C (2018) Faster variational execution with transparent bytecode transformation. Proc ACM Program Lang 2(OOPSLA), https:\/\/doi.org\/10.1145\/3276487","DOI":"10.1145\/3276487"},{"key":"10217_CR112","unstructured":"Young J (2021) Variational Satisfiability Solving. PhD thesis, Oregon State University, https:\/\/ir.library.oregonstate.edu\/concern\/graduate_thesis_or_dissertations\/dv140182g?locale=en"},{"key":"10217_CR113","doi-asserted-by":"publisher","unstructured":"Young JM, Walkingshaw E, Th\u00fcm T (2020) Variational satisfiability solving. In: Proceedings of the 24th acm conference on systems and softwar product line: volume a - volume a, association for computing machinery, New York, SPLC \u201920, https:\/\/doi.org\/10.1145\/3382025.3414965","DOI":"10.1145\/3382025.3414965"},{"key":"10217_CR114","unstructured":"Zhang L, Madigan CF, Moskewicz MH, Malik S (2001) Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of the 2001 IEEE\/ACM international conference on computer-aided design, IEEE Press, Piscataway, NJ, USA, ICCAD \u201901, pp 279\u2013285, http:\/\/dl.acm.org\/citation.cfm?id=603095.603153"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-022-10217-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10664-022-10217-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-022-10217-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,1,10]],"date-time":"2023-01-10T03:21:03Z","timestamp":1673320863000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10664-022-10217-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,11,28]]},"references-count":114,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,1]]}},"alternative-id":["10217"],"URL":"https:\/\/doi.org\/10.1007\/s10664-022-10217-3","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"value":"1382-3256","type":"print"},{"value":"1573-7616","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,11,28]]},"assertion":[{"value":"6 July 2022","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"28 November 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"This work has been partially supported by the German Research Foundation within the project VariantSync (TH 2387\/1-1).","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}}],"article-number":"14"}}