6.1.1 Automatic Sequence Generation: PebSeq1UIP

Algorithm 1, PebSeq1UIP, describes a way of generating a good branching sequence for pebbling formulas. It works on any pebbling graph G with distinct label variables as input and produces a branching sequence linear in the size of the associated pebbling formula. In particular, the sequence size is linear in the number of variables as well when the indegree as well as label size are bounded by a constant.

PebSeq1UIP starts off by handling the set U of all nodes labeled with unit clauses. Their outgoing edges are deleted and they are treated as pseudo sources. The procedure first generates a branching sequence for non-target nodes in U in increasing order of height. The key here is that when zChaff learns a unit clause, it fast-backtracks to decision level zero, effectively restarting at that point. We make use of this fact to learn these unit clauses in a bottom up fashion, unlike the rest of the process which proceeds top down in a depth-first way.

PebSeq1UIP now adds branching sequences for the targets. Note that for an unsatisfiability proof, we only need the sequence corresponding to the first (lowest) target. However, we process all targets so that this same sequence can also be used when the formula is made satisfiable by deleting enough clauses. The subroutine PebSubseq1UIP runs on a node v, looking at its i^th predecessor u in increasing order by height. No labels are output if u is the lowest predecessor; the negations of these variables will be indirectly implied during clause learning. However, it is recursed upon if not previously visited. This recursive sequence results in learning something close to the clause labeling this lowest node, but not quite that exact clause. If u is a higher predecessor (it will be marked as visitedAsHigh), PebSubseq1UIP outputs all but one variables labeling u. If u is not a source and has not previously been visited as high, the last label is output as well, and u recursed upon if necessary. This recursive sequence results in learning the clause labeling u. Finally, PebSubseq1UIP generates a recursive pattern, calling the subroutine with the next lower predecessor of v. The precise structure of this pattern is dictated by the 1UIP learning scheme and fast backtracking used in zChaff. Its size is exponential in the degree of v with label size as the base.

The Grid Case. It is insightful to look at the simplified version of the sequence generation algorithm that works only for grid pebbling formulas. This is described below as Algorithm 2, GridPebSeq1UIP. Note that both predecessors of any node are at the same level for grid pebbling graphs and need not be sorted by height. There are no nodes labeled with unit clauses and there is exactly one target node t, simplifying the whole algorithm to a single call to PebSubseq1UIP(t,2) in the notation of Algorithm 1. The last for loop of this procedure and the recursive call that follows it are now redundant. We combine the original wrapper method and the calls to PebSubseq1UIP with parameters (v, 2) and (v, 1) into a single method GridPebSubseq1UIP with parameter v.

The resulting branching sequence can actually be generated by a simple depth first traversal (DFS) of the grid pebbling graph, printing no labels for the nodes on the rightmost path (including the target node), both labels for internal nodes, and one arbitrarily chosen label for source nodes. However, this resemblance to DFS is a somewhat misleading coincidence. The resulting sequence diverges substantially from DFS order as soon as label size or indegree of some nodes is changed. For the 10 node depth 4 grid pebbling graph shown in Figure 1, the branching sequence generated by the algorithm is h₁, h₂, e₁, e₂, a₁, b₁, f₁, f₂, c₁. Here, for instance, b₁ is generated after a₁ not because it labels the right (second) predecessor of node e but because it labels the left (first) predecessor of node f. Similarly, f₁ and f₂ appear after the subtree rooted at h as left predecessors of node i rather than as right predecessors of node h.

Example for the General Case. To clarify the general algorithm, we describe its execution on a small example. Let G be the pebbling graph in Figure 4. Denote by t the node labeled (t₁ $\vee$ t₂), and likewise for other nodes. Nodes c, d, f and g are at height 1, nodes a and e at height 2, node b at height 3, and node t at height 4. U = {a, b}. The edges (a, t) and (b, t) originating from these unit clause labeled nodes are removed, and t, with no predecessors anymore, is added to the list of sources. We output the label of the non-target unit nodes in U in increasing order of height, and recurse on each of them in order, i.e. we output a₁, setting B = (a₁), call PebSubseq1UIPWrapper on a, and then repeat this process for b. This is followed by a recursive call to PebSubseq1UIPWrapper on the target node t.

Figure 4: A simple pebbling graph to illustrate branch sequence generation

The call PebSubseq1UIPWrapper on a in turn invokes PebSubseq1UIP with parameters (a, 2). This sorts the predecessors of a in increasing order of height to, say, d, c, with d being the lowest predecessor. v is set to a and u is set to the second predecessor c. We output all but the last label of u, i.e. of c, making the current branching sequence B = (a₁, c₁). Since u is a source, nothing more needs to be done for it and we make a recursive call to PebSubseq1UIP with parameters (a, 1). This sets u to d, which is the lowest predecessor and requires nothing to be done because it is also a source. This finishes the sequence generation for a, ending at B = (a₁, c₁). After processing this part of the sequence, zChaff will have a as a learned clause.

We now output b₁, the label of the unit clause b. The call, PebSubseq1UIPWrapper on b, proceeds similarly, setting predecessor order as (d, f, e), with d as the lowest predecessor. Procedure PebSubseq1UIP is called first with parameters (b, 3), setting u to e. This adds all but the last label of e to the branching sequence, making it B = (a₁, c₁, b₁, e₁, e₂). Since this is the first time e is being visited as high, its last label is also added, making B = (a₁, c₁, b₁, e₁, e₂, e₃), and it is recursed upon with PebSubseq1UIPWrapper(e). This recursion extends the sequence to B = (a₁, c₁, b₁, e₁, e₂, e₃, f₁). After processing this part of B, zChaff will have both a and (e₁ $\vee$ e₂ $\vee$ e₃) as learned clauses. Getting to the second highest predecessor f of b, which happens to be a source, we simply add another f₁ to B. Finally, we get to the third highest predecessor d of b, which happens to be the lowest as well as a source, thus requiring nothing to be done. Coming out of the recursion, back to u = f, we generate the pattern given by the last for loop, which is empty because the label size of f is only 2. Coming out once more of the recursion to u = e, the for loop pattern generates e₁, f₁ and is followed by a call to PebSubseq1UIP with the next lower predecessor f as the second parameter, which generates f₁. This makes the current sequence B = (a₁, c₁, b₁, e₁, e₂, e₃, f₁, f₁, e₁, f₁, f₁). After processing this, zChaff will also have b as a learned clause.

The final call to PebSubseq1UIPWrapper with parameter t doesn't do anything because both predecessors of t were removed in the beginning. Since both a and b have been learned, zChaff will have an immediate contradiction at decision level zero. This gives us the complete branching sequence B = (a₁, c₁, b₁, e₁, e₂, e₃, f₁, f₁, e₁, f₁, f₁) for the pebbling formula Pbl_G.