1 Introduction

Classical answer set programming, ASP, has been intensively studied during the past three decades [3, 5, 9]. In addition, a great deal of attention has been devoted to ASP implementations [4, 7, 8, 12, 16]. One of the prominent techniques proposed earlier for computing answer sets is based on translating ASP programs into classical propositional formulas and then applying SAT solvers to generate answer sets. In [6, 12] it is shown that Clark’s completion together with loop formulas characterize answer sets for ASP programs. One of the obstacles in characterizing answer sets using propositional formulas is their \(\varSigma ^P_2\) complexity. Loop formulas contribute to this because one may require exponentially many of them [10]. The current extended abstract provides an alternative to loop formulas, iteratively-supported formulas, that ameliorates this problem. Polynomial translations of normal ASP programs have also been considered in [11, 13, 14]. However, our translation is extended to disjunctive programs in a natural way.

In [15] a possible model semantics for disjunctive programs is proposed. It is formulated with the use of split programs and there can be exponentially many of them comparing to the original program. Similar semantics was independently proposed in [1] under the name of the possible world semantics. In [2] we have analyzed minimality and supportedness in the context of ASP s and proposed Kleene Answer Set Programs (ASP\(^{K}\)) using the concept of strongly supported models. The semantics used for Kleene Answer Set programs is based on Kleene logic, \(K_3\), with an extra weak negation. In [2] it is shown that the problem of showing whether an ASP\(^{K}\) program has a strongly supported model is in NP (i.e., in \(\varSigma ^P_1\)). This result applies to both normal and disjunctive ASP\(^{K}\) programs. For disjunctive ASP\(^{K}\) programs, the minimality assumption is relaxed, resulting in a classical interpretation of disjunction.Footnote 1 The ability to fine-tune the separation of supportedness and minimality in the disjunctive case results in a lower complexity for generating strongly supported models. In comparison to [15], ASP\(^{K}\) programs allow for strong negation and a three-valued model-theoretic semantics is provided. The presence of both default and strong negation in ASP\(^{K}\) provides a tool to close the world locally in a contextual manner, more flexible than possible model negation proposed in [15]. Though defined independently and using different foundations, both semantics appear compatible on positive programs, so the results of the current paper apply to possible model semantics of [15], too.

The main contribution of the current paper is the definition and use of ISFs to characterize strongly supported models for both normal and disjunctive ASP\(^{K}\) programs. Such formulas are shown to be polynomially bounded in both cases. As a derivative result, in the case of normal ASP programs and due to a correspondence between answer sets and strongly supported models, ISFs provide a more efficient alternative to loop formulas when using SAT solvers. For disjunctive ASP\(^{K}\) programs, the use of supported models and ISFs provide an efficient means for using SAT solvers, but with an alternative semantics that interprets disjunction classically due to a relaxation of minimality assumptions.

The paper is structured as follows. In Sect. 2 we introduce basic definitions related to both classical ASP programs and ASP\(^{K}\) programs in addition to strong supportedness. Section 3 introduces ISFs used to characterize normal and disjunctive ASP\(^{K}\) programs. Section 4 concludes the paper.

2 Kleene Answer Set Programs

In this paper, the syntax for Kleene ASP\(^{K}\) programs is identical for that of classical ASP programs. The semantics for Kleene ASP\(^{K}\) programs is based on the use of a three-valued Kleene logic \(K_3\) and strongly-supported models presented in [2]. The semantics for classical ASP programs is based on stable model semantics [9]. For the sake of clarity we consider propositional programs only. Truth values are denoted by T (true), F (false) and U (unknown). The empty conjunction is T and the empty disjunction is F.

Definition 1

By a positive literal (or an atom) we mean any propositional variable of \(\mathcal{P} \). A negative literal is an expression of the form \(\lnot r\), where \(r\in \mathcal{P} \). A classical literal is a positive or a negative literal. A set of literals is consistent if it does not contain a literal \(\ell \) together with its negation \(\lnot \ell \).Footnote 2 By an extended literal we understand a classical literal or an expression of the form \( not \,\ell \), where \(\ell \) is a classical literal. If \(\gamma \) is an expression (formula, program, etc.) then \({ Lit (\gamma )} \!\mathop {=}\limits ^{\mathrm {def}}\!\{p,\!\lnot p\mid p\!\in \!\mathcal{P} \text{ occurs } \text{ in } \gamma \}\) and \(\mathcal{P} (\varPi )\mathop {=}\limits ^{\mathrm {def}}\mathcal{P} \cap { Lit (\varPi )} \).

