You are viewing a javascript disabled version of the site. Please enable Javascript for this site to function properly.
Go to headerGo to navigationGo to searchGo to contentsGo to footer
In content section. Select this link to jump to navigation

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.

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 2kmO(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 tN, 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=a1ad 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=C1Cm 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 aC, and otherwise Cα is the disjunction of those literals aC 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 CF, and otherwise Fα is the conjunction of the clauses Cα for those clauses CF 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:

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 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 FC can be decided in polynomial time,

  • the satisfiability problem for formulas FC 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 HORN of Horn formulas, i.e., formulas in which every clause contains at most one positive literal.

  • The class CO-HORN 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 aC and a¯C for some literal a. A formula F is a hitting formula if any two different clauses in F clash. The class CLU 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)N. We denote by n=n(x)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)O(nd) for some computable function f and dN. 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)O(nd) for some computable function f and dN,

  • 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 WD(φ) is the following:

Instance:

Structure A for the language of φ, kN.

Parameter:

k.

Question:

Is there a relation RAd 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 WD(φ) for a Πt-formula φ(X).

The parameterized problem Weighted Circuit SAT is:

Instance:

Boolean circuit C, kN.

Parameter:

k.

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
FPTW[1]W[2]W[t]W[P].
The parameterized problem Hitting Set is the following :

Instance:

Family {S1,,Sm} of subsets SiU, kN.

Parameter:

k.

Question:

Is there a set HU of size |H|k with HSi 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 Si, and the element relation ∈ between elements of U and sets. Then Hitting Set is the problem WD(φ) for the following Π2-formula φ(X) with a unary relation variable X:
φ(X)x(set(x)y(U(y)X(y)xy)).

2.3.Backdoor Sets

Let F be a CNF-formula in the variables V, and let C be a tractable case of SAT. Let XV be a set of variables. The formula FX is the formula obtained by deleting from the clauses in F all occurrences of literals x and x¯ for xX.

  • A strong C-backdoor set for F is a subset XV such that for every assignment α:X{0,1}, the formula Fα is in C.

  • A weak C-backdoor set for F is a subset XV such that there is an assignment α:X{0,1} such that the formula Fα is in C and satisfiable.

  • A deletion C-backdoor set for F is a subset XV such that the formula FX is in C.

