Applications of #SAT Solvers for Product Lines : Master's Thesis
Product lines are widely used for managing families of similar products. Typically, product lines are complex and infeasible to analyze manually. In the last two decades, product-line analyses have been reduced to satisfiability problems which are well understood. However, there are methods for which satisfiability is not sufficient. Recently, researchers begun to reduce other problems to #SAT. Yet, only few applications have been considered and those are fairly limited in their scope. Furthermore, the authors mainly propose ad-hoc solutions that are only applicable under certain restrictions or do not scale to large product lines. In this thesis, we aim show the benefits of applying #SAT for the analysis of product lines. To this end, we make the following contributions: First, we summarize applications dependent on #AT considered in the literature and propose new applications to motivate the usage of #SAT technology. Second, we present a variety of algorithms and optimizations for these applications including new proposals. Third, we empirically evaluate 10 proposed algorithms with 14 off-the-shelf #SAT solvers on 131 industrial feature models to identify the fastest algorithms and solvers. Our results show that for each analysis at least one algorithm and solver scale on a vast majority of the feature models, whereas Linux and an automotive model not be analyzed at all. In addition, our results further reveal the benefits of knowledge compilation to deterministic decomposable negation normal form for performing counting-based analyses. Overall, our work shows that #SAT dependent analyses for feature models open a new variety of different applications and scale to a large number of industrial feature models.
Produktlinien sind weit verbreitet für die Verwaltung von Familien verwandter Pro-
dukte. In der Regel sind Produktlinien komplex und manuell schwer zu analysieren.
In den letzten zwei Jahrzehnten wurden Produktlinienanalysen auf Erfüllbarkeit-
sprobleme reduziert, für welche es eine Vielzahl an effizienten Werkzeugen gibt.
Allerdings ist Erfüllbarkeit nicht für alle Analysen hinreichend. Kürzlich haben
Forscher damit begonnen, andere Probleme auf #SAT zu reduzieren. Es wur-
den jedoch nur wenige Anwendungen in Betracht gezogen und auch der Anwen-
dungsbereich ist begrenzt. Darüber hinaus schlagen die Autoren hauptsächlich
Ad-hoc-Lösungen vor, die nur unter bestimmten Einschränkungen der Produktlin-
ien anwendbar sind oder nicht für große Produktlinien skalieren. In dieser Arbeit
zeigen wir die Vorteile von #SAT Anwendungen für Produtlinien auf. Unser wis-
senschaftlicher Beitrag besteht aus den folgenden drei Punkten: Zuerst fassen wir
die in der Literatur betrachteten #SAT-Anwendungen zusammen und schlagen neue
Anwendungen vor, um den Einsatz von #SAT-Technologien zu motivieren. Zweit-
ens stellen wir eine Vielzahl von Algorithmen und Optimierungen für diese Anwen-
dungen vor, einschließlich neuer Vorschläge. Drittens führen wir eine empirische
Evaluation von 10 der vorgeschlagenen Algorithmen mit 14 #SAT-Solvern auf 131
industriellen Feature-Modellen aus, um die schnellsten Algorithmen und Solver zu
identifizieren. Die Ergebnisse der Evaluation zeigen, dass wir für jede Analyse wenig-
stens einen Algorithmus und Solver identifiziert haben, die für industrielle Feature-
Modelle skalieren. Dazu sind die Ergebnisse ein starker Indikator für die Vorteile
des Einsatzes von d-DNNFs bei #SAT-Anwendungen. Insgesamt zeigt unsere Ar-
beit, dass #SAT-abhängige Analysen für Feature-Modelle eine Vielzahl neuer un-
terschiedlicher Anwendungen ermöglicht und für viele industirelle Feature-Modelle
skaliert.