implementability problem of asynchronous automata, and particular formalizations of classical mutual exclusion and dining philosophers problems (Heljanko and Stefänescu 2004; Heljanko and Stefänescu 2005). These programs involve no hidden atoms and both positive and negative interdependencies of atoms occur. The extremely high numbers of rules (2406357) and modules (101819) are clearly reflected in running times perceived for mutex9 . However, the respective rates of 4 and 10 modules per second do not differ too much from those obtained for ephp-13 given the fact that the nmber of rules is about 25 times higher. The data observed for phi3 is analogous to those obtained for ephp-13 and mutex9 but the respective modules-per-second rates are much higher: approximately 90 and 2000. This may partly boil down to the fact phi3 is the smallest program under consideration and it has also the smallest nmber of rules per module ratio.

Our last benchmark program, seq 4 -ss 4 , is taken from benchmark sets of (Brain et al. 2006)
where the optimization of machine code using ASP techniques is of interest. The program in question formalizes the optimization of a particular sequence of four SPARC-v7 instructions. This program instance has the greatest modules as regards the number of rules—the average number of rules per module varies from about 350 to 11200 depending on the module type. It has also hidden atoms which makes a difference between modules based on plain SCCs and their combinations induced by the dependencies caused by the use of hidden atoms. The respective modules-per-second rates 28, 19, and 5 are all better than 4 obtained for mutex3.

To provide the reader with a better idea of sizes of individual modules, we have collected some numbers about their distribution in Table 2. Each program involves a substantial number of modules with just one rule each of which defines a single atom of interest. On the other hand, the largest SCCs for ephp-13, mutex3, phi3, and seq4-ss4 involve 949, 2091912, 2579, and 1071689 rules, respectively. For mutex3, the biggest module consists of a definition of an equivalence relation over states in the verification domain—creating a huge set of positively interdependent atoms.

For ephp-13, the greatest module is a collection of nogoods which can be shown to have no stable models in roughly 99500 seconds using smodels (version 2.32).

However, the remaining rules of ephp-13 make this fact much faster to prove: only 61 seconds elapse.

A few concluding remarks follow. Increasing the number of modules in a program tends to decrease the number of modules that can be decomposed per time unit.

This observation suggests that the creation of the zipfile has a quadratic flavor although modules themselves can be figured out in linear time (using a variant of Tarjan's algorithm). Perhaps this can be improved in the future by better integrating the creation of the zipfile into modlist. For now, it creates a shell script for this purpose. Handling the biggest program instances is also subject to the effects of memory allocation which may further slow down computations. On the other hand, the cost of increasing the number of rules in modules seems to be relatively small. Moreover, it is clear on the basis of data given in Table 1 that the composition of programs is faster than decomposition. This would not be the case if the old version of LPCAT were used for composition. Last, we want to emphasize that MODLIST and LPCAT have been implemented as supplementary tools that are not directly related