Backdoors into Two 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 2k⋅mO(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∈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 x¯. A clause is a disjunction C=a1∨⋯∨ad of literals ai. 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=C1∧⋯∧Cm of clauses, it is usually identified with the set of clauses {C1,…,Cm}. 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→{0,1} from the set of variables V to the truth values {0,1}. A restriction α is extended to literals by setting α(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∈C, and otherwise C⌈α is the disjunction of those literals a∈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∈F, and otherwise F⌈α is the conjunction of the clauses C⌈α for those clauses C∈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 [x¯:=𝜖] denote [x:=(1−𝜖)].

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

A clause C is tautological, if both x and 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.

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:

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:

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.

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 xv∈V for v, and for every edge {u,v} a subformula Fe of three clauses:

On the other hand, if U⊆V is not a vertex cover, and let edge e={u,v} be uncovered, then the subformula Fe remains unchanged after deleting the variables in XU, thus xu and xv occur at least three times each, thus XU 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.

Proof:We reduce Hitting Set to Weak CNF(2)-Backdoor Set. Let an instance S={S1,…,Sm} of Hitting Set be given, with U=S1∪⋯∪Sm. We construct a formula F=F(S) in the variables xs for s∈U plus zi,1 and zi,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 Si∈S the subformula Di consisting of the three clauses

Let H⊆U be a hitting set for S. We show that XH:={xs;s∈H} is a weak CNF(2)-backdoor set for F(S) of the same size. Let α be the assignment with α(xs)=1 for every s∈H. Then since H hits every set Si, it follows that α⊧∨s∈Sixs for every i, and hence Di⌈α=(zi,1∨zi,2)∧(zi,1∨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 xs for s∈U. If B contains a variable zi,b, then the assignment α restricted to the variables in B∖{zi,b} will still leave every subformula Dj for j≠i in CNF(2) and satisfiable. Thus if we let B′=B∖{zi,b}∪{xs} for an arbitrary s∈Si, and let α′(xs)=1 and α′ coincide with α for all variables in B∖{zi,b}, then F⌈α′ is in CNF(2) and satisfiable, thus B′ is a weak CNF(2)-backdoor set with |B′|⩽|B|.

Now we define HB:={s;xs∈B}, and show that HB is a hitting set for S of size |B|. Assume for contradiction that Si∩HB=∅. Then the formula Di is left unchanged in F⌈α, and therefore the variable zi,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=HORN 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:

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 C1,C2,C3 in F that share a common variable x will be called an obstruction.

This holds because otherwise we have Ci⌈α=Ci 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.

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 α=∅. 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 C1,C2,C3 in F⌈α with the common variable x.

Now for each literal a based on a variable occurring in C1,C2,C3, add a child to v with the assignment α∪[a:=1]. These are at most 14 children since the clauses C1,C2,C3 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 14k, and therefore the runtime is O(14kn).  □

The algorithm generalizes in the obvious way to formulas in d-CNF for every fixed d∈N, where the branching degree of the search tree is 2(3(d−1)+1)=6d−4, and hence its size is (6d−4)k, which yields a runtime of (6d−4)k⋅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.

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={S1,…,Sm} of Hitting Set be given, with U:=S1∪⋯∪Sm. We construct a formula F=F(S) in the variables xs for s∈U plus zi,1,zi,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 Si∈S, viz.

Let H⊆U be a hitting set for S. We show that XH:={xs;s∈H} is a strong CNF(2)-backdoor set for F(S) of the same size.

Let α be an assignment to the variables in XH. If α(xs)=0 for some s∈H, then α satisfies ∨s∈Ux¯s, and hence α⊧Ci for every i. If, on the other hand α(xs)=1 for every s∈H, then since H is a hitting set, α satisfies ∨s∈Sixs and hence α⊧Ci for very i. Thus in either case F⌈α∈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 xs for s∈S. If B contains a variable zi,b, then as before we can exchange it for a variable xs for an arbitrary s∈Si.

Now as above, we define HB:={s;xs∈B}, and show that HB is a hitting set for S of size |B|. Assume for contradiction that Si∩HB=∅, and let α be the assignment with α(xs)=1 for every xs∈B. Then α does not satisfy any of the clauses associated with Si, and thus the variable zi,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.

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.

Otherwise, if Y⊇X is a set that is disjoint from the variables of C1,C2,C3, then for any restriction β:Y→{0,1} that extends α the formula F⌈β still contains the obstruction C1,C2,C3, 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.

We build a search tree of depth k, where at each node of depth d a set of variables Xv of size |Xv|=d is kept. Together with Xv we keep a set Cv⊆2Xv of closed assignments, with the property that F⌈α∈CNF(2) for every α∈Cv. A node v is closed if Cv=2Xv.

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

For each variable y occurring in C1,C2,C3, add a child to v labeled with X∪{y}. For each of these children, add a set C′ of assignments. To determine the set C′, we first put both extensions α∪{[y:=0]} and α∪{[y:=1]} of every closed assignment α∈C into C′. Then for every open assignment β∈2X∖C we consider the extension β0:=β∪{[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:=β∪{[y:=1]}.

If a node is closed, i.e., C=2X, 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 {C1,C2,C3} contain at most 7 variables, size of the search tree is bounded by 7k. At each node we need to perform at most 2kO(n) computation steps, so the runtime is bounded by 14kO(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∈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.

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-VAL and 0-VAL 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⊆V such that there is an assignment α:X→{0,1} such that the formula F⌈α is in C and non-trivial, i.e., F⌈α≠0.

The parameterized problem Very Weak C-Backdoor Set is:

For the classes 1-VAL and 0-VAL, 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-VAL and 0-VAL, 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.

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⌈α∈C. We also define a Π2-formula ntrivA expressing that the formula F after restriction by A is nontrivial. Thus the problem Very Weak C-Backdoor Set is equivalent to the problem WD(ψC), where ψC:≡ntrivA∧φC(A). Since both formulas ntrivA 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:

We then can express the condition that the formula F restricted by A is non-trivial by the Π2-formula

With the aid of these formulas, we can write down the formula as:

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.

The following Π2-formula φHORN(A) states that F restricted by A is a Horn formula.

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:

We define Σ1-formulas stating that two clauses overlap or clash as:

Finally, we define the Π2-formula φ1-VAL(A) expressing that the formula F restricted by A is 1-valid. The formula φ0-VAL(A) is defined analogously.

We define the Σ1-formula