Backdoors into Two Occurrences

Abstract

Backdoor sets for the class CNF(2) of CNF-formulas in which every variable has at most two occurrences are studied in terms of parameterized complexity. The question whether there exists a CNF(2)-backdoor set of size k is hard for the class $W [2]$ , for both weak and strong backdoors, and in both cases it becomes fixed-parameter tractable when restricted to inputs in d-CNF for a fixed d.

Besides that, it is shown that the problem of finding weak backdoor sets is $W [2]$ -complete, for certain tractable cases. These are the first completeness results in lower levels of the $W$ -hierarchy for any backdoor set problems.

Keywords

Backdoor set fixed-parameter tractability parameterized complexity completeness formulas with two variable occurrences

1. Introduction

Despite the theoretical hardness of the SAT problem, being the canonical NP-complete problem [1] and conjectured to not be solvable in sub-exponential time [6], state-of-the-art SAT solvers have become very efficient, and routinely solve instances arising from applications with hundreds of thousands of variables and millions of clauses. Even though there are lots of known tractable cases of SAT, i.e., classes of formulas that can be solved in polynomial time, the efficiently solvable instances arising in practice usually do not belong to these tractable classes, and thus the existence of these classes does not suffice to explain this apparent discrepancy between theory and practice.

A possibly better attempt at explaining the discrepancy is that the large, efficiently solvable instances are in some way close to a tractable case. One possible such notion of closeness is that there is a small subset of variables, such that after giving values to these variables the residual formula is in the tractable class. This concept was introduced by Crama et al. [2] and Williams et al. [13], the latter work coined the name backdoor set for such a set of variables.

There are several kinds of backdoor sets for each tractable case considered in the literature. A strong backdoor set for the class C is a set of variables, such that for every setting of these variables the residual formula is in C. A weak backdoor set for C is a set of variables, such that for some setting of these variables the residual formula is in C and satisfiable. There is also the auxiliary notion of a deletion backdoor set to be defined below.

A strong backdoor set of size k allows to solve a formula of size m in time $2^{k} \cdot m^{O (1)}$ . This runtime bound depends on the two parameters (size of the formula m and backdoor set size k) in essentially different ways, and the proper framework to analyze such complexity bounds is fixed-parameter tractability and parameterized complexity as introduced by Downey and Fellows [3].

Besides the class of fixed-parameter tractable problems, the theory of parameterized complexity provides a hierarchy of classes of increasingly hard problems that are probably fixed-parameter intractable, the $W$ -hierarchy containing in particular the classes $W [t]$ for $t \in N$ , and a notion of reduction that allows to define hardness and completeness for these classes.

The complexity bound mentioned above thus means that given a formula together with a strong backdoor set of size k, testing for satisfiability is fixed-parameter tractable w.r.t. the parameter k. Thus, if the problem of finding a backdoor set of size k was fixed-parameter tractable w.r.t. the parameter k as well, then the size of a smallest backdoor set would be a parameter with respect to which SAT is fixed-parameter tractable. Thus, starting with the work of Nishimura et al. [11], the parameterized complexity of finding backdoor sets was determined for various tractable cases, most of the results in that direction are collected in the recent survey by Gaspers and Szeider [5].

A less well-known tractable case is the class $CNF (2)$ of $CNF$ -formulas in which every variable has at most two occurrences. The satisfiability problem for these formulas can be solved in linear time [9], and it has been shown to be complete for deterministic logarithmic space [8].

In this work, we determine the parameterized complexity of finding backdoor sets w.r.t. the class $CNF (2)$ . We show that the problem is hard for the class $W [2]$ , for both weak and strong backdoor sets, and that in both cases it becomes fixed-parameter tractable when restricted to inputs in $d - CNF$ for a fixed d.

For those tractable cases where the problem of finding backdoor sets is $W [2]$ -hard, including $CNF (2)$ , the smallest parameterized complexity class known to contain the problem is $W [P]$ , which lies higher up in the $W$ -hierarchy, beyond the classes $W [t]$ . For the tractable cases of 0-valid and 1-valid formulas, we show that the weak backdoor set problem is complete for $W [2]$ . To the best of our knowledge, these are the first completeness results in the $W$ -hierarchy for any weak backdoor set problems.

In order prove this latter result, we study a related artificial problem of finding so-called very weak backdoor sets, whose definition differs from that of weak backdoor sets by weakening the condition that the residual formula has to be satisfiable. We show that the problem of finding very weak backdoor sets for these classes is in $W [2]$ , by utilizing the characterization of the $W$ -hierarchy in terms of first-order logic definability. The method also allows us to put the very weak backdoor set problem for other tractable cases into the class $W [2]$ , including the class $CNF (2)$ .

The paper is structured as follows: in Section 2 we review the necessary background on the problem SAT and its tractable cases, in particular the class $CNF (2)$ , on parameterized complexity and on backdoor sets. Section 3 treats some general properties of $CNF (2)$ -backdoor sets. In Section 4 we show the results about weak $CNF (2)$ -backdoor sets, and in Section 5 those about strong $CNF (2)$ -backdoor sets. Finally Section 6 presents the mentioned upper bounds in the $W$ -hierarchy.

2. Preliminaries

We briefly review basic notions about the propositional satisfiability problem, mainly to fix the notation.

A literal is a variable x or a negated variable $\bar{x}$ . A clause is a disjunction $C = a_{1} \lor \dots \lor a_{d}$ of literals $a_{i}$ . The width $w (C)$ of C is d, the number of literals in C. We identify a clause with the set of literals occurring in it, even though for clarity we still write it as a disjunction.

A formula in conjunctive normal form ( $CNF$ ) is a conjunction $F = C_{1} \land \dots \land C_{m}$ of clauses, it is usually identified with the set of clauses ${C_{1}, \dots, C_{m}}$ . A formula F in $CNF$ is in $d - CNF$ if every clause C in F is of width $w (C) ⩽ d$ .