An interpretation is a finite consistent set of literals. Interpretation I satisfies a classical literal \(\ell \) iff \(\ell \in I\) and I satisfies an extended literal \( not \,\ell \) iff \(\ell \not \in I\). The satisfiability relation is denoted by \(I\models \ell \).\(\vartriangleleft \)

Definition 2

By an ASP\(^{K}\) rule we understand an expression \(\varrho \) of the form:

$$\begin{aligned} \begin{array}{l} \ell _1\vee \ldots \vee \ell _k\leftarrow \ell _{k+1},\ldots ,\ell _m, not \,\ell _{m+1},\ldots , not \,\ell _n,\\ \end{array} \end{aligned}$$
(1)

where \(n\ge m\ge k\ge 0\), \(\ell _1,\ldots ,\ell _k,\ell _{k+1},\ldots , \ell _m, \ell _{m+1},\ldots \ell _n\) are (positive or negative) literals. The expression at the lefthand side of ‘\(\leftarrow \) ’ in (1), denoted by \(h(\varrho )\), is called the head and the righthand side of ‘\(\leftarrow \)’, denoted by \(B(\varrho )\), is called the body of the rule. The rule is called disjunctive if \(k>1\).

An ASP\(^{K}\) program \(\varPi \) is a finite set of rules. A program is normal if each of its rules has at most one literal in its head. If a program contains a disjunctive rule, we call it disjunctive. By \( Disj (\varPi )\) we denote the set of disjunctive rules appearing in \(\varPi \).

The set of rules with the empty body is denoted by \( Fct (\varPi )\) and the set of rules with the empty head is denoted by \( Ctr (\varPi )\). Members of \( Fct (\varPi )\) and \( Ctr (\varPi )\) are called facts and constraints, respectively. The set of rules whose bodies and heads are nonempty is denoted by \( Rul (\varPi )\).

An interpretation I satisfies a rule \(\varrho \) of the form (1), denoted by \(I\models \varrho \), if whenever \(\ell _{k+1},\ldots , \ell _m\in I\) and \(\ell _{m+1},\ldots , \ell _n\not \in I\), we have \(\ell _i\in I\) for some \(1\le i\le k\). An interpretation I satisfies an ASP\(^{K}\) program \(\varPi \), denoted by \(I\models \varPi \), if for all rules \(\varrho \in \varPi \), \(I\models \varrho \). \(\vartriangleleft \)

The following definition is needed to define strong supportedness (a construction similar in spirit is considered in [18]).

Definition 3

Given interpretations I and J, the value of a formula A w.r.t. (I, J), denoted by (I, J)(A), is defined as follows:

$$\begin{aligned} (I,J)(A)\mathop {=}\limits ^{\mathrm {def}}\left\{ \begin{array}{ll} \text{ T } &{} \text{ when } I\models reduct^J(A);\\ \text{ F } &{} \text{ when } I\models reduct^J(\lnot A);\\ \text{ U } &{} \text{ otherwise. } \end{array} \right. \end{aligned}$$
(2)

where \(reduct^J(A)\) (respectively, \(reduct^J(\lnot A)\)) is a formula obtained from A (\(\lnot A\)) by substituting subformulas of the form \( not \,\ell \) by their truth values evaluated in J.\(\vartriangleleft \)

Definition 4

An interpretation N is a strongly supported model of an ASP\(^{K}\) program \(\varPi \) provided that N satisfies \(\varPi \) and there exists a sequence of interpretations \(I_0\subseteq I_1\subseteq \ldots \subseteq I_n\) where \(n\ge 0\) such that \(I_0= Fct (\varPi )\), \(N=I_n\), and:

  1. 1.

    for every \(1\le i\le n\) and every rule \(\ell _1\vee \ldots \vee \ell _k\leftarrow B\) of \(\varPi \),

if \(\big (I_{i-1},N\big )(B)=\text{ T } \) then a nonempty subset of \(\{\ell _1,\ldots ,\ell _k\}\)

is included in \(I_i\);

  1. 2.

    for \(i=1,\ldots ,n\), \(I_i\) can only contain literals obtained by applying point 1.\(\vartriangleleft \)

3 Iteratively-Supported Formulas

Let p be a propositional variable. Then \(p_i\) (respectively \(\bar{p}_i\)) denotes the fact that in the i-th iteration, p (respectively, \(\lnot p\)) is in the computed candidate for a strongly supported model. Thus, \(\lnot p_i\) (respectively \(\lnot \bar{p}_i\)) denotes the fact that in the i-th iteration \(p_i\) (respectively, \(\lnot p_i\)) is not in the computed candidate for a strongly supported model.

The number of different literals in heads of \( Rul (\varPi )\) is denoted by \(\#\varPi \). Since support can only be generated for up to \(\#\varPi \) distinct literals, \(\#\varPi \) iterations will be sufficient to provide support for all literals in any strongly supported model.

Definition 5

The translation function is defined as follows, where \(1\le i\le \#\varPi \) and \(\ell \) is an extended literal:

$$\begin{aligned} Tr _{\varPi }({i},\ell ) \mathop {=}\limits ^{\mathrm {def}}\left\{ \begin{array}{ll} p_i &{} \text{ when } \ell =p;\\ \bar{p}_i &{} \text{ when } \ell =\lnot p;\\ \lnot p_{\#\!\varPi } &{} \text{ when } \ell = not \,p;\\ \lnot \bar{p}_{\#\!\varPi } &{} \text{ when } \ell = not \,\lnot p. \end{array} \right. \end{aligned}$$
(3)

We extend the translation for bodies and heads of rules by setting:

      \( Tr _{\varPi }({i},B) \mathop {=}\limits ^{\mathrm {def}}\bigwedge _{\ell \in B} Tr _{\varPi }({i},\ell ) \) and \(\displaystyle Tr _{\varPi }({i},H) \mathop {=}\limits ^{\mathrm {def}}\bigvee _{\ell \in H} Tr _{\varPi }({i},\ell ) \).

Definition 6

By a support of a classical literal \(\ell \) in a normal ASP\(^{K}\) program \(\varPi \) at i (\(i>0\)) we understand the formula:

$$\begin{aligned} \begin{array}{l} Supp _{\varPi }^{i}(\ell ) \mathop {=}\limits ^{\mathrm {def}}\big [ Tr _{\varPi }({i},\ell ) \equiv \; \big ( Tr _{\varPi }({i-1},\ell ) \; \vee \displaystyle \bigvee _{\varrho \in \varPi : \ell = h(\varrho )}\!\!\!\! Tr _{\varPi }({i-1},B(\varrho )) \big )\;\big ]. \end{array} \end{aligned}$$
(4)

Definition 7

By the iteratively-supported formula for a normal ASP\(^{K}\) program \(\varPi \) we understand the following formula of classical propositional calculus:

$$\begin{aligned} \displaystyle ISF (\varPi ) \mathop {=}\limits ^{\mathrm {def}}&\displaystyle \! \bigwedge _{0\le i\le \#\varPi }\;\;\bigwedge _{p\in \mathcal{P} (\varPi )}\lnot \big (p_i\wedge \bar{p}_i\big )\;\wedge \end{aligned}$$
(5)
$$\begin{aligned}&\displaystyle \!\!\! \bigwedge _{F\in Fct (\varPi )}\!\!\! Tr _{\varPi }({0},h(F)) \;\;\wedge \!\!\!\!\bigwedge _{\ell \in { Lit (\varPi )}-\{h(F)\mid F\in Fct (\varPi )\}}\!\!\!\!\!\!\!\!\!\!\!\!\!\! \lnot Tr _{\varPi }({0},\ell ) \;\wedge \end{aligned}$$
(6)
$$\begin{aligned}&\!\!\bigwedge _{1\le i\le \#\varPi }\bigwedge _{\ell \in { Lit (\varPi )}} Supp _{\varPi }^{i}(\ell ) \;\wedge \end{aligned}$$
(7)
$$\begin{aligned}&\;\;\bigwedge _{\varrho \in \varPi }\big ( Tr _{\varPi }({\#\varPi },B(\varrho )) \rightarrow Tr _{\varPi }({\#\varPi },h(\varrho )) \big ). \end{aligned}$$
(8)

We have the following theorem for normal ASP\(^{K}\) programs.

Theorem 1

For any normal ASP\(^{K}\) program \(\varPi \), I is a strongly supported model of \(\varPi \) iff there is a valuation v satisfying \( ISF (\varPi ) \) such that:

       \(I=\{p\mid v(p_{\#\varPi })=\text{ T } \}\cup \{\lnot p\mid v(\bar{p}_{\#\varPi })=\text{ T } \}\). \(\vartriangleleft \)

Since for normal ASP\(^{K}\) programs strongly supported models are also classical answer sets, Theorem 1 applies to classical ASP, too.

Given a disjunctive ASP\(^{K}\) program \(\varPi \), the support of literals appearing only in non-disjunctive heads remains unchanged. For literals appearing in disjunctive heads we have the following definition.

Definition 8

By a support of a classical literal \(\ell \) occurring in a disjunctive head in an ASP\(^{K}\) program \(\varPi \) at i (\(i>0\)) we understand the formula:

$$\begin{aligned} \begin{array}{ll} \displaystyle Supp _{\varPi }^{i}(\ell ) \mathop {=}\limits ^{\mathrm {def}}&{} \displaystyle \big [ Tr _{\varPi }({i},\ell ) \rightarrow \; \big ( Tr _{\varPi }({i-1},\ell ) \; \vee \!\!\!\! \bigvee _{\varrho \in \varPi : \ell \in h(\varrho )}\!\!\!\!\!\! Tr _{\varPi }({i-1},B(\varrho )) \,\big )\,\big ]\,\wedge \\ &{}\big [ Tr _{\varPi }({i-1},\ell ) \;\rightarrow Tr _{\varPi }({i},\ell ) \,\big ]. \end{array} \end{aligned}$$
(9)

For other literals, the support of \(\ell \) is still specified by formula (4) in Definition 6. \(\vartriangleleft \)

Definition 9

By an iteratively-supported formula for a disjunctive ASP\(^{K}\) program \(\varPi \) we understand the formula (7) with \( Supp _{\varPi }^{i}() \) understood as in Definition 8.\(\vartriangleleft \)

We now have the following generalization of Theorem 1.

Theorem 2

For any (normal or disjunctive) ASP\(^{K}\) program \(\varPi \), I is a strongly supported model of \(\varPi \) iff there is a valuation v satisfying \( ISF (\varPi ) \) such that:

       \(I=\{p\mid v(p_{\#\varPi })=\text{ T } \}\cup \{\lnot p\mid v(\bar{p}_{\#\varPi })=\text{ T } \}\). \(\vartriangleleft \)

Note that for any ASP\(^{K}\) program \(\varPi \), the number of different literals in heads of \( Rul (\varPi )\) (i.e., \(\#\varPi \)) is linear in the size of \(\varPi \). Therefore we have the following lemma.

Lemma 1

For any (normal or disjunctive) ASP\(^{K}\) program \(\varPi \), the size of \( ISF (\varPi )\) is polynomial in the size of \(\varPi \).\(\vartriangleleft \)

4 Conclusions

In this extended abstract, we have defined iteratively-supported formulas expressed in classical propositional logic and used them to characterize strongly supported models for ASP\(^{K}\) programs. For normal ASP\(^{K}\) programs, I is a classical answer set of the program iff I is a strongly supported model of the program. Since iteratively-supported formulas provide polynomially bounded characterizations of supported models for normal ASP\(^{K}\) programs, they also provide polynomially bounded characterizations of classical answer sets for normal ASP programs. In contrast, use of loop formulas could result in formulas of exponential size for normal ASP programs.

ISFs also characterize strongly supported models for disjunctive ASP\(^{K}\) programs and guarantee that all conclusions are grounded in facts or default reasoning based on extended literals (using default negation \( not \,\)). Additionally, due to a weakened minimization assumption, disjunction is interpreted classically which results in a semantics enjoying among other properties, a \(\varSigma ^P_1\) complexity for computing strongly-supported models. This, together with a polynomial bound on ISFs, is a striking theoretical improvement compared to the \(\varSigma ^P_2\) complexity of computing classical answer sets for ASP programs.