6.1 Solving Pebbling Formulas

As a first step toward our grand goal of translating theoretical understanding into effective implementations, we show, using pebbling problems as a concrete example, how one can utilize high level problem descriptions to generate effective branching strategies for clause learning algorithms. Specifically, we use insights from our theoretical analysis to give an efficient algorithm to generate an effective branching sequence for unsatisfiable as well as satisfiable pebbling formulas (see Section 2.5). This algorithm takes as input the underlying pebbling graph (which is the high level description of the pebbling problem), and not the CNF pebbling formula itself. As we will see in Section 6.3, the generated branching sequence gives exponential empirical speedup over zChaff for both grid and randomized pebbling formulas.

zChaff, despite being one of the current best clause learners, by default does not perform very well on seemingly simple pebbling formulas, even on the uniform grid version. Although clause learning should ideally need only polynomial time to solve these problem instances (in fact, linear time in the size of the formula), choosing a good branching order is critical for this to happen. Since nodes are intuitively pebbled in a bottom up fashion, we must also learn the right clauses (i.e. clauses labeling the nodes) in a bottom up order. However, branching on variables labeling lower nodes before those labeling higher ones prevents any DPLL based learning algorithm from backtracking the right distance and proceeding further in an effective manner. To make this clear, consider the general pebbling graph of Figure 1. Suppose we branch on and set d₁, d₂, d₃ and a₁ to FALSE. This will lead to a contradiction through unit propagation by implying a₂ is TRUE and b₁ and b₂ are both FALSE. We will learn (d₁ $\vee$ d₂ $\vee$ d₃ $\vee$ $\neg$a₂) as the associated 1UIP conflict clause and backtrack. There will still be a contradiction without any further branches, making us learn (d₁ $\vee$ d₂ $\vee$ d₃) and backtrack. At this stage, we will have learned the correct clause but will be stuck with two branches on d₁ and d₂. Unless we had branched on e₁ before branching on the variables of node d, we will not be able to learn e₁ as the clause corresponding to the next higher pebbling node.