A restriction α is a partial assignment $α : V \to {0, 1}$ from the set of variables V to the truth values ${0, 1}$ . A restriction α is extended to literals by setting $α (\bar{x}) : = 1 - α (x)$ . We occasionally identify a restriction α with the set of literals it sets, i.e., ${a; α (a) = 1}$ .

For a clause C over the variables V, we define $C ⌈ α = 1$ if $α (a) = 1$ for some literal $a \in C$ , and otherwise $C ⌈ α$ is the disjunction of those literals $a \in C$ for which $α (a) = 0$ does not hold, i.e., which are left unset by α. Here the empty disjunction is identified with the constant 0.

For a $CNF$ -formula F over V, we define $F ⌈ α = 0$ if $C ⌈ α = 0$ for some $C \in F$ , and otherwise $F ⌈ α$ is the conjunction of the clauses $C ⌈ α$ for those clauses $C \in F$ for which $C ⌈ α = 1$ is not the case. Here the empty conjunction is identified with the constant 1.

In other words, the formula $F ⌈ α$ is obtained by deleting clauses satisfied by α from F, and deleting literals falsified by α from the remaining clauses in F.

For $𝜖 = 0, 1$ , we denote by $[x : = 𝜖]$ the restriction setting the variable x to 𝜖. This notation is also extended to literals by letting $[\bar{x} : = 𝜖]$ denote $[x : = (1 - 𝜖)]$ .

If $F ⌈ α = 1$ , then we say that α satisfies F and write $α ⊧ F$ . The satisfiability problem SAT is the decision problem: Instance:

Formula F in $CNF$ .

Question:

Is there a restriction α with $α ⊧ F$ ?

This problem SAT is the canonical NP-complete problem [1], and the strong exponential time hypothesis [6] is a widely-believed conjecture that implies that SAT is not solvable in sub-exponential time.

A clause C is tautological, if both x and $\bar{x}$ occur in C for some variable x. Since tautological clauses are satisfied by all restrictions of their variables, they are irrelevant for the satisfiability of a formula they appear in. Therefore, SAT and other related problems are often restricted to formulas that do not contain any tautological clauses. Except when noted, all our results hold for problems restricted in this way.

2.1. Tractable Cases of SAT

Despite its hardness, many easy special cases of the problem SAT have been identified. A tractable case of SAT, sometimes also called an “island of tractability”, is a class of $CNF$ -formulas such that

membership $F \in C$ can be decided in polynomial time,

the satisfiability problem for formulas $F \in C$ can be decided in polynomial time.

Many tractable cases of SAT have been defined and studied in the literature, some well-known examples of such classes are, e.g., the following:

The class $H ORN$ of Horn formulas, i.e., formulas in which every clause contains at most one positive literal.

The class $CO -H ORN$ of formulas in which every clause contains at most one negative literal.

The class $2 - CNF$ of formulas in which every clause is of width at most 2.

The class 1-Val of formulas where every clause contains at least one positive literal.

The class 0-Val of formulas where every clause contains at least one negative literal.

Note that formulas from the latter two classes are trivially satisfiable by the assignment setting every variable to 1 (resp., 0).

All the above tractable cases are defined by properties of the individual clauses in the formula, and by the classification result of Schaefer [12], these are the only maximal such classes of $CNF$ formulas.

A different tractable class which is not defined by properties of clauses is the class of cluster formulas [7,10]. Two clauses C and $C^{'}$ clash if they contain complementary literals, i.e. if $a \in C$ and $\bar{a} \in C^{'}$ for some literal a. A formula F is a hitting formula if any two different clauses in F clash. The class $C LU$ of cluster formulas is the class of $CNF$ -formulas that are variable-disjoint unions of hitting formulas.

Another less well-known tractable class is the class $CNF (2)$ of formulas with at most two occurrences of every variable – in a way a dual to $2 - CNF$ . It is known that satisfiability of formulas in $CNF (2)$ can be tested in linear time [9] and in logarithmic space – in fact it is complete for the class of problems solvable in deterministic logarithmic space [8].

2.2. Parameterized Complexity

We briefly review the basic concepts of parameterized complexity as used in this work, mostly following the textbook of Flum and Grohe [4].

A parameterized problem is a decision problem P together with a parameterization, i.e., a polynomial time computable mapping that associates with every instance x of P a parameter $k = k (x) \in N$ . We denote by $n = n (x) \in N$ the size of an instance, the number of bits required to represent x.

A parameterized problem P with parameter k is fixed-parameter tractable if there is an algorithm that solves P in time $f (k) \cdot O (n^{d})$ for some computable function f and $d \in N$ . The class of parameterized problems that are fixed-parameter tractable is called $FPT$ .