If the class C is closed under subsets, then every deletion backdoor set is also a strong backdoor set, since FαFX for every α:X{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 FX=αFα where the union is over all α:X{0,1}.

The parameterized problem Strong C-Backdoor Set is:

Instance:

CNF-formula F, and kN.

Parameter:

k.

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=HORN, CO-HORN, 2-CNF, 1-VAL and 0-VAL, 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 dN. For the class of cluster formulas, both problems Strong CLU-Backdoor Set and Weak CLU-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:

(x1x2x¯3),(x¯1x2x5),(x¯1x¯3x¯5),(x¯2x4),(x3x¯4).
The variables {x1,x2,x3} occur three times each, so the smallest deletion CNF(2)-backdoor set has size 3. But {x1} 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 xvV for v, and for every edge {u,v} a subformula Fe of three clauses:

xuxv,x¯uxv,xux¯v.
Now if U is a vertex cover in G, the set XU={xu;uU} is a deletion CNF(2)-backdoor set: after deleting the variable xu for uU, the remaining formula consists of the unit clauses xv and x¯v for vVU.

On the other hand, if UV 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.

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={S1,,Sm} of Hitting Set be given, with U=S1Sm. We construct a formula F=F(S) in the variables xs for sU plus zi,1 and zi,2 for 1im, 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 SiS the subformula Di consisting of the three clauses

sSixsz¯i,1,zi,1zi,2,zi,1z¯i,2.

Let HU be a hitting set for S. We show that XH:={xs;sH} is a weak CNF(2)-backdoor set for F(S) of the same size. Let α be the assignment with α(xs)=1 for every sH. Then since H hits every set Si, it follows that αsSixs for every i, and hence Diα=(zi,1zi,2)(zi,1z¯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 sU. 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 ji in CNF(2) and satisfiable. Thus if we let B=B{zi,b}{xs} for an arbitrary sSi, 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;xsB}, and show that HB is a hitting set for S of size |B|. Assume for contradiction that SiHB=. 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:

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

Proposition 5.

Let an obstruction C1,C2,C3 in F be given. Then every backdoor restriction α for F must set some variable that occurs in C1,C2,C3.

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.

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 k1.

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 dN, where the branching degree of the search tree is 2(3(d1)+1)=6d4, and hence its size is (6d4)k, which yields a runtime of (6d4)kO(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={S1,,Sm} of Hitting Set be given, with U:=S1Sm. We construct a formula F=F(S) in the variables xs for sU plus zi,1,zi,2 for 1im, 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 SiS, viz.

Ci:=sUx¯ssSixszi,1,z¯i,1zi,2,z¯i,1z¯i,2.

Let HU be a hitting set for S. We show that XH:={xs;sH} 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 sH, then α satisfies sUx¯s, and hence αCi for every i. If, on the other hand α(xs)=1 for every sH, then since H is a hitting set, α satisfies sSixs 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 sS. If B contains a variable zi,b, then as before we can exchange it for a variable xs for an arbitrary sSi.

Now as above, we define HB:={s;xsB}, and show that HB is a hitting set for S of size |B|. Assume for contradiction that SiHB=, and let α be the assignment with α(xs)=1 for every xsB. 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.

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{0,1} be a restriction. If C1,C2,C3 is an obstruction in Fα, then every strong CNF(2)-backdoor set for F extending X contains a variable that occurs in C1,C2,C3.

Otherwise, if YX 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.

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|k1 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 Xv of size |Xv|=d is kept. Together with Xv we keep a set Cv2Xv 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 β2XC 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 dN, 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-VAL and 0-VAL, 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-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 XV 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:

Instance:

CNF-formula F, and kN.

Parameter:

k.

Question:

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

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.

Proposition 12.

For each of the tractable classes

C=CNF(2),HORN,CO-HORN,2-CNF,CLU,1-VAL and 0-VAL,
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

RelationMeaning
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α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:

falseA(a):x(comp(a,x)A(x))x(comp(a,x)A(x)).
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

ntrivA:ccl(c)alit(a)occ(a,c)¬falseA(a).
We define a Σ1-formula stating that the clause c is satisfied by A as:
satA(c):x(occ(x,c)A(x)).
The following Π1-formulas express that clauses c1 and c2 are equal after restriction by A:
subA(c1,c2):x(occ(x,c1)falseA(x)occ(x,c2)),eqA(c1,c2):subA(c1,c2)subA(c2,c1).
We can express that the variable underlying literal a occurs in clause c by the Δ1-formula
varocc(a,c):occ(a,c)x(comp(a,x)occ(x,c))occ(a,c)x(comp(a,x)occ(x,c)).

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

c1,c2,c31i3cl(ci)(1i3satA(ci)1i<j3eqA(ci,cj)a(lit(a)A(a)falseA(a)1i3¬varocc(a,ci))).
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.

ccl(c)satA(c)a1,a2,a31i3lit(ai)(1i<j3ai=aj1i3A(ai)1i3falseA(ai)1i3¬occ(ai,c)).
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 φHORN(A) states that F restricted by A is a Horn formula.

ccl(c)satA(c)a,alit(a)lit(a)(a=aA(a)A(a)falseA(a)falseA(a)¬occ(a,c)¬occ(a,c)neg(a)neg(a))
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-HORN(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 C1, C2 and C3 such that C1 and C2 clash, and C2 and C3 clash, but C1 and C3 do not clash.

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

overlap(c1,c2):xlit(x)¬A(x)¬falseA(x)varocc(x,c1)varocc(x,c2),clash(c1,c2):xlit(x)¬A(x)¬falseA(x)occ(x,c1)clash(c1,c2):y(comp(x,y)occ(y,c2)).
With the help of these formulas, we define the Π2-formula φCLU(A) as φCLU1(A)φCLU2(A), where φCLU1(A) states that the formula F does not contain the first type of obstruction:
c1,c2(cl(c1)cl(c2)satA(c1)satA(c2)eqA(c1,c2)¬overlap(c1,c2)clash(c1,c2))
and φCLU2(A) states that F does not have the second type of obstruction:
c1,c2,c3(1i3cl(ci)1i3satA(ci)1i<j3eqA(ci,cj)¬clash(c1,c2)¬clash(c2,c3)clash(c1,c3)).

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

cpos(c):=xocc(x,c)¬falseA(x)pos(x)
expressing that clause c contains a positive literal that is not falsified by A. Thus the following Π2-formula
φ1-VAL(A):=ccl(c)satA(c)cpos(c)
states that F restricted by A is 1-valid.  □

6.1.Open Problems

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=CLU, for which we know it is W[2]-hard?

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

[1] 

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

[2] 

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

[3] 

R.G. Downey and M.R. Fellows, Fixed-parameter tractability and completeness, Congressus Numerantium 87 (1992), 161–187.

[4] 

J. Flum and M. Grohe, Parameterized Complexity Theory, Texts in Theoretical Computer Science, Springer, 2006.

[5] 

S. Gaspers and S. Szeider, Backdoors to satisfaction, in: The Multivariate Algorithmic Revolution and Beyond, H.L. Bodlaender, R. Downey, F.V. Fomin and D. Marx, eds, Lecture Notes in Computer Science, Vol. 7370, 2012, pp. 287–317. doi:10.1007/978-3-642-30891-8_15.

[6] 

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

[7] 

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

[8] 

J. Johannsen, Satisfiability problems complete for deterministic logarithmic space, in: 21st International Symposium on Theoretical Aspects of Computer Science (STACS 2004), V. Diekert and M. Habib, eds, Lecture Notes in Computer Science, Vol. 2996, 2004, pp. 317–325.

[9] 

H. Kleine Büning and T. Lettmann, Propositional Logic: Deduction and Algorithms, Cambridge University Press, 1999.

[10] 

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

[11] 

N. Nishimura, P. Ragde and S. 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] 

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

[13] 

R. Williams, C. Gomes and B. Selman, Backdoors to typical case complexity, in: Proceedings of the 18th International Joint Conference on Artificial Intelligence, G. Gottlob and T. Walsh, eds, 2003, pp. 1173–1178.