# Parameterised Enumeration for Modification Problems +
## 4 Generalisation to Modification Problems
### Backdoors  
In this section, we will consider the concept of backdoors. Let \(\mathcal{C}\) be a class of propositional formulas. Intuitively, a \(\mathcal{C}\) backdoor is a set of variables of a given propositional formula with the following property. Applying assignments over these variables to the formula always yields a formula in the class \(\mathcal{C}\). Of course, one aims for formula classes for which satisfiability can be decided efficiently. Informally speaking, with the parameter backdoor size of a formula one tries to describe a distance to tractability. This definition was first introduced by [PERSON], [PERSON] and [PERSON] [18] to model short distances to efficient subclasses. Until today, backdoors gained copious attention in many differentareas: abduction [33], answer set programming [34; 35], argumentation [36], default logic [37], temporal logic [38], planning [39] and constraint satisfaction [40; 41]. Consider a formula \(\phi\) in conjunctive normal form. Denote by \(\phi[\tau]\) for a partial truth assignment \(\tau\) the result of removing all clauses from \(\phi\) which contain a literal \(\ell\) with \(\tau(\ell)=1\) and removing literals \(\ell\) with \(\tau(\ell)=0\) from the remaining clauses. Definition 14: Let \(\mathcal{C}\) be a class of CNF formulas and \(\phi\) be a CNF formula. A set \(V\subseteq\mathit{Vars}(\phi)\) of variables of \(\phi\) is a strong \(\mathcal{C}\) backdoor set of \(\phi\) if for all truth assignments \(\tau\colon V\to\{0,1\}\) we have that \(\phi[\tau]\in\mathcal{C}\). Definition 15 ([42; 43]): Let \(\mathcal{C}\) be a class of CNF formulas and \(\phi\) be a CNF formula. A set \(V\subseteq\mathit{Vars}(\phi)\) of variables of \(\phi\) is a \(\mathcal{C}\)-deletion backdoor set of \(\phi\) if \(\phi[V]\) is in \(\mathcal{C}\), where \(\phi[V]\) denotes the formula obtained from \(\phi\) by deleting in \(\phi\) all occurrences of variables from \(V\). Definition 16 (Weak Backdoor Sets): Let \(\mathcal{C}\) be a class of CNF formulas and \(\phi\) be a propositional CNF formula. A set \(V\subseteq\mathit{Vars}(\phi)\) of variables from \(\phi\) is a weak \(\mathcal{C}\) backdoor set of \(\phi\) if there exists an assignment \(\theta\in\Theta(V)\) such that \(\phi[\theta]\in\mathcal{C}\) and \(\phi[\theta]\) is satisfiable. Now let us consider the following enumeration problem. \begin{tabular}{l l} \hline \hline
**Problem:** & Enum-Weak-BackDoorSet\((\mathcal{C})\) \\ \hline
**Input:** & A formula \(\phi\) in CNF, \(k\in\mathbb{N}\). \\
**Parameter:** & The integer \(k\). \\
**Output:** & The set of all weak \(\mathcal{C}\) backdoor sets of \(\phi\) of size at most \(k\). \\ \hline \hline \end{tabular}   
Similarly, define Enum-Strong-BackDoorSet\((\mathcal{C})\) for the set of all strong \(\mathcal{C}\) backdoor sets of \(\phi\) of size at most \(k\). Observe that the backdoor set problems can be seen as modification problems where solutions are sequences of variable assignments. The target property then simply is the class of CNF formulas \(\mathcal{C}\). Notice that [PERSON] et al. [13] (Theorem 4), have studied enumeration for exact strong HORNbackdoor sets and provided an algorithm running in DelayFPT, where HORN denotes the set of all Horn formulas, that is, CNF formulas whose clauses contain at most one positive literal. Definition 17 (Base Class [44]): The class \(\mathcal{C}\) is a base class if it can be recognised in \(\mathrm{P}\) (that is, \(\mathcal{C}\in\mathrm{P}\)), the satisfiability of its formulas is in \(\mathrm{P}\) and the class is closed under isomorphisms w.r.t. variable names. We say that \(\mathcal{C}\) is clause defined if for every CNF formula \(\phi\) we have: \(\phi\in\mathcal{C}\) if and only if \(\{\mathcal{C}\}\in\mathcal{C}\) for all clauses \(\mathcal{C}\) from \(\phi\).