An $FPT$ -reduction between parameterized problems P and $P^{'}$ with parametrizations k and $k^{'}$ , resp., is a function r mapping instances of P to instances of $P^{'}$ such that

r is computable in $FPT$ -time $f (k) \cdot O (n^{d})$ for some computable function f and $d \in N$ ,

$r (x)$ is a positive instance of $P^{'}$ iff x is a positive instance of P,

there is a computable function g s.t. for every instance x of P we have $k^{'} (r (x)) ⩽ g (k (x))$ .

For a first-order formula $φ (X)$ with a free relation variable X of arity d, the parameterized problem $W D (φ)$ is the following: Instance:

Structure A for the language of φ, $k \in N$ .

Parameter:

Question:

Is there a relation $R \subseteq A^{d}$ of size $| R | ⩽ k$ with $A ⊧ φ (R)$ ?

A first-order formula is a

Π_{t}

-formula if it has at most t alternations of quantifiers, with the outermost quantifier being universal. A

Σ_{t}

-formula has at most t alternations of quantifiers, with the outermost one an existential. The class

W [t]

is the class of parameterized problems that are

FPT

-reducible to some problem

W D (φ)

for a

Π_{t}

-formula

φ (X)

The parameterized problem Weighted Circuit SAT is: Instance:

Boolean circuit C, $k \in N$ .

Parameter:

Question:

Is there a satisfying assignment $α ⊧ C$ with $| {x; α (x) = 1} | ⩽ k$ ?

The class

W [P]

is the class of parameterized problems that are

FPT

-reducible to Weighted Circuit SAT. Since restricted forms of Weighted Circuit SAT (for circuits of constant depth and weft t, see [3]) are complete for the classes

W [t]

, we have that

\begin{matrix} FPT \subseteq W [1] \subseteq W [2] \subseteq \dots \subseteq W [t] \subseteq \dots \subseteq W [P] . \end{matrix}

The parameterized problem Hitting Set is the following :

Instance:

Family ${S_{1}, \dots, S_{m}}$ of subsets $S_{i} \subseteq U$ , $k \in N$ .

Parameter:

Question:

Is there a set $H \subseteq U$ of size $| H | ⩽ k$ with $H \cap S_{i} \neq \emptyset$ for every i?

Hitting Set is one of the canonical

W [2]

-complete problems. To see that it is in

W [2]

, view an instance as a structure with unary predicates

U (x)

for the elements of U, and

set (x)

for the sets

S_{i}

, and the element relation ∈ between elements of U and sets. Then Hitting Set is the problem

W D (φ)

for the following

Π_{2}

-formula

φ (X)

with a unary relation variable X:

\begin{matrix} φ (X) \equiv \forall x (set (x) \to \exists y (U (y) \land X (y) \land x \in y)) . \end{matrix}

2.3. Backdoor Sets

Let F be a $CNF$ -formula in the variables V, and let C be a tractable case of SAT. Let $X \subseteq V$ be a set of variables. The formula $F ∖ X$ is the formula obtained by deleting from the clauses in F all occurrences of literals x and $\bar{x}$ for $x \in X$ .

A strong C-backdoor set for F is a subset $X \subseteq V$ such that for every assignment $α : X \to {0, 1}$ , the formula $F ⌈ α$ is in C.

A weak C-backdoor set for F is a subset $X \subseteq V$ such that there is an assignment $α : X \to {0, 1}$ such that the formula $F ⌈ α$ is in C and satisfiable.

A deletion C-backdoor set for F is a subset $X \subseteq V$ such that the formula $F ∖ X$ is in C.

If the class C is closed under subsets, then every deletion backdoor set is also a strong backdoor set, since

F ⌈ α \subseteq F ∖ X

for every

α : X \to {0, 1}

. This fact is useful since deletion backdoor sets are usually easier to find than strong backdoor sets. For classes C that are also closed under unions, strong and deletion backdoor sets coincide, since

F ∖ X = ⋃_{α} F ⌈ α

where the union is over all

α : X \to {0, 1}

The parameterized problem Strong C -Backdoor Set is: Instance:

$CNF$ -formula F, and $k \in N$ .

Parameter:

Question:

Is there a strong C-backdoor set for F of size k?

The problems Weak C -Backdoor Set and Deletion C -Backdoor Set are defined analogously.

The parameterized complexity of these problems for various tractable classes of formulas has been determined in the literature. For the classes $C = H ORN$ , $CO -H ORN$ , $2 - CNF$ , $1 -V AL$ and $0 -V AL$ , the problem Strong C -Backdoor Set is fixed parameter tractable. Since these classes are defined by properties of individual clauses, they are closed under subsets and unions, so the problem is the same as Deletion C -Backdoor Set, which is easily seen to be fixed parameter tractable in these cases.

The problem Weak C -Backdoor Set for all of these classes, on the other hand, is $W [2]$ -hard, but fixed parameter tractable when the input is restricted to formulas in $d - CNF$ for a fixed $d \in N$ . For the class of cluster formulas, both problems Strong $C LU$ -Backdoor Set and Weak $C LU$ -Backdoor Set are $W [2]$ -hard, but are in $FPT$ when restricted to inputs in $d - CNF$ . These results, together with many more results for other tractable cases, can be found in a recent survey by Gaspers and Szeider [5].

3. Backdoors into $CNF (2)$

Since the class $CNF (2)$ is obviously not closed under unions, deletion and strong backdoor sets do not necessarily coincide for this class. This is actually not the case, as the following example shows. Consider the following set of clauses: $\begin{matrix} (x_{1} \lor x_{2} \lor {\bar{x}}_{3}), ({\bar{x}}_{1} \lor x_{2} \lor x_{5}), ({\bar{x}}_{1} \lor {\bar{x}}_{3} \lor {\bar{x}}_{5}), ({\bar{x}}_{2} \lor x_{4}), (x_{3} \lor {\bar{x}}_{4}) . \end{matrix}$ The variables ${x_{1}, x_{2}, x_{3}}$ occur three times each, so the smallest deletion $CNF (2)$ -backdoor set has size 3. But ${x_{1}}$ is a strong $CNF (2)$ -backdoor set, showing that strong backdoors can be smaller than deletion backdoors for this class.

For the base class $CNF (2)$ , it matters whether formulas are represented as multisets, with multiple occurrences of the same clause allowed, or as sets, since the number of occurrences of variables is counted differently in both cases.

If formulas are represented as multisets, then the smallest deletion $CNF (2)$ -backdoor set is exactly the set of variables with more than two occurrences, hence we trivially have:

Proposition 1.
For formulas represented as multisets, the problem Deletion $CNF (2)$ -Backdoor Set can be solved in linear time.

On the other hand, for formulas represented as sets, clauses can become equal – and hence identified – if literals are deleted or set to 0. To show that this actually makes a difference note the following proposition.
Proposition 2.
For formulas represented as sets, the problem Deletion $CNF (2)$ -Backdoor Set is $NP$ -hard.

Proof:We reduce the well-known $NP$ -hard problem Vertex Cover to Deletion $CNF (2)$ -Backdoor Set. For a graph $G = (V, E)$ , define a formula $F = F (G)$ as follows: F has variables $x_{v} \in V$ for v, and for every edge ${u, v}$ a subformula $F_{e}$ of three clauses: $\begin{matrix} x_{u} \lor x_{v}, {\bar{x}}_{u} \lor x_{v}, x_{u} \lor {\bar{x}}_{v} . \end{matrix}$ Now if U is a vertex cover in G, the set $X_{U} = {x_{u}; u \in U}$ is a deletion $CNF (2)$ -backdoor set: after deleting the variable $x_{u}$ for $u \in U$ , the remaining formula consists of the unit clauses $x_{v}$ and ${\bar{x}}_{v}$ for $v \in V ∖ U$ .

On the other hand, if $U \subseteq V$ is not a vertex cover, and let edge $e = {u, v}$ be uncovered, then the subformula $F_{e}$ remains unchanged after deleting the variables in $X_{U}$ , thus $x_{u}$ and $x_{v}$ occur at least three times each, thus $X_{U}$ is not a deletion $CNF (2)$ -backdoor set. Thus F has a deletion $CNF (2)$ -backdoor set of size k iff G has a vertex cover of size k. □

We will focus on the case of formulas represented as sets in the remainder of the paper.
4. Weak Backdoors

We now show the hardness of finding weak $CNF (2)$ -backdoor sets.

Theorem 3.
Weak $CNF (2)$ -Backdoor Set is $W [2]$ -hard.

Proof:We reduce Hitting Set to Weak $CNF (2)$ -Backdoor Set. Let an instance $S = {S_{1}, \dots, S_{m}}$ of Hitting Set be given, with $U = S_{1} \cup \dots \cup S_{m}$ . We construct a formula $F = F (S)$ in the variables $x_{s}$ for $s \in U$ plus $z_{i, 1}$ and $z_{i, 2}$ for $1 ⩽ i ⩽ m$ , such that F has a weak $CNF (2)$ -backdoor set of size k iff S has a hitting set of size k.

The formula F has for every set $S_{i} \in S$ the subformula $D_{i}$ consisting of the three clauses $\begin{array}{l} \underset{s \in S_{i}}{\lor} x_{s} \lor {\bar{z}}_{i, 1}, z_{i, 1} \lor z_{i, 2}, z_{i, 1} \lor {\bar{z}}_{i, 2} . \end{array}$

Let $H \subseteq U$ be a hitting set for S. We show that $X_{H} : = {x_{s}; s \in H}$ is a weak $CNF (2)$ -backdoor set for $F (S)$ of the same size. Let α be the assignment with $α (x_{s}) = 1$ for every $s \in H$ . Then since H hits every set $S_{i}$ , it follows that $α ⊧ \lor_{s \in S_{i}} x_{s}$ for every i, and hence $D_{i} ⌈ α = (z_{i, 1} \lor z_{i, 2}) \land (z_{i, 1} \lor {\bar{z}}_{i, 2})$ is in $CNF (2)$ and satisfiable for every i. Thus $F ⌈ α$ is in $CNF (2)$ and satisfiable.

For the other direction, let B be a weak $CNF (2)$ -backdoor set for F, and let α be an assignment to the variables in B such that $F ⌈ α$ is in $CNF (2)$ and satisfiable. We first show that without loss of generality, B contains only variables $x_{s}$ for $s \in U$ . If B contains a variable $z_{i, b}$ , then the assignment α restricted to the variables in $B ∖ {z_{i, b}}$ will still leave every subformula $D_{j}$ for $j \neq i$ in $CNF (2)$ and satisfiable. Thus if we let $B^{'} = B ∖ {z_{i, b}} \cup {x_{s}}$ for an arbitrary $s \in S_{i}$ , and let $α^{'} (x_{s}) = 1$ and $α^{'}$ coincide with α for all variables in $B ∖ {z_{i, b}}$ , then $F ⌈ α^{'}$ is in $CNF (2)$ and satisfiable, thus $B^{'}$ is a weak $CNF (2)$ -backdoor set with $| B^{'} | ⩽ | B |$ .

Now we define $H_{B} : = {s; x_{s} \in B}$ , and show that $H_{B}$ is a hitting set for S of size $| B |$ . Assume for contradiction that $S_{i} \cap H_{B} = \emptyset$ . Then the formula $D_{i}$ is left unchanged in $F ⌈ α$ , and therefore the variable $z_{i, 1}$ has three occurrences in $F ⌈ α$ . Hence B can not be a weak $CNF (2)$ -backdoor set. □

In the survey [5] of Gaspers and Szeider, there is a generic construction to show the $W [2]$ -hardness of the problem Weak C -Backdoor Set for a class C. Our reduction is based on that construction, but it is simplified, and it has the property that the formula $F (S)$ only depends on S and is independent from the parameter k. In other words, it is a polynomial time reduction between the underlying classical problems that does not increase the parameter. The same simplification can also be made to other applications of the generic construction in [5], e.g. for $C = H ORN$ and $C = 2 - CNF$ .

On the other hand, the problem of finding weak $CNF (2)$ -backdoor sets becomes fixed-parameter tractable when restricted to inputs in $3 - CNF$ :
Theorem 4.
The problem Weak $CNF (2)$ -Backdoor Set for $3 - CNF$ -formulas is fixed-parameter tractable.

Proof:We will devise a bounded search tree algorithm that, given a formula F and parameter k, will search for a restriction α of size $| α | ⩽ k$ such that $F ⌈ α$ is in $CNF (2)$ and satisfiable. We will call such a restriction a backdoor restriction, its domain is a weak $CNF (2)$ -backdoor set. Obviously, a backdoor restriction exists if and only if a weak $CNF (2)$ -backdoor set exists.

A set of three clauses $C_{1}, C_{2}, C_{3}$ in F that share a common variable x will be called an obstruction.
Proposition 5.
Let an obstruction $C_{1}, C_{2}, C_{3}$ in F be given. Then every backdoor restriction α for F must set some variable that occurs in $C_{1}, C_{2}, C_{3}$ .

This holds because otherwise we have $C_{i} ⌈ α = C_{i}$ for $i = 1, 2, 3$ and therefore $F ⌈ α$ still contains the obstruction, and is thus not in $CNF (2)$ .

Once we have chosen a literal to be set, the following obvious proposition shows the correctness of the recurrence that the search tree algorithm is based on.
Proposition 6.
F has a backdoor restriction of size k that contains the assignment $[a : = 1]$ iff $F ⌈ [a : = 1]$ has a backdoor restriction of size $k - 1$ .

These two proposition show the correctness of the following algorithm, that finds a backdoor restriction of size k in a $3 - CNF$ -formula F if one exists.

Build a search tree of depth k, where at each node v at depth d we keep a partial assignment $α_{v}$ of size $| α_{v} | = d$ . At the root we have $α = \emptyset$ . A node v is closed if $F ⌈ α_{v}$ is in $CNF (2)$ .

To extend the tree from a node v of depth $d < k$ that is not closed and labeled with α, find an obstruction $C_{1}, C_{2}, C_{3}$ in $F ⌈ α$ with the common variable x.

Now for each literal a based on a variable occurring in $C_{1}, C_{2}, C_{3}$ , add a child to v with the assignment $α \cup [a : = 1]$ . These are at most 14 children since the clauses $C_{1}, C_{2}, C_{3}$ together contain at most 6 distinct variables besides x.

Now, for every closed leaf v labeled α, test whether $F ⌈ α$ is satisfiable. If so, α is a backdoor restriction. If there is no closed leaf, or for no closed leaf v the residual formula $F ⌈ α_{v}$ is satisfiable, then F does not have a backdoor restriction of size k, and hence no weak $CNF (2)$ -backdoor set of size k.

Since every inner node has at most 14 children, the size of the search tree is $14^{k}$ , and therefore the runtime is $O (14^{k} n)$ . □

The algorithm generalizes in the obvious way to formulas in $d - CNF$ for every fixed $d \in N$ , where the branching degree of the search tree is $2 (3 (d - 1) + 1) = 6 d - 4$ , and hence its size is ${(6 d - 4)}^{k}$ , which yields a runtime of ${(6 d - 4)}^{k} \cdot O (n)$ .
5. Strong Backdoors

Next, we show the hardness of finding strong $CNF (2)$ -backdoor sets. Unfortunately, the proof of this result only works when the input formulas are allowed to contain tautological clauses. The complexity of the problem restricted to formulas without tautological clauses remains open.

Theorem 7.
Strong $CNF (2)$ -Backdoor Set is $W [2]$ -hard.

Proof:We reduce Hitting Set to Strong $CNF (2)$ -Backdoor Set. The reduction is similar to that used in the proof of Theorem 3.

Let an instance $S = {S_{1}, \dots, S_{m}}$ of Hitting Set be given, with $U : = S_{1} \cup \dots \cup S_{m}$ . We construct a formula $F = F (S)$ in the variables $x_{s}$ for $s \in U$ plus $z_{i, 1}, z_{i, 2}$ for $1 ⩽ i ⩽ m$ , such that F has a strong $CNF (2)$ -backdoor set of size k iff S has a hitting set of size k.

The formula F has three clauses for every set $S_{i} \in S$ , viz. $\begin{array}{l} C_{i} : = \underset{s \in U}{\lor} {\bar{x}}_{s} \lor \underset{s \in S_{i}}{\lor} x_{s} \lor z_{i, 1}, {\bar{z}}_{i, 1} \lor z_{i, 2}, {\bar{z}}_{i, 1} \lor {\bar{z}}_{i, 2} . \end{array}$

Let $H \subseteq U$ be a hitting set for S. We show that $X_{H} : = {x_{s}; s \in H}$ is a strong $CNF (2)$ -backdoor set for $F (S)$ of the same size.

Let α be an assignment to the variables in $X_{H}$ . If $α (x_{s}) = 0$ for some $s \in H$ , then α satisfies $\lor_{s \in U} {\bar{x}}_{s}$ , and hence $α ⊧ C_{i}$ for every i. If, on the other hand $α (x_{s}) = 1$ for every $s \in H$ , then since H is a hitting set, α satisfies $\lor_{s \in S_{i}} x_{s}$ and hence $α ⊧ C_{i}$ for very i. Thus in either case $F ⌈ α \in CNF (2)$ .

Now let B be strong $CNF (2)$ -backdoor set for F. As in the proof of Theorem 3, we first show that without loss of generality, B contains only variables $x_{s}$ for $s \in S$ . If B contains a variable $z_{i, b}$ , then as before we can exchange it for a variable $x_{s}$ for an arbitrary $s \in S_{i}$ .

Now as above, we define $H_{B} : = {s; x_{s} \in B}$ , and show that $H_{B}$ is a hitting set for S of size $| B |$ . Assume for contradiction that $S_{i} \cap H_{B} = \emptyset$ , and let α be the assignment with $α (x_{s}) = 1$ for every $x_{s} \in B$ . Then α does not satisfy any of the clauses associated with $S_{i}$ , and thus the variable $z_{i, 1}$ occurs three times in $F ⌈ α$ . Hence B cannot have been a strong $CNF (2)$ -backdoor set. □

The comment after the proof of Theorem 3 applies here as well: the reduction from Hitting Set to Strong $CNF (2)$ -Backdoor Set given is actually a polynomial time reduction that does not change the parameter.

As in the case of weak $CNF (2)$ -backdoor sets, the problem of finding strong $CNF (2)$ -backdoor sets becomes fixed-parameter tractable when restricted to inputs in $3 - CNF$ .
Theorem 8.
Strong $CNF (2)$ -Backdoor Set for $3 - CNF$ -formulas is fixed-parameter tractable.

Proof:Let F be a $3 - CNF$ -formula, and X a subset of the variables of F. The following two propositions show the correctness of the bounded search tree algorithm to be presented below.
Proposition 9.
Let $α : X \to {0, 1}$ be a restriction. If $C_{1}, C_{2}, C_{3}$ is an obstruction in $F ⌈ α$ , then every strong $CNF (2)$ -backdoor set for F extending X contains a variable that occurs in $C_{1}, C_{2}, C_{3}$ .

Otherwise, if $Y \supseteq X$ is a set that is disjoint from the variables of $C_{1}, C_{2}, C_{3}$ , then for any restriction $β : Y \to {0, 1}$ that extends α the formula $F ⌈ β$ still contains the obstruction $C_{1}, C_{2}, C_{3}$ , and is therefore not in $CNF (2)$ .

Once we have chosen a variable to be included in the backdoor set, the following proposition, which holds obviously, shows the correctness of the recurrence that the search tree algorithm is based on.
Proposition 10.
F has a strong $CNF (2)$ -backdoor set of size k that contains the variable x iff there is a set B of size $| B | ⩽ k - 1$ that is a strong $CNF (2)$ -backdoor set for $F ⌈ [x : = 0]$ and for $F ⌈ [x : = 1]$ .

We build a search tree of depth k, where at each node of depth d a set of variables $X_{v}$ of size $| X_{v} | = d$ is kept. Together with $X_{v}$ we keep a set $C_{v} \subseteq 2^{X_{v}}$ of closed assignments, with the property that $F ⌈ α \in CNF (2)$ for every $α \in C_{v}$ . A node v is closed if $C_{v} = 2^{X_{v}}$ .

To extend the tree from a node of depth $d < k$ labeled $(X, C)$ that is not closed, pick an assignment $α : X \to {0, 1}$ such that $F ⌈ α \notin CNF (2)$ , and an obstruction, i.e., three clauses $C_{1}, C_{2}, C_{3}$ in $F ⌈ α$ that share a common variable x.

For each variable y occurring in $C_{1}, C_{2}, C_{3}$ , add a child to v labeled with $X \cup {y}$ . For each of these children, add a set $C^{'}$ of assignments. To determine the set $C^{'}$ , we first put both extensions $α \cup {[y : = 0]}$ and $α \cup {[y : = 1]}$ of every closed assignment $α \in C$ into $C^{'}$ . Then for every open assignment $β \in 2^{X} ∖ C$ we consider the extension $β_{0} : = β \cup {[y : = 0]}$ , and test whether $F ⌈ β_{0}$ is in $CNF (2)$ . If that is the case, we add $β_{0}$ to $C^{'}$ . We perform the same for the assignment $β_{1} : = β \cup {[y : = 1]}$ .

If a node is closed, i.e., $C = 2^{X}$ , then X is a strong backdoor set. If on the other hand, no closed node has been found up to depth k, then by the two Propositions 9 and 10 above there is no strong backdoor set of size k.

Since the three clauses ${C_{1}, C_{2}, C_{3}}$ contain at most 7 variables, size of the search tree is bounded by $7^{k}$ . At each node we need to perform at most $2^{k} O (n)$ computation steps, so the runtime is bounded by $14^{k} O (n)$ . □

As in the case of the algorithm for weak backdoor sets, this algorithm generalizes in the obvious way to formulas in $d - CNF$ for every fixed $d \in N$ , with a larger search tree size and thus a larger exponential dependence on the parameter k.
6. Upper Bounds

For most weak backdoor set problems that are not known to be in $FPT$ , there is no exact characterization of their complexity. With the exception of a few cases which are $W [P]$ -complete, for most of the other cases it is only known that they are $W [2]$ -hard and in $W [P]$ . We will now show the – to the best of our knowledge – first $W [2]$ -completeness results for weak backdoor set problems in the following theorem.

Theorem 11.
For the classes $C = 1 -V AL$ and $0 -V AL$ , the problem Weak C -Backdoor Set is $W [2]$ -complete.

Since finding weak backdoor sets for these classes is known to be $W [2]$ -hard [5], we only need to show that they are in $W [2]$ .

Since all formulas in $1 -V AL$ and $0 -V AL$ are satisfiable, weak backdoor sets into these classes are the same as the very weak backdoor sets defined next. This is an admittedly artificial notion of backdoor set where we weaken the requirement that the residual formula is satisfiable to the condition that it is not already false.

We define a very weak C-backdoor set for F to be a subset $X \subseteq V$ such that there is an assignment $α : X \to {0, 1}$ such that the formula $F ⌈ α$ is in C and non-trivial, i.e., $F ⌈ α \neq 0$ .

The parameterized problem Very Weak C -Backdoor Set is:
Instance:
$CNF$ -formula F, and $k \in N$ .
Parameter:
k.
Question:
Is there a very weak C-backdoor set for F of size k?

For the classes $1 -V AL$ and $0 -V AL$ , this problem is equivalent to Weak C -Backdoor Set, thus to prove Theorem 11 it suffices to show it is in $W [2]$ . Since our technique readily generalizes to other cases, we show that the problem of finding very weak C-backdoor sets is in $W [2]$ , for various tractable cases C. For the other cases besides $1 -V AL$ and $0 -V AL$ , this might turn out to be useful in the future.

We show that these problems are in the class $W [2]$ by making use of the logical characterization of this class. Proposition 12.
For each of the tractable classes $\begin{matrix} C = CNF (2), H ORN, CO -H ORN, 2 - CNF, C LU, 1 -V AL and 0 -V AL, \end{matrix}$ the problem Very Weak C -Backdoor Set is in $W [2]$ .
Proof:View a $CNF$ -formula F as a structure whose elements are the literals of F and the clauses of F, with the relations described in Table 1.

Table 1.
Relations of a formula as a structure

Relation Meaning

$lit (a)$ a is a literal

$cl (c)$ c is a clause

$occ (a, c)$ literal a occurs in clause c

$comp (a, b)$ a and b are complementary literals

$pos (a)$ a is a positive literal

$neg (a)$ a is a negative literal

For each of the classes C in the statement of the theorem, we will define a $Π_{2}$ -formula $φ_{C} (A)$ in this language with a free set variable A expressing that A is a backdoor restriction into the class C, i.e. $F ⊧ φ_{C} (α)$ for a restriction α iff $F ⌈ α \in C$ . We also define a $Π_{2}$ -formula ${ntriv}_{A}$ expressing that the formula F after restriction by A is nontrivial. Thus the problem Very Weak C -Backdoor Set is equivalent to the problem $W D (ψ_{C})$ , where $ψ_{C} : \equiv {ntriv}_{A} \land φ_{C} (A)$ . Since both formulas ${ntriv}_{A}$ and $φ_{C} (A)$ are $Π_{2}$ -formulas, this shows that these problems are in $W [2]$ .

We start by expressing that literal a is false under A. By uniqueness of the complementary literal, this can be expressed by the following formula: $\begin{matrix} {false}_{A} (a) : \equiv \exists x (comp (a, x) \land A (x)) \equiv \forall x (comp (a, x) \to A (x)) . \end{matrix}$ Note that this formula is a $Δ_{1}$ -formula, i.e., it is equivalent to both a $Π_{1}$ - and a $Σ_{1}$ -formula. Therefore it can be used like an atomic formula without increasing the quantifier complexity.

We then can express the condition that the formula F restricted by A is non-trivial by the $Π_{2}$ -formula $\begin{matrix} {ntriv}_{A} : \equiv \forall c cl (c) \to \exists a lit (a) \land occ (a, c) \land \neg {false}_{A} (a) . \end{matrix}$ We define a $Σ_{1}$ -formula stating that the clause c is satisfied by A as: $\begin{matrix} {sat}_{A} (c) : \equiv \exists x (occ (x, c) \land A (x)) . \end{matrix}$ The following $Π_{1}$ -formulas express that clauses $c_{1}$ and $c_{2}$ are equal after restriction by A: $\begin{array}{l} {sub}_{A} (c_{1}, c_{2}) : \equiv \forall x (occ (x, c_{1}) \to {false}_{A} (x) \lor occ (x, c_{2})), \\ {eq}_{A} (c_{1}, c_{2}) : \equiv {sub}_{A} (c_{1}, c_{2}) \land {sub}_{A} (c_{2}, c_{1}) . \end{array}$ We can express that the variable underlying literal a occurs in clause c by the $Δ_{1}$ -formula $\begin{array}{l} varocc (a, c) & : \equiv occ (a, c) \lor \exists x (comp (a, x) \land occ (x, c)) \\ \equiv occ (a, c) \lor \forall x (comp (a, x) \to occ (x, c)) . \end{array}$

With the aid of these formulas, we can write down the formula as: $\begin{array}{l} \forall c_{1}, c_{2}, c_{3} \underset{1 ⩽ i ⩽ 3}{\land} cl (c_{i}) \to (\underset{1 ⩽ i ⩽ 3}{\lor} {sat}_{A} (c_{i}) \lor \underset{1 ⩽ i < j ⩽ 3}{\lor} {eq}_{A} (c_{i}, c_{j}) \\ \lor \forall a (lit (a) \to A (a) \lor {false}_{A} (a) \lor \underset{1 ⩽ i ⩽ 3}{\lor} \neg varocc (a, c_{i}))) . \end{array}$ This formula $φ_{CNF (2)} (A)$ states that for any three clauses one of the following holds:
either one of them is satisfied by A,

or two of them are equal under A,

or every variable that is not set by A does not occur in one of them.
Thus $F ⊧ φ_{CNF (2)} (α)$ if and only if $F ⌈ α$ is in $CNF (2)$ .

We can use the same technique to obtain upper bounds on the complexity of finding very weak backdoor sets for other tractable cases:

The following $Π_{2}$ -formula $φ_{2 - CNF} (A)$ states that F restricted by A is a $2 - CNF$ -formula. $\begin{array}{l} \forall c cl (c) \to & {sat}_{A} (c) \lor \forall a_{1}, a_{2}, a_{3} \underset{1 ⩽ i ⩽ 3}{\land} lit (a_{i}) \to (\underset{1 ⩽ i < j ⩽ 3}{\lor} a_{i} = a_{j} \\ \lor \underset{1 ⩽ i ⩽ 3}{\lor} A (a_{i}) \lor \underset{1 ⩽ i ⩽ 3}{\lor} {false}_{A} (a_{i}) \lor \underset{1 ⩽ i ⩽ 3}{\lor} \neg occ (a_{i}, c)) . \end{array}$ This formula states that for every clause c that is not satisfied by A, and any three literals, one of the following holds:
either two of the literals are equal,

or at least one of them is set by A,

or at least one of them does not occur in c.
Thus $F ⊧ φ_{2 - CNF} (α)$ if and only if $F ⌈ α$ is in $2 - CNF$ .

The following $Π_{2}$ -formula $φ_{H ORN} (A)$ states that F restricted by A is a Horn formula. $\begin{array}{l} \forall c cl (c) \to & {sat}_{A} (c) \lor \forall a, a^{'} lit (a) \land lit (a^{'}) \to (a = a^{'} \lor A (a) \lor A (a^{'}) \\ \lor {false}_{A} (a) \lor {false}_{A} (a^{'}) \\ \lor \neg occ (a, c) \lor \neg occ (a^{'}, c) \lor neg (a) \lor neg (a^{'})) \end{array}$ This formula states that for every clause c unsatisfied by A, and any two distinct literals that are not set by A and occur in c, one of them is negative. The formula $φ_{CO -H ORN} (A)$ is defined symmetrically.

A result of Nishimura et al. [10] characterizes the class of cluster formulas by excluded configurations: A formula is a cluster formula if it does not contain any of the following obstructions:
1.
two clauses C and $C^{'}$ that overlap, i.e., have a variable in common, but do not clash,
2.
three clauses $C_{1}$ , $C_{2}$ and $C_{3}$ such that $C_{1}$ and $C_{2}$ clash, and $C_{2}$ and $C_{3}$ clash, but $C_{1}$ and $C_{3}$ do not clash.

We define $Σ_{1}$ -formulas stating that two clauses overlap or clash as: $\begin{array}{l} overlap (c_{1}, c_{2}) : \equiv \exists x lit (x) \land \neg A (x) \land \neg {false}_{A} (x) \land varocc (x, c_{1}) \land varocc (x, c_{2}), \\ clash (c_{1}, c_{2}) : \equiv \exists x lit (x) \land \neg A (x) \land \neg {false}_{A} (x) \land occ (x, c_{1}) \\ \land \exists y (comp (x, y) \land occ (y, c_{2})) . \end{array}$ With the help of these formulas, we define the $Π_{2}$ -formula $φ_{C LU} (A)$ as $φ_{C LU 1} (A) \land φ_{C LU 2} (A)$ , where $φ_{C LU 1} (A)$ states that the formula F does not contain the first type of obstruction: $\begin{array}{l} \forall c_{1}, c_{2} (cl (c_{1}) \land cl (c_{2}) \to {sat}_{A} (c_{1}) \lor {sat}_{A} (c_{2}) \lor {eq}_{A} (c_{1}, c_{2}) \\ \lor \neg overlap (c_{1}, c_{2}) \lor clash (c_{1}, c_{2})) \end{array}$ and $φ_{C LU 2} (A)$ states that F does not have the second type of obstruction: $\begin{array}{l} \forall c_{1}, c_{2}, c_{3} (\underset{1 ⩽ i ⩽ 3}{\land} cl (c_{i}) \to \underset{1 ⩽ i ⩽ 3}{\lor} {sat}_{A} (c_{i}) \lor \underset{1 ⩽ i < j ⩽ 3}{\lor} {eq}_{A} (c_{i}, c_{j}) \\ \lor \neg clash (c_{1}, c_{2}) \lor \neg clash (c_{2}, c_{3}) \lor clash (c_{1}, c_{3})) . \end{array}$

Finally, we define the $Π_{2}$ -formula $φ_{1 -V AL} (A)$ expressing that the formula F restricted by A is 1-valid. The formula $φ_{0 -V AL} (A)$ is defined analogously.

We define the $Σ_{1}$ -formula $\begin{matrix} cpos (c) : = \exists x occ (x, c) \land \neg {false}_{A} (x) \land pos (x) \end{matrix}$ expressing that clause c contains a positive literal that is not falsified by A. Thus the following $Π_{2}$ -formula $\begin{matrix} φ_{1 -V AL} (A) : = \forall c cl (c) \to {sat}_{A} (c) \lor cpos (c) \end{matrix}$ states that F restricted by A is 1-valid. □
6.1. Open Problems

Relation	Meaning
$lit (a)$	a is a literal
$cl (c)$	c is a clause
$occ (a, c)$	literal a occurs in clause c
$comp (a, b)$	a and b are complementary literals
$pos (a)$	a is a positive literal
$neg (a)$	a is a negative literal

We list some problems left open by this work.

Settle the parameterized complexity of the problem Strong $CNF (2)$ -Backdoor Set in the restricted case when formulas do not contain tautological clauses, i.e., show the problem remains $W [2]$ -hard in this case.

Determine the precise parameterized complexity of Weak C -Backdoor Set for tractable cases C other that 1-Val and 0-Val, possibly using the logical approach used in this paper.

Is the problem Strong C -Backdoor Set in $W [2]$ for the tractable cases $C = CNF (2)$ and $C = C LU$ , for which we know it is $W [2]$ -hard?

Footnotes

Acknowledgements

I thank Stefan Szeider, Sebastian Ordyniak and Ulrich Schöpp for useful discussions about the contents of the paper, and an anonymous referee whose comments helped to improve the presentation of the paper. The research leading to the results in this paper was initiated at Dagstuhl Seminar 12471 “SAT Interactions”.

References

Cook

S.A.

, The complexity of theorem-proving procedures, in: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, 1971, pp. 151–158.

Crama

Ekin

and Hammer

P.L.

, Variable and term removal from Boolean formulae, Discrete Applied Mathematics 75(3) (1997), 217–230. doi:10.1016/S0166-218X(96)00028-5.

Downey

R.G.

and Fellows

M.R.

, Fixed-parameter tractability and completeness, Congressus Numerantium 87 (1992), 161–187.

Flum

and Grohe

, Parameterized Complexity Theory, Texts in Theoretical Computer Science, Springer, 2006.

Gaspers

and Szeider

, Backdoors to satisfaction, in: The Multivariate Algorithmic Revolution and Beyond Bodlaender

H.L.

Downey

Fomin

F.V.

and Marx

, eds, Lecture Notes in Computer Science, Vol. 7370, 2012, pp. 287–317. doi:10.1007/978-3-642-30891-8_15.

Impagliazzo

Paturi

and Zane

, Which problems have strongly exponential complexity?, Journal of Computer and System Sciences 63(4) (2001), 512–530. doi:10.1006/jcss.2001.1774.

Iwama

, CNF-satisfiability test by counting and polynomial average time, SIAM Journal on Computing 18(2) (1989), 385–391. doi:10.1137/0218026.

Johannsen

, Satisfiability problems complete for deterministic logarithmic space, in: 21st International Symposium on Theoretical Aspects of Computer Science (STACS 2004) Diekert

and Habib

, eds, Lecture Notes in Computer Science, Vol. 2996, 2004, pp. 317–325.

Kleine Büning

and Lettmann

, Propositional Logic: Deduction and Algorithms, Cambridge University Press, 1999.

10.

Nishimura

Ragde

and Szeider

, Solving #SAT using vertex covers, Acta Informatica 44(7–8) (2007), 509–523. doi:10.1007/s00236-007-0056-x.

11.

Nishimura

Ragde

and Szeider

, Detecting backdoor sets with respect to Horn and binary clauses, in: Proceedings of the 7th International Conference on Theory and Applications of Satisfiability Testing, 2004, pp. 96–103.

12.

Schaefer

T.J.

, The complexity of satisfiability problems, in: Proceedings of the 10th ACM Symposium on Theory of Computing, 1978, pp. 216–226.

13.

Williams

Gomes

and Selman

, Backdoors to typical case complexity, in: Proceedings of the 18th International Joint Conference on Artificial Intelligence Gottlob

and Walsh

, eds, 2003, pp. 1173–1178.

Backdoors into Two Occurrences

Abstract

Keywords

1. Introduction

2. Preliminaries

2.1. Tractable Cases of SAT

2.2. Parameterized Complexity

2.3. Backdoor Sets

3. Backdoors into CNF ( 2 )

Footnotes

Acknowledgements

References

3. Backdoors into $CNF (2)$