2.5 Pebbling Formulas

Pebbling formulas are unsatisfiable CNF formulas whose variations have been used repeatedly in proof complexity to obtain theoretical separation results between different proof systems (Ben-Sasson, 2000, Beame et al., 2003a). The version we will use in this paper is known to be easy for regular resolution but hard for tree-like resolution, and hence for DPLL without learning (Ben-Sasson, 2000). We use these formulas to show how one can utilize problem structure to allow clause learning algorithms to handle much bigger problems than they otherwise can.

Pebbling formulas represent the constraints for sequencing a system of tasks that need to be completed, where each task can be accomplished in a number of alternative ways. The associated pebbling graph has a node for each task, labeled by a disjunction of variables representing the different ways of completing the task. Placing a pebble on a node in the graph represents accomplishing the corresponding task. Directed edges between nodes denote task precedence; a node is pebbled when all of its predecessors in the graph are pebbled. The pebbling process is initialized by placing pebbles on all indegree zero nodes. This corresponds to completing those tasks that do not depend on any other.

Formally, a Pebbling formula Pbl_G is an unsatisfiable CNF formula associated with a directed, acyclic pebbling graph G (see Figure 1). Nodes of G are labeled with disjunctions of variables, i.e. with clauses. A node labeled with clause C is thought of as pebbled under a (partial) variable assignment $\sigma$ if C|_$\sigma$ = TRUE. Pbl_G contains three kinds of clauses - precedence clauses, source clauses and target clauses. For instance, a node labeled (x₁ $\vee$ x₂) with three predecessors labeled (p₁ $\vee$ p₂ $\vee$ p₃), q₁ and (r₁ $\vee$ r₂) generates six precedence clauses ($\neg$p_i $\vee$ $\neg$q_j $\vee$ $\neg$r_k $\vee$ x₁ $\vee$ x₂), where i $\in$ {1, 2, 3}, j $\in$ {1} and k $\in$ {1, 2}. The precedence clauses imply that if all predecessors of a node are pebbled, then the node itself must also be pebbled. For every indegree zero source node s of G, Pbl_G contains the clause labeling s as a source clause. Thus, Pbl_G implies that all source nodes are pebbled. For every outdegree zero target node of G labeled, say, (t₁ $\vee$ t₂), Pbl_G has target clauses $\neg$t₁ and $\neg$t₂. These imply that target nodes are not pebbled, and provide a contradiction.

Figure 1: A general pebbling graph with distinct node labels, and a 4-layer grid pebbling graph

Grid pebbling formulas are based on simple pyramid-shaped layered pebbling graphs with distinct variable labels, 2 predecessors per node, and disjunctions of size 2 (see Figure 1). Randomized pebbling formulas are more complicated and correspond to random pebbling graphs. In this paper, we only consider pebbling graphs where no variable appears more than once in any node label. In general, random pebbling graphs allow multiple target nodes. However, the more the targets, the easier it is to produce a contradiction because we can focus only on the (relatively smaller) subgraph under the lowest target. Hence, for our experiments, we add a simple grid structure at the top of randomly generated pebbling formulas to make them have exactly one target.

All pebbling formulas with a single target are minimally unsatisfiable, i.e. any strict subset of their clauses admits a satisfying assignment. For each formula Pbl_G we use for our experiments, we also use a satisfiable version of it, called Pbl_G^SAT, obtained by randomly choosing a clause of Pbl_G and deleting it. When G is viewed as a task graph, Pbl_G^SAT corresponds to a task system with a single fault, and finding a satisfying assignment for it corresponds to locating the fault.