Backdoors To Typical Case Complexity

1 Introduction

Most interesting AI formalisms for reasoning, planning, and learning have been shown to be worst-case intractable. In the eighties and early nineties, such negative complexity re­ sults led to an extensive search for tractable subclasses of the general formalisms. Unfortunately, these tractable sub­ classes were often too restrictive for real-world applications. In the mid-nineties, we saw the emergence of a more practical approach to computationally hard problems in AI, with the introduction of fast satisfiability solvers and fast constraint based reasoning methods [17]. For example, in planning we saw the success of constraint-based planners, such as Graph­ plan [2] and SatPlan [13], and most recently, heuristic search selman@cs.cornell.edu based planners, e.g., [11; 8; 1]. Somewhat surprisingly, on practical problem instances these methods scale well beyond what one might expect based on a formal complexity anal­ ysis. In fact, current state-of-the-art SAT solvers can han­ dle problem instances, as they arise in finite model-checking and planning, with up to a million variables and five million clauses [15]. The success of these methods appears to hinge on a combination of two factors: ( 1) practical combinato­ rial problem instances generally have a substantial amount of (hidden) tractable sub-structure, and (2) new algorithmic techniques exploit such tractable structure, through, e.g., ran­ domization and constraint learning.

*Supported in part by an NSF Graduate Fellowship and the NSF ALADDIN Center.

tResearch supported by AFOSR, Darpa, and the NSF.

These developments suggest that a standard worst-case complexity analysis does not capture well the true complex­ ity of typical problem instances encountered in practical ap­ plications. Theoretical computer scientists have been well­ aware of the limitations of worst-case complexity results and have explored alternatives, such as average-case complexity and smoothed analysis [20]. In average-case analysis, one studies the computational cost of solving problem instances drawn from a predefined problem distribution. Such an anal­ ysis can provide valuable insights, as demonstrated by the work on uniform random instance distributions (e.g. ran­ dom k-SAT). However, the relatively basic distributions for which one can obtain average-complexity results appear to be quite far removed from the instance distributions one en­ counters in practice. In fact, formally defining the distribution of real-world problem instances is generally an open prob­ lem in itself. Smoothed analysis attempts to unify worst-case and average-case, but suffers from limited applicability: it works well on algorithms for problems defined over dense fields such as the simplex algorithm, but the applicability of smoothed analysis on discrete problem domains is unclear.

An alternative approach, which we will pursue in this pa­ per, is to identify special structural properties common to known problem instances and rigorously show how clever algorithms can exploit such properties. Informal insights about what such special structure might be are currently al­ ready used in the design of, for example, branching and vari­ able choice heuristics in combinatorial search methods. A common feature of these techniques is an understanding that different groups of variables in a problem encoding often play quite distinct roles. For example, at the highest level, one can distinguish between dependent and independent vari­ ables. The dependent or auxiliary variables are needed to ob­ tain compact problem encodings but the true combinatorics arises from the independent variables; e.g., the independent variables in an encoding of a planning domain represent the various operators applicable in a given state of the world, whereas the dependent variables encode the consequences of selecting a particular operator. A plan search technique that branches purely on the independent variables can obtain sub­ stantial speedups over search methods that do not exploit vari­ able dependencies [4].

Another powerful intuition in the design of search methods is that one wants to select variables that simplify the prob­ lem instance as much as possible when these variables are assigned values. This intuition leads to the common heuristic of branching on the most constrained variable first. In terms of Boolean satisfiability, this amounts to, in effect, focusing in on the tractable substructure of the problem, namely the unit clauses (I-SAT structure) and the binary clauses (2-SAT structure). The true effectiveness of this approach arises from the fact that setting most constraint variables also simplifies higher arity clauses, which either become satisfied or in tum shrink themselves eventually to binary or unary clauses.

These general insights have been incorporated in state-of­ the-art SAT and constraint solvers, and their effectiveness has been demonstrated empirically on a significant number of benchmark problems [18]. However, a more formal un­ derpinning explaining the practical success of these strate­ gies has been lacking. In this paper, we introduce a formal framework directly inspired by these techniques and present rigorous complexity results that support their effectiveness.

Preview of results. We first introduce the notion of "back­ door" variables. This is a set of variables for which there is a value assignment such that the simplified problem can be solved by a poly-time algorithm, called the "sub-solver". The sub-solver captures any form of poly-time simplification pro­ cedure as used in current SAT/CSP solvers. We also con­ sider the notion of a "strong backdoor" where any setting of the backdoor variables leads to a poly-time solvable sub­ problem. The set of all problem variables forms a trivial back­ door set, but many interesting practical problem instances possess much smaller backdoors and strong backdoors. We will study backdoors in several practical problem instances, and identify backdoors that contain only a fraction of the to­ tal number of variables. For example, the SAT encoding of a logistics planning problem (logistics. d. cnf) contains a backdoor with only 12 variables out of a total of nearly 7,000 variables. When given a set of back door variables of a problem instance, one can restrict the combinatorial search by branching only on the backdoor variables and thus search a drastically reduced space.

