# Reasoning Algorithms on Feature Modeling--A Systematic Mapping Study
## 2 Background
### Automated Analysis of FMs-Reasoning Algorithms  
Automatic analysis of FMs (AAFM) extracts information from such models using automated mechanisms [22]. This information includes verifying whether a given product represents a valid combination of features or checking the similarity between FMs. The analysis of FMs is an error-prone, tedious task, and it is not feasible to achieve this task manually with large-scale FMs. AAFM is an active area of research and is gaining importance for both practitioners and researchers in the SPL community [23].  
[PERSON] et al. mention that AAFM can be defined as the computer-assisted extraction of information from FMs [24]. Different proposals for extracting this information have been made, based on specific algorithms or binary decision diagrams, such as BDD, SAT, and CSP [25]. Table 1 presents a summary of these proposals.  
The process of extracting information from an FM starts with the translation of the features and relationships encoded in the FMs and any additional information into a knowledge base described in a logical paradigm [28]. Subsequently, queries to the knowledge base can be performed using solvers.These operations are performed automatically using different approaches. Most of them translate FMs into specific logical paradigms, such as propositional logic, constraint programming, and description logic [14].  
A classification of different proposals related to automatic or semi-automatic FM construction is presented in [29]. The authors of that study conceptualized an analysis  
\begin{table}
\begin{tabular}{p{113.8 pt} p{227.6 pt}} \hline \hline
**Proposal** & **Characteristics** \\ \hline Constraint Satisfaction Problem (CSP) & This consists of a set of variables, finite domains for those variables, and a set of constraints that restrict the values of the variables. It can perform most of the operations currently identified in feature models [23]. \\ \hline Boolean Satisfiability Problem (SAT) & This consists of a set of Boolean variables connected by logical operators. The SAT problem consists of deciding whether a given propositional formula satisfies whether logical values can be assigned to its variables so that the formula is true [26]. \\ \hline Binary Decision Diagrams (BDD) & A data structure is used to represent a boolean function. A BDD is an acyclic, directed, rooted graph composed of a group of decision nodes and two terminal nodes called 0-terminal and 1-terminal. Each node of the graph represents a variable in a Boolean function and has two child nodes representing an assignment of the variable to 0 and 1 [27]. \\ \hline \hline \end{tabular}
\end{table}
Table 1: Proposals to extract information from FMs.  
Figure 2: Example of an FM for a Mobile Phone SPL.  
framework for work in the field of automated FM construction. The framework considers four dimensions (proposal, input, tasks, and output) and fifteen sub-dimensions.  
Next, in Table 2, we present specific examples describing analysis operations on FMs and possible practical applications of this automation. Table 3 summarizes two relationships of FMs (mandatory and optional), depicting their representation using _propositional logic (PL)_ and _constraint programming (CP)_, and examples of their application using the Mobile Phone SPL example presented in Figure 2. A detailed compilation of operations, formal definitions, and solution proposals can be seen in [14; 23; 28]. Finally, a synthesis of FM data extraction process can be seen in Figure 3.