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).
|
|
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 GTn 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.