In general, finding a small set of backdoor variables for a problem instance is, however, itself a computationally hard problem. One contribution of this paper is that we formally show how the presence of a small backdoor in a problem pro­ vides a concrete computational advantage in solving it. We analyze three scenarios. First, we consider a deterministic scenario with an exhaustive search of backdoor sets. We show that one obtains provably better search complexity when the backdoor contains up to a certain fraction of all variables. We then show that a randomized search technique, which in ef­ fect repeatedly guesses backdoor sets, provably outperforms a deterministic search. Finally, in our third scenario we con­ sider the availability of a variable selection heuristic, which provides guidance towards the backdoor set. This strategy can yet further reduce the search space. Table 1 gives a high­ level summary of the results. By exploiting restart strategies, we can identify a polynomially solvable case when the back­ door contains at most log( n) variables. We believe that this final scenario is closest to the behavior of current effective SAT and constraint solvers. Our formal analysis also sug­ gests several novel algorithmic strategies that warrant further empirical exploration.

2 Hidden structure: Backbones and Backdoors

Our approach and analysis applies both to SAT and CSP problems [17]. SAT is the abbreviation for the well-studied Boolean satisfiability problem. CSP is the abbreviation for the more general problem of constraint satisfaction.

A CSP problem, C, is characterized by a set V = { x 1 , x2 , . .. , Xn} of variables, with respective domains D1, D2, ... , Dn (which list the possible values for each vari­ able) and a set of constraints. A constraint is defined on a subset of variables si c v denoting the variables' simulta­ neous legal assignments. That is, if si = {Xi, ' X;2 ' . .. 'X;,.}, then the constraint defines a subset of the Cartesian product D; 1 x ... x D;r. To simplify notation, we will assume that all variables have the same domain D. We use d to denote the size of D. An assignment a is a function from variables to D. A solution to a CSP is a complete variable assignment that satisfies all constraints. A partial assignment defines the values of a subset of the variables in V. SAT is a special case of CSP with only Boolean variables (D = {True, False}) and constraints given in the form of clauses. A clause is a disjunction of literals and a literal is a Boolean variable or its negation.

We use the notation C[v/x] to denote the simplified CSP obtained from a CSP, C, by setting the value of variable x to value v. (A constraint involving x is simplified by keeping only the allowed tuples that have x assigned to v.) Let as :

S s:;; V --t D be a partial assignment. We use C[as] to denote the simplified CSP obtained by setting the variables defined in as . In a SAT problem, this corresponds to simplifying the formula by fixing the truth values of some of the variables.

Our goal is to capture structural properties of real world problem instances. We start by reviewing the concept of a backbone in a SAT/CSP problem, as introduced in [14]. A variable is called a backbone variable if in all solutions to the CSP the variable is assigned the same value. Such variables are also called frozen variables [6] . Backbone variables are useful in studying the properties of the solution space of a constraint satisfaction problem.

Definition 2.1 [backbone] S is a backbone if there is a unique partial assignment as : S --t D such that C[as] is satisfiable.

We contrast this variable type with the kind we introduce, backdoors. Backdoors are variable subsets defined with re­ spect to a particular algorithm; once the backdoor variables are assigned a value, the problem becomes easy under that algorithm. (Note that contrarily to the backbone there can be different sets of backdoor variables.)

To begin our exposition of backdoors, we define the sort of algorithms we have in mind. We will call them sub-solvers, as they solve tractable subcases of the general constraint sat­ isfaction problem.

Definition 2.2 A sub-solver A given as input a CSP, C, sat­ isfies the following:

• (Trichotomy) A either rejects the input C, or "deter­ mines " C correctly (as unsatisfiable or satisfiable, returning a solution if satisfiable),
• (Efficiency) A runs in polynomial time,
• (Trivial solvability) A can determine if C is trivially true (has no constraints) or trivially false (has a contradictory constraint),
• (Self-reducibility) if A determines C, then for any vari­ able x and value v, then A determines C[v / x].

For instance, A could be an algorithm that solves 2-SAT in­ stances but rejects all other instances. It is important to note that the results we will show in this paper are independent of a particular sub-solver; our results will hold for any A satis­ fying the above four properties.

