Feature-Model Counting

In this project, we work on the following aspects of feature-model analysis related to computing the number of valid configuration:

  1. Gather use-case scenarios for feature-model counting
  2. Identify scalable solutions for computing the number of valid configurations
  3. Optimize and tailor existing solutions for the application on feature models
  4. Develop new algorithms and tools to support analysis

Motivation

Feature-model counting enables a large variety of analyses. These range from simple analyses, such as prioritizing errors that appear in more valid configurations, to more complex computations such as finding a uniformly distributed sample of configurations.

Model Counting aka #SAT

The #SAT problem corresponds to computing the number of satisfying assignments of a propositional formula. By translating a feature model to a formula, we can reduce computing the number of valid configurations to a #SAT problem. This allows the usage of heavily optimized tools, #SAT solvers, that have made significant advances in the last decade. Nevertheless, we have seen feature models in the wild that cannot be analyzed within weeks of runtime.

Team Members

Student Members, Workers, and Projecteers

Publications & Theses

Publications

2021

2.
C. Sundermann, M. Nieke, P. M. Bittner, T. Heß, T. Thüm and I. Schaefer, "Applications of #SAT Solvers on Feature Models" in Proc. Int'l Working Conf. on Variability Modelling of Software-Intensive Systems (VaMoS), New York, NY, USA: ACM, Feb. 2021.
DOI:10.1145/3442391.3442404
ISBN:9781450388245
Datei:pdfhttps://github.com/SoftVarE-Group/Papers/raw/master/2021/2021-VaMoS-Sundermann.pdf

2020

1.
C. Sundermann, T. Thüm and I. Schaefer, "Evaluating #SAT Solvers on Industrial Feature Models" in Proc. Int'l Working Conf. on Variability Modelling of Software-Intensive Systems (VaMoS), New York, NY, USA: ACM, Feb. 2020.
DOI:10.1145/3377024.3377025
ISBN:9781450375016
Datei:pdfhttps://github.com/SoftVarE-Group/Papers/raw/master/2020/2020-VaMoS-Sundermann.pdf

Theses

2022

2.
D. Schiessl, "An Incremental #SAT Solver for Efficient Analysis of Feature Models", Master's Thesis, University of Ulm, Germany, Jan. 2022.
1.
H. Raab, "Exploiting d-DNNFs for Efficient Cardinality-Based Feature-Model Analyses", Bachelor's Thesis, University of Ulm, Germany, Jan. 2022.

Project Lead