English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Zendy Plus

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Zendy Tools

Zendy Open

Modern conflict-driven clause-learning (CDCL) Boolean SAT solvers provideefficient automatic analysis of real-world feature models (FM) of systemsranging from cars to operating systems. It is well-known that solver-basedanalysis of real-world FMs scale very well even though SAT instances obtainedfrom such FMs are large, and the corresponding analysis problems are known tobe NP-complete. To better understand why SAT solvers are so effective, wesystematically studied many syntactic and semantic characteristics of arepresentative set of large real-world FMs. We discovered that a key reason whylarge real-world FMs are easy-to-analyze is that the vast majority of thevariables in these models are unrestricted, i.e., the models are satisfiablefor both true and false assignments to such variables under the current partialassignment. Given this discovery and our understanding of CDCL SAT solvers, weshow that solvers can easily find satisfying assignments for such modelswithout too many backtracks relative to the model size, explaining why solversscale so well. Further analysis showed that the presence of unrestrictedvariables in these real-world models can be attributed to their high-degree ofvariability. Additionally, we experimented with a series of well-knownnon-backtracking simplifications that are particularly effective in solvingFMs. The remaining variables/clauses after simplifications, called the core,are so few that they are easily solved even with backtracking, furtherstrengthening our conclusions.

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