Abstract
In this extended abstract, we discuss the use of iteratively-supported formulas (ISFs) as a basis for computing strongly-supported models for Kleene Answer Set Programs (ASP\(^{K}\)). ASP\(^{K}\) programs have a syntax identical to classical ASP programs. The semantics of ASP\(^{K}\) programs is based on the use of Kleene three-valued logic and strongly-supported models. For normal ASP\(^{K}\) programs, their strongly supported models are identical to classical answer sets using stable model semantics. For disjunctive ASP\(^{K}\) programs, the semantics weakens the minimality assumption resulting in a classical interpretation for disjunction. We use ISFs to characterize strongly-supported models and show that they are polynomially bounded.
Access provided by Autonomous University of Puebla. Download conference paper PDF
Similar content being viewed by others
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:
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:
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.
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\);
-
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:
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:
Definition 7
By the iteratively-supported formula for a normal ASP\(^{K}\) program \(\varPi \) we understand the following formula of classical propositional calculus:
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:
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.
References
Chan, P.: A possible world semantics for disjunctive databases. IEEE Trans. Knowl. Data Eng. 5(2), 282–292 (1993)
Doherty, P., Szałas, A.: Stability, supportedness, minimality and kleene answer set programs. In: Eiter, T., Strass, H., Truszczyński, M., Woltran, S. (eds.) Advances in Knowledge Representation. LNCS, vol. 9060, pp. 125–140. Springer, Heidelberg (2015)
Ferraris, P., Lifschitz, V.: On the minimality of stable models. In: Balduccini, M., Son, T.C. (eds.) Logic Programming, Knowledge Representation, and Nonmonotonic Reasoning. LNCS, vol. 6565, pp. 64–73. Springer, Heidelberg (2011)
Gebser, M., Kaufmann, B., Neumann, A., Schaub, T.: clasp: a conflict-driven answer set solver. In: Baral, C., Brewka, G., Schlipf, J. (eds.) LPNMR 2007. LNCS (LNAI), vol. 4483, pp. 260–265. Springer, Heidelberg (2007)
Gelfond, M., Kahl, Y.: Knowledge Representation, Reasoning, and the Design of Intelligent Agents -The Answer-Set Programming Approach. Cambridge University Press, Cambridge (2014)
Lee, J., Lifschitz, V.: Loop formulas for disjunctive logic programs. In: Palamidessi, C. (ed.) ICLP 2003. LNCS, vol. 2916, pp. 451–465. Springer, Heidelberg (2003)
Leone, N., Pfeifer, G., Faber, W., Eiter, T., Gottlob, G., Perri, S., Scarcello, F.: The DLV system for knowledge representation and reasoning. ACM Trans. Comput. Log. 7(3), 499–562 (2006)
Lierler, Y.: cmodels – SAT-based disjunctive answer set solver. In: Baral, C., Greco, G., Leone, N., Terracina, G. (eds.) LPNMR 2005. LNCS (LNAI), vol. 3662, pp. 447–451. Springer, Heidelberg (2005)
Lifschitz, V.: Thirteen definitions of a stable model. In: Blass, A., Dershowitz, N., Reisig, W. (eds.) Fields of Logic and Computation. LNCS, vol. 6300, pp. 488–503. Springer, Heidelberg (2010)
Lifschitz, V., Razborov, A.: Why are there so many loop formulas? ACM Trans. Comput. Log. 7(2), 261–268 (2006)
Lin, F., Zhao, J.: On tight logic programs and yet another translation from normal logic programs to propositional logic. In: Gottlob, G., Walsh, T. (eds.) Proceedings of the IJCAI-03, pp. 853–858. Morgan Kaufmann (2003)
Lin, F., Zhao, Y.: ASSAT: computing answer sets of a logic program by SAT solvers. Artif. Intell. 157(1–2), 115–137 (2004)
Liu, G., Janhunen, T., Niemelä, I.: Answer set programming via mixed integer programming. In: Brewka, G., T., E., McIlraith, S. (eds.) Proceedings of the KR 2012. AAAI Press (2012)
Pelov, N., Ternovska, E.: Reducing inductive definitions to propositional satisfiability. In: Gabbrielli, M., Gupta, G. (eds.) ICLP 2005. LNCS, vol. 3668, pp. 221–234. Springer, Heidelberg (2005)
Sakama, C., Inoue, K.: An alternative approach to the semantics of disjunctive logic programs and deductive databases. J. Autom. Reasoning 13(1), 145–172 (1994)
Simons, P., Niemelä, I., Soininen, T.: Extending and implementing the stable model semantics. Artif. Intell. 138(1–2), 181–234 (2002)
Soininen, T., Niemelä, I.: Developing a declarative rule language for applications in product configuration. In: Gupta, G. (ed.) PADL 1999. LNCS, vol. 1551, pp. 305–319. Springer, Heidelberg (1999)
Son, T., Pontelli, E.: A constructive semantic characterization of aggregates in answer set programming. TPLP 7(3), 355–375 (2007)
Acknowledgments
This work is partially supported by the Swedish Research Council (VR) Linnaeus Center CADICS, the ELLIIT network organization for Information and Communication Technology, the Swedish Foundation for Strategic Research (CUAS Project, SymbiKCloud Project), the EU FP7 project SHERPA (grant agreement 600958), and Vinnova NFFP6 Project 2013-01206.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing AG
About this paper
Cite this paper
Doherty, P., Kvarnström, J., Szałas, A. (2016). Iteratively-Supported Formulas and Strongly Supported Models for Kleene Answer Set Programs. In: Michael, L., Kakas, A. (eds) Logics in Artificial Intelligence. JELIA 2016. Lecture Notes in Computer Science(), vol 10021. Springer, Cham. https://doi.org/10.1007/978-3-319-48758-8_36
Download citation
DOI: https://doi.org/10.1007/978-3-319-48758-8_36
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-48757-1
Online ISBN: 978-3-319-48758-8
eBook Packages: Computer ScienceComputer Science (R0)