6.2 Solving GT_n Formulas

While pebbling formulas are not so easy to solve by popular SAT solvers, they are inherently not too difficult for clause learning algorithms. In fact, even without any learning, they admit tree-like proofs under a somewhat stronger related proof system, RES(k), for large enough k:

Proposition 6 (Esteban et al. 2002)   Pbl_G has a size O(| G|) tree-like RES(k) refutation, where k is the maximum width of a clause labeling a node of G. In particular, when G is a grid graph with n nodes, Pbl_G has an O(n) size tree-like RES(2) refutation.

Here RES(k) denotes the extension of RES that allows resolving, instead of clauses, disjunctions of conjunctions of up to k literals (Krajíek, 2001). RES(1) is simply RES. Proposition 6 implies that addition of natural extension variables corresponding to k-conjunctions of variables of Pbl_G leads to O(| G| ^. k) size tree-like resolution proofs of related pebbling formulas Pbl_G(k) (Atserias and Bonet, 2002).

For GT_n formulas, however, no such short tree-like proofs are known in RES(k) for any k. Reusing derived clauses (equivalently, learning clauses with DPLL) seems to be the key to finding short proofs of GT_n. This makes them a good candidate for testing clause learning based SAT solvers. Our experiments indicate that GT_n formulas, despite their simplicity, are quite hard for default zChaff. Using a good branching sequence based on the ordering structure underlying these formulas leads to significant performance gains. Recall that PebSeq1UIP was a fairly complex algorithm that generated a perfect branching sequence for randomized pebbling graphs. In contrast, the branching sequence we give below for GT_n formulas is generated by a nearly trivial algorithm. It is an incomplete sequence (see Definition 4) but boosts performance in practice.