6.3 Experimental Results

We conducted experiments on a Linux machine with a 1600 MHz AMD Athelon processor, 256 KB cache and 1024 MB RAM. Time limit was set to 6 hours and memory limit to 512 MB; the program was set to abort as soon as either of these was exceeded. We took the base code of zChaff (Moskewicz et al., 2001), version 2001.6.15, and modified it to incorporate a branching sequence given as part of the input, along with a CNF formula. When an incomplete branching sequence is specified that gets exhausted before a satisfying assignment is found or the formula is proved to be unsatisfiable, the code reverts to the default variable selection scheme VSIDS of zChaff. For consistency, we analyzed the performance with random restarts turned off. For all other parameters, we used the default values of zChaff. For all formulas, results are reported for DPLL (zChaff with clause learning disabled), for CL (unmodified zChaff), and for CL with a specified branching sequence (modified zChaff).

Table 1: zChaff on grid pebbling formulas. denotes out of memory.

Grid formula Runtime in seconds

Solver Layers Variables Unsatisfiable Satisfiable

5 30 0.24 0.12

DPLL 6 42 110 0.02

7 56 > 6 hrs 0.07

8 72 > 6 hrs > 6 hrs

CL 20 420 0.12 0.05

(unmodified 40 1,640 59 36

zChaff) 65 4,290 47

70 4,970

CL + 100 10,100 0.59 0.62

branching 500 250,500 254 288

sequence 1,000 1,001,000 4,251 5,335

1,500 2,551,500 21,097

Table 2: zChaff on randomized pebbling formulas with distinct labels, indegree $\le$5, and disjunction label size $\le$6. denotes out of memory.

Randomized pebbling formula Runtime in seconds

Solver Nodes Variables Clauses Unsatisfiable Satisfiable

9 33 300 0.00 0.00

DPLL 10 29 228 0.58 0.00

10 48 604 > 6 hrs > 6 hrs

CL 50 154 3,266 0.91 0.03

(unmodified 87 296 9,850 65

zChaff) 109 354 11,106 584 0.78

110 354 18,467

CL + 110 354 18,467 0.28 0.29

branching 4,427 14,374 530,224 48 49

sequence 7,792 25,105 944,846 181 > 6 hrs

13,324 43,254 1,730,952 669 249

Table 3: zChaff on GT_n formulas. denotes out of memory.

GT_n formula Runtime in seconds

Solver n Variables Clauses Unsatisfiable Satisfiable

8 62 372 1.05 0.34

DPLL 9 79 549 48.2 0.82

10 98 775 3395 248

11 119 1,056 > 6 hrs 743

CL 10 98 775 0.20 0.00

(unmodified 13 167 1,807 93.7 7.14

zChaff) 15 223 2,850 1492 0.01

18 322 5,067

CL + 18 322 5,067 0.52 0.13

branching 27 727 17,928 701 0.17

sequence 35 1,223 39,900 3.6 0.15

45 2,023 86,175 0.81

Tables 1 and 2 show the performance on grid pebbling and randomized pebbling formulas, respectively. In both cases, the branching sequence used was generated by Algorithm 1, PebSeq1UIP, and the size of problems that can be solved increases substantially as we move down the tables. Note that randomized pebbling graphs typically have a more complex structure than grid pebbling graphs. In addition, higher indegree and larger disjunction labels make both the CNF formula size as well as the required branching sequence larger. This explains the difference between the performance of zChaff, both original and modified, on grid and randomized pebbling instances. For all instances considered, the time taken to generate the branching sequence from the input graph was significantly less than that for generating the pebbling formula itself.

Table 3 shows the performance on the GT_n formulas using the branching sequence given in Figure 5. As this sequence is incomplete, the solver had to revert back to zChaff's VSIDS heuristic to choose variables to branch on after using the given branching sequence as a guide for the first few decisions. Nevertheless, the sizes of problems that could be handled increased significantly. The satisfiable versions proved to be relatively easier, with or without a specified branching sequence.