hidden in Π, one 
an see that red∗(Π) ≡v Π. Hen
e, even though there is a bije
tive orresponden e between the stable models of EPHPn+1 n and red∗(EPHPn+1 n ) =
PHPn+1 n , red∗
auses a superpolynomial blow-up in the length of proofs in ASP-T
and the related solvers, if applied before a tually proving EPHPn+1 n .

## 6 Experiments

```
We experimentally evaluate how well 
                        urrent state-of-the-art ASP solvers 
                                              an make
                                                   

use of the additional stru
                        ture introdu
                                    ed to programs using the extension rule. For
                                                                             

```

the experiments, we ran the solvers 7smodels (Simons et al. 2002) (version 2.33, a widely used lookahead solver), clasp (Gebser et al. 2007) (version 1.1.0, with many

```
te
 hniquesin
          luding 
                oni
                   t learningadopted from DPLL-based SAT solvers),
                                                        

```

and cmodels (Giun
higlia et al. 2006) (version 3.77, a SAT-based ASP solver run-

```
ning the 
        oni
             t-learning SAT solver zCha (Moskewi
                                                 z et al. 2001) version 2007.3.12
                                                                             

```

as the ba k-end). The experiments were run on standard PCs with 2-GHz AMD

3200+ pro essors under Linux. Running times were measured using /usr/bin/time.

First, we investigate whether ASP solvers are able to benet from the extension in EPHPn+1 n. We 
ompare the number of de
isions and running times of ea
h of the solvers on PHPn+1 n, CPHPn+1 n = PHPn+1 n ∪S1<l≤n EXTl, and EPHPn+1 n. By Theorem 5.2 the solvers should in theory be able to exhibit polynomially s aling numbers of de isions for EPHPn+1 n. In fa
t with 
oni
t-learning this might also be possible for CPHPn+1 n due to the tight 
orresponden
e with 
oni
t-learning SAT solvers and RES (Beame et al. 2004). The results for n = 10 **. . .** 12 are shown

```
in Table 1. While the number of de
                                        isions for the 
                                                        oni
                                                              t-learning solvers clasp

```

and cmodels is somewhat redu
ed by the extensions, the solvers do not seem to be

```
7 We note that the detailed results reported here dier somewhat from those reported in the
                                                                                                
  onferen
           e version of this work (Järvisalo and Oikarinen 2007). This is due to the fa
                                                                                      t that, for
                                                                                                

the 
    urrent arti
               le, we used more re
                                   ent versions of the solvers.
                                                            

```

| n        | with timeout (-) of 2 hours.   |          |           |           |          |           |           |
|----------|--------------------------------|----------|-----------|-----------|----------|-----------|-----------|
| Time (s) | De isions                      |          |           |           |          |           |           |
| Solver   | n                              | PHPn+1 n | CPHPn+1 n | EPHPn+1 n | PHPn+1 n | CPHPn+1 n | EPHPn+1 n |
| smodels  | 10                             | 34.02    | 119.69    | 8.65      | 164382   | 144416    | 0         |
| smodels  | 11                             | 486.44   | 1833.48   | 21.70     | 1899598  | 1584488   | 0         |
| smodels  | 12                             | -        | -         | 49.28     | -        | -         | 0         |
| clasp    | 10                             | 6.81     | 7.29      | 10.05     | 337818   | 216894    | 38863     |
| clasp    | 11                             | 58.48    | 45.00     | 82.07     | 1840605  | 882393    | 203466    |
| clasp    | 12                             | 579.28   | 509.43    | 941.23    | 12338982 | 6434939   | 1467623   |
| cmodels  | 10                             | 1.60     | 1.69      | 7.87      | 8755     | 8579      | 12706     |
| cmodels  | 11                             | 8.20     | 8.51      | 43.96     | 24318    | 23758     | 42782     |
| cmodels  | 12                             | 46.33    | 54.26     | 122.72    | 88419    | 94917     | 88499     |
