publication . Preprint . 2015

SAT-based Analysis of Large Real-world Feature Models is Easy

Liang, Jia Hui; Ganesh, Vijay; Raman, Venkatesh; Czarnecki, Krzysztof;
Open Access English
  • Published: 17 Jun 2015
Abstract
Modern conflict-driven clause-learning (CDCL) Boolean SAT solvers provide efficient automatic analysis of real-world feature models (FM) of systems ranging from cars to operating systems. It is well-known that solver-based analysis of real-world FMs scale very well even though SAT instances obtained from such FMs are large, and the corresponding analysis problems are known to be NP-complete. To better understand why SAT solvers are so effective, we systematically studied many syntactic and semantic characteristics of a representative set of large real-world FMs. We discovered that a key reason why large real-world FMs are easy-to-analyze is that the vast majorit...
Subjects
free text keywords: Computer Science - Software Engineering, Computer Science - Artificial Intelligence
Download from
20 references, page 1 of 2

[1] A. Balint, A. Belov, M. Ja¨rvisalo, and C. Sinz. Overview and analysis of the SAT Challenge 2012 solver competition. Artificial Intelligence, 223:120-155, 2015.

[2] D. Batory. Feature models, grammars, and propositional formulas. In Proceedings of the 9th International Conference on Software Product Lines, SPLC'05, pages 7-20, Berlin, Heidelberg, 2005. Springer-Verlag. [OpenAIRE]

[3] D. Benavides, S. Segura, and A. Ruiz-Cort´es. Automated analysis of feature models 20 years later: A literature review. Information Systems, 35(6):615 - 636, 2010. [OpenAIRE]

[4] D. Benavides, S. Segura, P. Trinidad, and A. Ruiz-Cort´es. A first step towards a framework for the automated analysis of feature models. In Managing Variability for Software Product Lines: Working With Variability Mechanisms, 2006. [OpenAIRE]

[5] T. Berger, R.-H. Pfeiffer, R. Tartler, S. Dienst, K. Czarnecki, A. Wasowski, and S. She. Variability mechanisms in software ecosystems. Information and Software Technology, 56(11):1520-1535, 2014.

[6] T. Berger, R. Rublack, D. Nair, J. M. Atlee, M. Becker, K. Czarnecki, and A. Wasowski. A survey of variability modeling in industrial practice. In Proceedings of the Seventh International Workshop on Variability Modelling of Software-intensive Systems, VaMoS '13, pages 7:1-7:8, New York, NY, USA, 2013. ACM. [OpenAIRE]

[7] T. Berger, S. She, R. Lotufo, A. Wasowski, and K. Czarnecki. Variability modeling in the real: A perspective from the operating systems domain. In Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, ASE '10, pages 73-82, New York, NY, USA, 2010. ACM.

[8] T. Berger, S. She, R. Lotufo, A. Wasowski, and K. Czarnecki. A study of variability models and languages in the systems software domain. IEEE Trans. Softw. Eng., 39(12):1611-1640, Dec. 2013.

[9] K. Czarnecki and U. W. Eisenecker. Generative Programming: Methods, Tools, and Applications. ACM Press/Addison-Wesley Publishing Co., New York, NY, USA, 2000.

[10] R. Gheyi, T. Massoni, and P. Borba. A theory for feature models in Alloy. pages 71-80, Portland, USA, November 2006.

[11] M. Janota. Do SAT solvers make good configurators? In SPLC (2), pages 191-195, 2008.

[12] K. C. Kang, S. G. Cohen, J. A. Hess, W. E. Novak, and A. S. Peterson. Feature-oriented domain analysis (FODA) feasibility study. Technical report, Carnegie-Mellon University Software Engineering Institute, November 1990.

[13] H. Katebi, K. A. Sakallah, and J. a. P. Marques-Silva. Empirical study of the anatomy of modern SAT solvers. In Proceedings of the 14th International Conference on Theory and Application of Satisfiability Testing, SAT'11, pages 343-356, Berlin, Heidelberg, 2011. Springer-Verlag.

[14] D. Le Berre, A. Parrain, M. Baron, J. Bourgeois, Y. Irrilo, F. Fontaine, F. Laihem, O. Roussel, and L. Sais. Sat4j-a satisfiability library for java, 2006.

[15] R. Mateescu. Treewidth in industrial SAT benchmarks. Technical report, Microsoft Research, 2011.

