grams. The properties of elementary loops and HEF programs studied here may be useful in improving the computation of disjunctive answer set solvers, such as claspd3**(Drescher et al. 2008),** cmodels **(Lierler 2005),** dlv4**(Leone et al. 2006),** and gnt5**(Janhunen et al. 2006).**
The outline of this paper is as follows. In Section 2, we present our reformulated definition of an elementary loop of a nondisjunctive program and provide a corresponding refinement of the theorem on loop formulas, as well as some properties of elementary loops. These results are extended to disjunctive programs in Section 3.

In Section 4, we introduce the class of HEF programs and show that **their shifted** variants preserve stable models. In Section 5, we generalize the notion of inherent tightness to HEF programs. An operational characterization of stable models of HEF programs is presented in Section 6. Finally, Section 7 concludes the paper.

This paper is an extended version of the conference papers (Gebser et al. 2006)
and (Gebser et al. 2007).6

## 2 Nondisjunctive Programs

After providing the relevant background on nondisjunctive programs, this section introduces elementary loops of nondisjunctive programs. We further refine elementary loops to elementarily unfounded sets, yielding a syntactic characterization of minimal unfounded sets. Moreover, we show that elementary loops **of nondisjunctive** programs can be recognized in polynomial time. (The statements of **the theorems** and the propositions in this section which apply to nondisjunctive programs will be generalized to disjunctive programs or HEF programs in later sections and the proofs will be given there.) Finally, we compare our reformulation of elementary loops with the definition by Gebser and Schaub (2005).

## 2.1 Background

A *nondisjunctive rule* **is an expression of the form**
a1 ← a2, . . . , am, not am+1 , . . . , not an (1)
where n ≥ m ≥ 1 and a1, . . . , an are propositional atoms. A *nondisjunctive program* is a finite set of nondisjunctive rules.

We will identify a nondisjunctive rule (1) with the propositional formula

$$a_{2}\land\cdots\land a_{m}\land\neg a_{m+1}\land\cdots\land\neg a_{n}\;\to\;a_{1}\ ,$$
a2 ∧ · · · ∧ am ∧ ¬am+1 ∧ · · · ∧ ¬an → a1 , (2)
and will often write (1) as $\frac{1}{2}$
$$\left(2\right)$$
$$a_{1}\;\leftarrow\;B,F$$
$$\left({\boldsymbol{3}}\right)$$
a1 ← B, F (3)