SAT-based analysis of feature models is easy

340 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Model checking lots of systems: efficient verification of temporal properties in software product lines (2010, methodology): “A straightforward and efficient implementation of this check can be done with a SAT solver [27].”
Automated analysis of feature models 20 years later: A literature review (2010, methodology): “[57, 56] defines theExtra Constraint Representativeness (ECR) as the ratio of the number of features involved in crosstree constraints (repeated features counted once) to the number of features in the feature tree.”
An Overview of Feature-Oriented Software Development (2009, methodology): “For example, binary decision diagrams [94], satisfiability solvers [93], constraint satisfaction solvers [32], or simplified reasoning [122] were used to reason about feature models of up to 10 000 features.”
Feature-Oriented Software Product Lines (2013, background): “Despite exponential worst-case complexity, researchers have empirically shown that modern SAT solvers can solve practical Boolean satisfiability problems quickly in the context of feature-model analysis, even for very large feature models (Mendonça et al. 2009).”
S.P.L.O.T.: software product lines online tools (2009, methodology): “As well, the system capitalizes on the observed efficiency of SAT systems in the feature modeling domain [12] to provide high-performance SAT-based algorithms (e.”