1. positive dependencies only, 2. positive dependencies and hidden atoms, and 3. both positive and negative dependencies as well as hidden atoms.

The number of modules created by modlist decreases in this order. However, our benchmarks cover program instances that get split in tens of thousands of modules. To tackle the problem of storing such numbers of modules in separate files we decided to use file compression and packaging tools and, in particular, the ZIP
utility available in standard Linux installations. We found ZIP superior to TAR as it allows random access to files in an archive, or a zipfile . This feature becomes valuable when the modules are accessed from the archive for further processing.

The tool for program composition has been named as LPCAT which refers to the concatenation of files containing logic programs. A new version of the tool was implemented for experiments reported below for better performance as well as usability. The old version (version 1.8) is only able to combine two modules at a time which gives a quadratic nature for a process of combining n modules together: modules are added one-by-one to the composition. The new version, however, is able to read in modules from several files and, even more conveniently, a stream of modules from an individual file. The ZIP facility provides an option for creating such a stream that can then be forwarded for LPCAT for composition. This is the strategy for composing programs in experiments that are described next.

To test the performance of our tools, we picked a set of benchmark instances having from tens of thousands up to millions of rules—expressed in the smodels format. For each instance, the first task is to decompose the instance into modules using modlist and to create a zipfile containing the modules. The type of modules to be created is varied according the three schemes summarized above. The second task is to recreate the benchmark instance from a stream of modules extracted from the respective zipfile. As suggested above, the actual composition is carried out using LPCAT and we also check that the number of rules matches with the original instance. Due to high number of rules, checking the equivalence of the original and composed programs (Janhunen and Oikarinen 2007) is unfeasible in many cases. If all atoms are visible, this can be accomplished syntactically on the basis of sorted textual representations of the programs involved. To ensure that modlist and LPCAT produce correct (de)compositions of programs, such a check was performed for all compositions created for the first three benchmarks which involve no hidden atoms. As regards computer hardware, we run MODLIST and LPCAT on a PC with a 1.8GHz Intel Core 2 Duo CPU and 2GBs of main memory—operating under the Linux 2.6.18 system. In experimental results collected in Table 1, we report the sum of user and system times that are measured with the /usr/bin/time command.

There are three benchmark types ( bt for short) as enumerated in the beginning of this section. We refer to them using the respective abbreviations +, +h, and ±h.

The first benchmark instance in Table 1, viz. ephp-13 , is a formalization (Järvisalo and Oikarinen 2007)
of the classical pigeon hole principle for 13 pigeons—extended by redundant rules in analogy to Tseitin's extended resolution proof system. This program can be deemed medium-sized within our benchmarks. There are no hidden atoms, no positive re-