20 references, page 1 of 2
Related research
Abstract
Modern conflict-driven clause-learning (CDCL) Boolean SAT solvers provide efficient automatic analysis of real-world feature models (FM) of systems ranging from cars to operating systems. It is well-known that solver-based analysis of real-world FMs scale very well even though SAT instances obtained from such FMs are large, and the corresponding analysis problems are known to be NP-complete. To better understand why SAT solvers are so effective, we systematically studied many syntactic and semantic characteristics of a representative set of large real-world FMs. We discovered that a key reason why large real-world FMs are easy-to-analyze is that the vast majorit...
Subjects
free text keywords: Computer Science - Software Engineering, Computer Science - Artificial Intelligence
Download from
20 references, page 1 of 2

[1] A. Balint, A. Belov, M. Ja¨rvisalo, and C. Sinz. Overview and analysis of the SAT Challenge 2012 solver competition. Artificial Intelligence, 223:120-155, 2015.

[2] D. Batory. Feature models, grammars, and propositional formulas. In Proceedings of the 9th International Conference on Software Product Lines, SPLC'05, pages 7-20, Berlin, Heidelberg, 2005. Springer-Verlag. [OpenAIRE]

[3] D. Benavides, S. Segura, and A. Ruiz-Cort´es. Automated analysis of feature models 20 years later: A literature review. Information Systems, 35(6):615 - 636, 2010. [OpenAIRE]

[4] D. Benavides, S. Segura, P. Trinidad, and A. Ruiz-Cort´es. A first step towards a framework for the automated analysis of feature models. In Managing Variability for Software Product Lines: Working With Variability Mechanisms, 2006. [OpenAIRE]

[5] T. Berger, R.-H. Pfeiffer, R. Tartler, S. Dienst, K. Czarnecki, A. Wasowski, and S. She. Variability mechanisms in software ecosystems. Information and Software Technology, 56(11):1520-1535, 2014.

[6] T. Berger, R. Rublack, D. Nair, J. M. Atlee, M. Becker, K. Czarnecki, and A. Wasowski. A survey of variability modeling in industrial practice. In Proceedings of the Seventh International Workshop on Variability Modelling of Software-intensive Systems, VaMoS '13, pages 7:1-7:8, New York, NY, USA, 2013. ACM. [OpenAIRE]

[7] T. Berger, S. She, R. Lotufo, A. Wasowski, and K. Czarnecki. Variability modeling in the real: A perspective from the operating systems domain. In Proceedings of the IEEE/ACM International Conference on Automated Software Engineering, ASE '10, pages 73-82, New York, NY, USA, 2010. ACM.

[8] T. Berger, S. She, R. Lotufo, A. Wasowski, and K. Czarnecki. A study of variability models and languages in the systems software domain. IEEE Trans. Softw. Eng., 39(12):1611-1640, Dec. 2013.

[9] K. Czarnecki and U. W. Eisenecker. Generative Programming: Methods, Tools, and Applications. ACM Press/Addison-Wesley Publishing Co., New York, NY, USA, 2000.

[10] R. Gheyi, T. Massoni, and P. Borba. A theory for feature models in Alloy. pages 71-80, Portland, USA, November 2006.

[11] M. Janota. Do SAT solvers make good configurators? In SPLC (2), pages 191-195, 2008.

[12] K. C. Kang, S. G. Cohen, J. A. Hess, W. E. Novak, and A. S. Peterson. Feature-oriented domain analysis (FODA) feasibility study. Technical report, Carnegie-Mellon University Software Engineering Institute, November 1990.

[13] H. Katebi, K. A. Sakallah, and J. a. P. Marques-Silva. Empirical study of the anatomy of modern SAT solvers. In Proceedings of the 14th International Conference on Theory and Application of Satisfiability Testing, SAT'11, pages 343-356, Berlin, Heidelberg, 2011. Springer-Verlag.

[14] D. Le Berre, A. Parrain, M. Baron, J. Bourgeois, Y. Irrilo, F. Fontaine, F. Laihem, O. Roussel, and L. Sais. Sat4j-a satisfiability library for java, 2006.

[15] R. Mateescu. Treewidth in industrial SAT benchmarks. Technical report, Microsoft Research, 2011.

20 references, page 1 of 2
Related research
Powered by OpenAIRE Open Research Graph
Any information missing or wrong?Report an Issue