2.6 The GT_n Formulas

The GT_n formulas are unsatisfiable CNF formulas based on the ordering principle that any partial order on the set {1, 2,..., n} must have a maximal element. They were first considered by Krishnamurthy (1985) and later used by Bonet and Galesi (2001) to show the optimality of the size-width relationship of resolution proofs. Recently, Alekhnovich et al. (2002) used a variation, called GT'_n, to show an exponential separation between RES and regular resolution.

The variables of GT_n are x_{i, j} for i, j $\in$ [n], i$\ne$j, which should be thought of as the binary predicate i $\succ$ j. Clauses ($\neg$x_{i, j} $\vee$ $\neg$x_{j, i}) ensure that $\succ$ is anti-symmetric and ($\neg$x_{i, j} $\vee$ $\neg$x_{j, k} $\vee$ x_{i, k}) ensure that $\succ$ is transitive. This makes $\succ$ a partial order on [n]. Successor clauses ( $\vee_{{k \ne j}}^{}$ x_{k, j}) provide the contradiction by saying that every element j has a successor in [n] $\setminus$ {j}, which is clearly false for the maximal elements of [n] under the ordering $\succ$.

These formulas, although capturing a simple mathematical principle, are empirically difficult for many SAT solvers including zChaff. We employ our techniques to improve the performance of zChaff on these formulas. We use for our experiments the unsatisfiable version GT_n described above as well as a satisfiable version GT_n^SAT obtained by deleting a randomly chosen successor clause. The reason we consider these ordering formulas in addition to seemingly harder pebbling formulas is that the latter admit short tree-like proofs in certain extensions of RES whereas the former seem to critically require reuse of derived or learned clauses for short refutations. We elaborate on this in Section 6.2.