In what follows, Jet A be a sub-solver, and C be a CSP.

We first consider a notion of "backdoor" that is suitable for satisfiable CSPs.

Definition 2.3 [backdoor] A nonempty subsetS of the vari­ ables is a backdoor in C for A if for some as : S --t D, A returns a satisfying assignment ofC[as].

Intuitively, the backdoor corresponds to a set of variables, such that when set correctly, the sub-solver can solve the re­ maining problem. In a sense, the backdoor is a "witness"

to the satisfiability of the instance, given a sub-solver algo­ rithm. 1 We also introduce a stronger notion of the backdoor to deal with both satisfiable and unsatisfiable (inconsistent) problem instances.

Definition 2.4 [strong backdoor] A nonempty subset S of the variables is a strong backdoor in C for A if for all as : S --t D, A returns a satisfying assignment or concludes unsatisfiability of C[as ].

In contrast to backbones which are necessarily set to a cer­ tain value, a (strong) backdoor S is sufficient for solving a problem. For example, when given the backdoor for a SAT problem, the search cost is of order IDIISI. (Simply check all possible assignments of S.) This means if S is relatively small , one obtains a large improvement over searching the full space of variable/value assignments.

We observe that independent variables are a particular kind of backdoor. As stated in [ 12], they are a set S of variables for which all other variables may be thought of as defined in terms of S . For example, a maximal subset of independent variables in a SAT encoding of a hardware verification prob­ lem is a backdoor for unit propagation, as the other variables' values may be directly determined after setting the indepen­ dent ones [19] .

There are two key questions concerning backdoors:

• What is the size of the backdoor in practical problem instances?
• When taking into account the cost of searching for a backdoor set, can one still obtain an overall computa­ tional advantage in solving the CSP?

We address these two key questions below. We will first show that practical problem instances can have surprisingly small backdoors. In the subsequent section, we show how even by taking into account the cost of searching for a back­ door, one can provably obtain an overall computational ad­ vantage by using the backdoor. As we will see, the magnitude of this improvement is, of course, a function of the size of the backdoor.

3 Size of backdoors

We did an empirical study of the size of backdoors in sev­ eral practical SAT instances, using the SAT solver Satz-rand, a randomized version of Satz [ 16]. Satz incorporates power­ ful variable selection heuristics and an efficient simplification strategy (i.e. , a good sub-solver) . We modified Satz-rand to trace the variables selected for branching, and to keep track of the minimum number of variables that need to be set before Satz-rand's simplification found a satisfying assignment effi­ ciently. (We are currently modifying this procedure to also handle unsatisfiable instances and find strong backdoors.)

1 Observe that any satisfiable CSP has a backdoor of size at most n-1; however, we will see that significantly smaller backdoors arise in practice and give a computational advantage in search.

Table 2 summarizes our results. Our instances are from a variety of domains [18]. These instances are now well within the range of the fastest current solvers, such as Chaff [15]. However, they are non-trivial and cannot be solved with the previous generation of SAT solvers, e.g. Tableau [3]. Clearly, the new solvers are better able to discover and exploit hidden structure, such as small back doors. In fact, as we can see from the table, these instances have fairly tiny backdoors. That is, only a very small fraction of all variables can be used to "un­ lock" a satisfying assignment. We conjecture that such small backdoors occur in many other real-world problem instances.

4 Exploiting backdoors formally

We will analyze three, increasingly powerful strategies: de­ terministic, randomized, and heuristic branching variable se­ lection. The first two are meant to work for any CSP where the instance has a small fraction of backdoor variables, with respect to the sub-solver. The randomized strategy gener­ ally outperforms the deterministic one with high probabil­ ity (1 - 1/n, where n is the number of variables). This reflects the performance gain found in practice when back­ tracking SAT solvers are augmented with randomization [15; 9]. The third strategy yields tighter runtime bounds than the first two, but requires us to assume the existence of a good heuristic for choosing backdoor variables (which we find to be the case in practice).

4.1 Deterministic strategy

The deterministic procedure may be construed as a gener­ alization of iterative deepening that runs over all possible search trees of each depth. We assume the algorithm has access to a particular sub-solver A running in T(n) (poly­ nomial) time, which defines the backdoor variables, and C is an arbitrary CSP instance.

Algorithm 4.1 Given a CSP C with n variables,

For all subsets S of then variables with lSI = i,

Perform a standard backtrack search (just on the vari­ ables in S} for an assignment that results in C being solved by sub-solver A.

An analogous algorithm works for finding and exploiting strong backdoors in a CSP to prove unsatisfiability: simply keep track of whether all assignments to the variables in S result in C being a contradiction (as determined by A). All of the following we will say holds for strong backdoors and unsatisfiable CSPs under this modified algorithm.

