6.1.2 Complexity of Sequence Generation

Let graph G have n nodes, indegree of non-source nodes between d_min and d_max, and label size between l_min and l_max. For simplicity of analysis, we will assume that l_min = l_max = l and d_min = d_max = d (l = d = 2 for a grid graph).

Let us first compute the size of the pebbling formula associated with G. The running time of PebSeq1UIP and the size of the branching sequence generated will be given in terms of this size. The number of clauses in the pebbling formula Pbl_G is roughly nl^d. Taking clause sizes into account, the size of the formula, | Pbl_G|, is roughly n(l + d )l^d. Note that the size of the CNF formula itself grows exponentially with the indegree and gets worse as label size increases. The best case is when G is the grid graph, where | Pbl_G| = $\Theta$(n). This explains the degradation in performance of zChaff, both original and modified, as we move from grid graphs to random graphs (see section 6.3). Since we construct Pbl_G^SAT by deleting exactly one randomly chosen clause from Pbl_G (see Section 2.5), the size | Pbl_G^SAT| of the satisfiable version is also essentially the same.

Let us now compute the running time of PebSeq1UIP. Initial computation of heights and predecessor sorting takes time $\Theta$(nd log d ). Assuming n_u unit clause labeled nodes and n_t target nodes, the remaining node sorting time is $\Theta$(n_ulog n_u + n_tlog n_t). Since PebSubseq1UIPWrapper is called at most once for each node, the total running time of PebSeq1UIP is $\Theta$(nd log d + n_ulog n_u + n_tlog n_t + nT_wrapper), where T_wrapper denotes the running time of PebSubseq1UIP- Wrapper without taking into account recursive calls to itself. When n_u and n_t are much smaller than n, which we will assume as the typical case, this simplifies to $\Theta$(nd log d + nT_wrapper). If T(v, i) denotes the running time of PebSubseq1UIP(v,i), again without including recursive calls to the wrapper method, then T_wrapper = T(v, d ). However, T(v, d )= lT(v, d - 1) + $\Theta$(l ), which gives T_wrapper = T(v, d )= $\Theta$(l^d+1). Substituting this back, we get that the running time of PebSeq1UIP is $\Theta$(nl^d+1), which is about the same as | Pbl_G|.

Finally, we consider the size of the branching sequence generated. Note that for each node, most of its contribution to the sequence is from the recursive pattern generated near the end of PebSubseq1UIP. Let Q(v, i) denote this contribution. Q(v, i) = (l - 2)(Q(v, i - 1) + $\Theta$(l )), which gives Q(v, i) = $\Theta$(l^d+2). Hence, the size of the sequence generated is $\Theta$(nl^d+2), which again is about the same as | Pbl_G|.

Theorem 3   Given a pebbling graph G with label size at most l and indegree of non-source nodes at most d, algorithm PebSeq1UIP produces a branching sequence $\sigma$ of size at most S in time $\Theta$(dS), where S = | Pbl_G| $\approx$ | Pbl_G^SAT|. Moreover, the sequence $\sigma$ is complete for Pbl_G as well as for Pbl_G^SAT under any clause learning algorithm using fast backtracking and 1UIP learning scheme (such as zChaff).

Proof. The size and running time bounds follow from the previous discussion in this section. That this sequence is complete can be verified by a simple hand calculation simulating clause learning with fast backtracking and 1UIP learning scheme.$\Box$