Note the procedure uses only polynomial time for CSPs with a constant sized backdoor. We are interested in the case where a backdoor of size B(n) exists, for some B(n) < n/2 almost everywhere. The following gives a simple runtime bound in terms of n and B ( n).

Theorem 4.1 If C has a variable domain of size d and a backdoor of size at most B ( n ), then Algorithm 4. 1 runs in O(p(n)( B(~~/2 )B(n)) time,for some polynomial p(n).

Proof. The runtime is bounded by T(n) L~~) (7)di (re­ call T(n) is a runtime bound on A). Since B(n) < n/2, "L:~J~)- 1 (7)::; q(n)( 8 (n)) forsomepolynomialq(n) . This and L~~)- 1 di ::; dB(n) imply that the runtime is domi­ nated by the last term of the sum. Putting it together, the bound is T(n) L~~) (7)di ::; T(n)q(n)( 8 (n))dB(n) :::; (d n)B(n) (d n)B(n) T(n)q(n) ~(n)! :S p(n) B(~)B(n) / 2 asymptotically, for p(n) = T(n) · q(n). D

The theorem implies that when small backdoors (or strong backdoors) are present, a substantial speedup almost always results. For example:

In our exposition of heuristic branching variable selection, we will see an improvement on this (a poly-time bound). For a visual representation of the deterministic strategy's runtime, when d = 2 and backdoors of size n/k are considered, see Figure I. This graph also indicates the following corollary in the case of SAT (proof omitted):

Corollary 4.2 For Boolean formulas with a backdoor of size at most n/ 4.404, Algorithm 4. I solves the formula in 0( en) time, where c < 2.

As we have seen in the previous section, in practice, back­ doors can be quite tiny c~ 1/566 = 0.18% of the variables, for logistics. d. cnf). Therefore, these results have real bearing on the improved solvability of real-world CSPs.

4.2 Randomized strategy

Better performance results from adding randomization. This speed-up formally verifies a well-known fact about real-world solvers: augmenting a solver with randomization can dramat­ ically improve performance [9; 10].

Again, we assume a sub-solver A is on tap, with runtime T(n). Let B(n) be a poly-time computable function on N that bounds the backdoor size, and b be a parameter to be later determined. The idea is to repeatedly choose random subsets of variables that are larger than B ( n), searching these subsets for a backdoor.

Algorithm 4.2 Given a CSP C with n variables,

Repeat n( (n/B(n)- 1 ) )B(n) times (and at least once)· (b-1) .

Randomly choose a subset S of the n variables, of size b · B(n). Perform a standard backtrack search on variables in S. If C is ever solvable by A, return the satisfying assignment.

As before, an analogous algorithm works for general (sat­ isfiable or unsatisfiable) CSPs with strong backdoors: if every leaf in the search tree ends with A reporting unsatisfiability, then the C is unsatisfiable.

The algorithm as stated requires a priori knowledge of B(n). This may be corrected by choosing a constant a > 1, then running the algorithm assuming a backdoor of size 1. If that fails, run it again assuming a backdoor of size a, then a 2 , a 3 , etc., until a solution to C is found.

Theorem 4.2 If C has a backdoor of size B(n), Algorithm 4.2 finds a satisfying assignment with probability approach­ ing I.

Proof. Given there is a B(n)-sized backdoor in C, the probability that a randomly chosen S of size j ~ B( n ), j < n contains the entire backdoor is at least

Setting j = b · B(n) , the probability that backtracking re-( \ B(n) suits in A finding a solution is at least (b1t.)ic~g·)) I =

( (n/~tnV- 1 ) )B(n), due to the self-reducibility property of A. Repeating this experiment n( (n(~~';))- 1 ) )B(n) times, the al­ gorithm succeeds with probability at least 1 - 1/n. D

One can show that the algorithm runs in 0 ( max{l n( (n( B(n)-l) )B(n) }db-B(n)T(n)l time It ' (b-1) . remains to choose b to minimize this expression. As b depends directly on B(n), we evaluate two natural cases for B(n).

• When B( n) = k log n for some constant k, the runtime is n((n((klog(n))- 1 ))klognnb·k' for some constant k' For (b-1) . large k', the runtime is optimized when b is constant; it is ( Io~ n )O(Iog n), an improvement over the deterministic bound.
• When B(n) = njk for some constant k, we can show h ..... d h b ~ ]" . t e runtime IS mm1m1ze w en = I+ln(d), resu tmg m a O(dn/k·(Hln(d))/ln(d) (ln(d)(k- l)t/k) time bound. For example, when d = 2 (the case of SAT), b = k/2.443 and the following holds.

Corollary 4.3 For Boolean formulas with at most n/2.443 backdoor variables, Algorithm 4.2 solves the formula in O(cn) time, wherec < 2.

In the Corollary, cis a function of k. See Figure 1.

·

4.3 Heuristic strategy

So far, we have considered general systematic and ran­ domized search strategies for finding and exploiting back­ doors. However, practical combinatorial solvers generally use heuristics to guide the variable selection process. As noted in the introduction, a common principle is to first branch on variables that simplify an instance the most. In effect, this means such heuristics steer the variable choice towards variables in a backdoor set. We will now formally analyze such heuristic guidance.

Restart Strategies for Heuristic Search. By incorporat­ ing the notion of a variable choice heuristic into our frame­ work, our results are further sharpened. We consider the case where a randomized depth-first search (DFS) solver with a sub-solver A is running on an instance C having a backdoor of size B. The solver chooses variables to branch on accord­ ing to a heuristic H, which has a success probability of at least 1 j h of choosing a backdoor variable at any point in the search. We will use the notation (DFS,H,A) to denote a solver with the above properties.

Informally, a restart strategy is simply a policy that restarts a solver after running it for a specified amount of time, until a solution is found. Our main result here gives a condition under which a polynomial time restart strategy exists for DFS solving CSPs with small backdoors.

Theorem 4.3 If the size of a backdoor of a CSP C is B :::;

Io;,~!I~g d for some constant c, then (DFS,H ,A) has a restart strategy that solves C in polynomial time.

Proof. Since the probability of choosing a backdoor vari­ able is at least 11 h, the probability that we consecutively choose them is 1l h 8 . The probability of choosing the cor­ rect solution with only a polynomial amount of backtracking in the DFS is at least 1ldB-klogn for some constant k. Sup­ pose 1ldB- klogn ·1lh 8 ::=: 1lne, for some constant e. Then by restarting the solver after every TA ( n) steps (where TA ( n) is the runtime of A), there is 1lne probability in each run that the backdoor will be found within a O(nk) amount of back­ tracking, and set correctly. From this one can show that the above inequality holds precisely when B :::; Io;~!I:gd for some constant c. D

An analogous result holds for strong backdoors. It turns out that the given bound on B is asymptotically tight; we will not prove that here. When the variable domain size is constant (e.g. SAT, 3-coloring, etc.), we have the following. Let f be any poly-time computable function on the natural numbers.

Corollary 4.4 Given CSPs with a 0( Io~j~)) backdoor for which H has success probability 11 f(n), (DFS,H,A) has a polynomial time restart strategy.

When the success probability is constant, then CSPs with O(log n) backdoors can be solved using a polynomial time restart strategy on (DFS,H,A) . This result is the best possible in terms of backdoor size, as it would take super-polynomial time to search for a solution among w(log n) backdoor vari­ ables. The heuristic search runtime when B(n) = nlk is sti ll exponential, but this exponential drops dramatically as nl k decreases, even when compared to the previous two al­ gorithms. That is, the runtime is on the order of cnfk, where c = d · 1 I h (recall d is the domain size and 1 I h is success probability) .

Formal Discovery of Heavy-Tails in Heuristic Search. We briefly outline our theoretical results connecting the heuristic search model described earlier with heavy-tailed runtime phenomena found empirically [9]. It was conjec­ tured that "critically constrained" variables were a cause of the heavy-tailed behavior. We can prove that small sets of backdoor variables lead to runtime profiles that are bounded from below by heavy-tails.

The analysis that achieves this result introduces a self­ similar binary tree structure, which we call a variable choice tree. Such trees recursively model a heuristic's selection of backdoor variables; as more backdoor variables are chosen, the resulting search cost is much lower. It turns out that back­ tracking solvers with variable choice heuristics can be mod­ eled precisely by these variable choice trees, when the size of a backdoor in the instance is small. Analysis of these trees leads to the following:

Theorem 4.4 (Heavy-tail/ower bound) If the backdoor size of an CSP C is o( nl log n ), then the runtime distribution of (DFS,A,H) on C is lower-bounded by a Pareto-Levy distri­ bution, when the success probability of H is constant.

5 Conclusions

We have formalized the idea of backdoor variables in CSP/SAT instances. Backdoor variables can be used to sig­ nificantly reduce the search needed in solving CSP/SAT prob­ lems. We showed that practical instances can have surpris­ ingly small backdoors. We also provided a detailed formal analysis demonstrating that one can obtain a concrete com­ putational advantage by exploiting such backdoors.