Stable models of logic programs have been studied and characterized also in comparison with other formalisms by many researchers. As already argued, such characterizations are interesting for many reasons, including the possibility of leading to new algorithms for computing stable models. In this paper we provide a simple characterization of stable models which can be seen as the proof-theoretic counterpart of the standard model-theoretic definition. We show how it can be naturally encoded in diference logic. Our encoding, compared to the existing reductions to classical logics, does not explicitly rely on a previous computation of Clark's completion, and it does not involve any Boolean variable.
studied and characterized also in comparison with other formalisms by many researchers, given its widespread use to solve application problems, even in an industrial setting [8, 9, 10, 11, 12, 13, 14]. As already argued (see, e.g., [15]), such characterizations are interesting for many reasons, including the possibility of leading to new algorithms for computing stable models.
In this paper we introduce stable derivations as a new characterization of stable models and show how it can be naturally encoded in diference logic, i.e., in quantifier free first order formulas whose atoms have the form
( ◁▷ + ), where and are variables ranging over the reals/rationals or the integers, ◁▷∈ {=, ̸=, ≤ , <, ≥ , >} and is a numeric constant. While this is neither the first alternative to the standard definition of stable models (see, e.g., [15]) nor the first reduction to diference logic (see, e.g., [16]),
Let be a countable set of atoms. By ⊥ we mean the set obtained adding the atom ⊥ denoting falsity to , i.e., ⊥ = ∪ {⊥}. A rule is an expression of the form ←
1, . . . , , ¬+1, . . . , ¬
(0 ≤ ≤ ) where , 1, . . . , are atoms in ⊥ and ¬ is the symbol for negation. We assume
that in (
Consider a logic program Π . A (truth) assignment is a subset of the set of atoms, thus not containing ⊥. A truth assignment satisfies 1. an atom if ∈ , 2. a negated atom ¬ if ̸∈ ,
suitable concept , we write |= to mean that satisfies .
Π by considering each rule ∈ Π of the form (
Π = {ℎ() ← +() : ∈ Π , ∩ − () = ∅}.
.
Example 1. Consider the program Π in the three atoms , , whose rules are:
(
Such definition of stable model is due to [ 4] and has the property that each stable model of Π is a supported model of Π , i.e., for each atom ∈ ⊥, ∈ if and only if there exists a rule ∈ Π such that ℎ() = and |= (). Thus, all the stable models are also supported while the converse is not necessarily true [18]. [19] proved that also the converse is true if Π is tight, i.e., if the positive dependency graph of Π
2. an edge from to each atom 1, . . . , for each rule (
Theorem 1 ([19]). Let Π be a program. A stable model of Π is also a supported model of Π , and if Π is tight then a supported model of Π is also a stable model of Π .
with the models of the Clark’s completion (Π) [17]. Assuming Π is finite, the Clark’s completion
(Π) of Π is defined to be the set of formulas in propositional logic consisting of
(
Note that (
and, in the latter case, (
[20] and later [21] generalized Fages’ [19] result to programs Π tight on a set ⊆ of atoms, defined as the programs for which there exists a function Π mapping each atom in to an ordinal such that for each rule in Π , if satisfies the head and the body of the rule then, for each atom in the positive body of the rule, (ℎ()) > (). A program is tight according to Fages’ [19] definition, if it is tight on every set of atoms.
Theorem 2 ([21]). Let Π be a program. Let be a supported model of Π . If Π is tight on then is a stable model of Π .
Example 2. Consider the rules in (
, :∈Π,ℎ()= ∈() ¬ ⋁︁ ⋀︁
:∈Π,ℎ()=⊥ ∈() ≡ ¬ , ≡ ,
¬. ≡ ( ∨ ¬), ≡ , ≡ ,
If Π consists of the last three rules in (
If Π consists of all the rules in (
order to rule out the supported models which are not stable, see for instance [22, 23, 24].
work. Other related works are briefly discussed in Section 6.
Janhunen [25] proved that in order to rule out the models of the completion which are not stable, it is suficient to add suitable level ordering constraints. For any truth assignment ⊆ , define the set of supporting rules of to be Π = { ∈ Π : |= ()}. Given an assignment , a level numbering of for Π is a function Π : ∪ Π ↦→ N such that for each atom ∈ , () = { () : ∈ Π , ℎ() = } and, for each rule ∈ Π ,
() = {0, { () : ∈ +()}} + 1.
Theorem 3 ([25]). Let Π be a program. Let be a supported model of Π . is a stable model of Π if and only if there exists a level numbering of for Π .
numbering, and also showed –assuming is finite– how to encode level numbering in propositional logic using ⌈2(| |+2)⌉ bits. Thanks to Theorem 3, there exists a one-one-correspondence between the stable models of Π and the models of the set (Π) of propositional formulas consisting of the encoding of the level numbering and of (Π) . (Π) has (| |×⌈ 2(| |)⌉)) Boolean variables and size (||Π || × 2(| |)).
A few years later, Niemelä [16] introduced level ranking of an assignment for Π to be a function Π : ↦→ N such that for each atom ∈ , there exists a rule ∈ Π such that ℎ() = and for each atom ∈ +(), () ≥ () + 1. [16] also showed that if we add the restrictions to level rankings saying that for each ∈ 1. () = 1 whenever there is a rule ∈ Π with ℎ() = and +() = ∅, and 2. for every rule ∈ Π with ℎ() = and +() ̸= ∅, there exists ∈ +() with () ≤ () + 1, then we have a one-to-one correspondence between level ranking and level numbering. Level rankings satisfying such additional restrictions are said to be strong.
Theorem 4 ([16]). Let Π be a program. Let be a supported model of Π . is a stable model of Π if and only if there exists a (strong) level ranking of for Π .
Like level numbering, for each supported model , there is at most one strong level ranking. The strong level ranking can be thus used to produce compact encodings in propositional logic as in [25], but without the need of encoding the level associated to the rules.
(Strong) level rankings can be encoded in diference logic, defined as the extension to propositional logic in which the set of atomic formulas is extended in order to allow for expressions of the form ◁▷ +, where and are variables ranging over a numeric unbounded domain (usually the integers or the rationals/reals), is a numeric constant and ◁▷∈ {=, ̸=, ≤ , <, ≥ , >}. Then, an interpretation maps each numeric variable to a value in its domain, and satisfies an atomic formula ◁▷ + if () ◁▷ () + 1. Thanks to Theorem 4, the stable models of Π can be computed as the models 1It is possible to distinguish between rational/real diference logic and integer diference logic ; in the former, variables take values in the rationals/reals while in the latter case variables are assumed to take integer values. The distinction is useful as, e.g., the satisfiability of 0 < − < 1 depends on the domain of and . However, in this paper such distinction is useless since we are going to consider formulas whose satisfiability does not depend on the chosen domain. of (Π) , where (Π) is the set of formulas in diference logic consisting of (Π) and of the encoding of the (strong) level ranking. (Π) has | | Boolean variables, | | numeric variables and size (||Π ||), though the introduction of additional Boolean variables may produce a more compact encoding, but still in (||Π ||).
Example 3. Let Π be the set rules in (
The formulas encoding the additional conditions on strong level ranking are → (¬ ∨ () ≤ () + 1) ∧ ( ∨ () = (⊤)), → ¬ ∨ () ≤ () + 1,
→ () ≤ () + 1,
where (⊤) is a “dummy" variable necessary in order to respect the syntax of diference logic and whose
intended interpretation is 1. The encoding in diference logic of the strong level ranking corresponds to the
formulas in (
As expected, strong level rankings (like level numbering) are unique: each atom in the stable model has a uniquely associated level, while the constraints say nothing about the value of the variables associated to the atoms not belonging to the stable model, in this case ().
based on the strongly connected components (SCCs) of the positive dependency graph associated to Π , and [26] show how it is possible to encode (strong) level rankings (also exploiting SCCs) in SAT modulo acyclicity.
Consider a program Π . A stable derivation is a function Π mapping each atom ∈ ⊥ to an ordinal such that () < (⊥) if and only if there exists a rule ∈ Π with head and 1. for each atom ∈ +(), () > (), and 2. for each atom ∈ − (), () ≥ (⊥).
Given a stable derivation Π, the set of atoms stably derived by Π is { : () < (⊥)}. A set of atoms is stably derivable (from Π) if there exists a stable derivation of . From the above definitions, it immediately follows that, in a stable derivation, (⊥) = 0 only if the set of stably derivable atoms is empty.
Example 4. In the case of the logic program (
Theorem 5. Let Π be a program. A set of atoms is a stable model of Π if and only if is stably derivable from Π .
Proof. For the left to right direction, assume is a stable model. We define a stable derivation for Π via the operator Π : 2 ↦→ 2 defined, for an arbitrary program Π , as
Π() = {ℎ() : ∈ Π , |= ()}, and considering the following sequence of subsets of and, for each ≥ 0,
Π↑0= ∅, Π↑+1= Π(Π↑).
Now, since is a stable model of Π , for each ∈ there is a unique such that ∈ Π ↑ ∖Π ↑− 1, and we set () = if ∈ Π ↑ ∖Π ↑− 1. For ̸∈ , we set () = (⊥) = , the first limit ordinal. Then, = Π ↑ and for each ∈ , () < (⊥) if ∈ . Clearly, Π is a stable derivation for Π : if () = < then ∈ Π ↑ ∖Π ↑− 1 and thus there exists a rule ∈ Π such that () for each ∈ +(), ∈ Π ↑− 1 and thus () < (), and () for each ∈ − (), ̸∈ and thus () = (⊥) = .
For the right to left direction, suppose there is a stable derivation Π for Π . We show that
= { : () < (⊥)} is the minimal model of Π , which implies that is a stable model of
Π . We first show that is a model of Π . Assume it is not. Then, there exists a rule of the form
(
The term “stable derivation" has been used given () the analogy with the standard definition of derivation in classical logic, and () the correspondence, as established by Theorem 5, with stable models. Indeed, a stable derivation can be seen as a sequence of applications of rules as in a standard derivation in classical logic, once 1. each rule is interpreted as the inference rule ℎ() ← +() carrying the restriction that the whole derivation must not contain the atoms in − (), and
rule may invalidate the (stability of the) derivation. These two diferences make the stably derivable relation nonmonotonic –while classical logic is indeed monotonic– but thanks to Theorem 5 we have a nice correspondence between the standard “model-theoretic" definition of stable model and this “proof-theoretic" definition of stable derivation, again similarly to what happens in classical logic.
terization of stable models does not assume that the starting assignment is a supported model.
condition > is equivalent to ≥ + 1, it is easy to check the correspondence between the first condition on stable derivation and the condition on level ranking.
atom, the number of stable derivations is, in general, infinite even in the case of finite programs. If we consider two stable derivations 1Π and 2Π to be equivalent if, for each pair of atoms , ∈ ⊥, 1Π() < 1Π() if and only if 2Π() < 2Π(), then, whenever ⊥ is finite, there are finitely many non equivalent stable derivations. It is however still possible that there exists two non equivalent stable derivations having the same set of stably derivable atoms.
Example 5. Consider the logic program Π obtained adding ← ¬ to (
We can thus define a weaker notion of equivalence, and say that two stable derivations are weakly equivalent if they have the same set of stably derivable atoms. Of course, two equivalent stable derivations are also weakly equivalent. Further, similarly to what has been done in [16] for level rankings, we can impose additional restrictions on stable derivations in order to enforce that any two of them are either not weakly equivalent or map ⊥ to a diferent ordinal. We do this by introducing strict stable derivations. A stable derivation is strict if it maps each atom ∈ to an ordinal () such that () ≤ (⊥) and either () = 1 or for each rule ∈ Π with head , 1. either there exists an atom ∈ +() with () ≤ () + 1, or 2. there exists an atom ∈ − () with () < (⊥).
Notice that the above conditions trivially hold when = ⊥ and, thus, in a strict stable derivation they hold for each ∈ ⊥. Further, it is easy to check that in a strict stable derivation, for each ∈ ⊥, () = 0 only if (⊥) = 0 and thus only if the set of stably derived atoms is empty. Theorem 6. Let Π be a program in the set of atoms. For any stable derivation of Π there is a strict stable derivation 1 of Π which is equivalent to and such that 1(⊥) = | | + 1 if is finite, and 1(⊥) = , otherwise. Any two distinct weakly equivalent strict stable derivations of Π difer only in the ordinal associated to ⊥.
Proof. Let be the set of atoms stably derived by . Consider the stable derivation 1 having as stably derived set of atoms constructed in the “left to right" direction of the proof of Theorem 5. By construction 1 is strict, equivalent to and satisfies 1(⊥) = . On the other hand, it is clear that if is finite, then the proof still holds if in the proof we replace = Π ↑ with = Π ↑| |+1 and impose 1(⊥) = | | + 1.
Assume there are two weakly equivalent strict stable derivations 1 and 2 and an atom ∈ with 1() ̸= 2(), and either 1() ̸= 1(⊥) or 2() ̸= 2(⊥). Since 1 and 2 are weakly equivalent then 1() < 1(⊥) and 2() < 2(⊥). Take such atom to be such that for each atom ∈ with 1() ̸= 2(), ( 1(), 2()) ≤ ( 1(), 2()). Assume ( 1(), 2()) = 1() (analogous proof can be done for the other case). Thus, for each atom with 1() < 1(), 1() = 2(). Further, from 1() < 2(), it follows 2() > 1. Then, 1() < 1(⊥), 2() < 2(⊥) and the equivalence between 1 and 2 implies the existence of a rule with ℎ() = and 1. for each ∈ +(), 1() = 2() < 1() < 2(), 2. for each ∈ − (), 1() = 1(⊥) and 2() = 2(⊥), and 3. since 2() > 1, there exists ∈ +(), 1() + 1 = 2() + 1 ≥ 2() > 1() ≥ 1() + 1 which is not possible.
atom ∈ , () ≤ (⊥). However, () ≤ (⊥) is already entailed by the definition of stable derivation for those atoms for which the rule ← ⊥ is in Π .
Consider a finite program Π in a finite set of variables. In the reduction of Π to diference logic
we have a variable () for each atom ∈ ⊥, while the set (Π) of formulas corresponding to
Π consists of the formula
⋁︀:∈Π,=ℎ()(⋀︀∈+()( () > ())∧
⋀︀∈− ()( () ≥ (⊥))),
(
Theorem 7. Let Π be a finite program. A set of atoms is a stable model of Π or, equivalently, is stably derivable from Π if and only if (Π) ∪ ( ) is satisfiable in diference logic.
of stable derivation.
Thus, for the left to right direction, every stable derivation corresponds to an interpretation such that for each atom ∈ with () < (⊥), ( ()) = () and for each atom ∈ with () ≥ (⊥), ( ()) = , where is a value bigger than any value assigned to the variables with () < (⊥). satisfies (Π) ∪ ( ) where is the set of atoms stably derived by .
For the right to left direction, if is a satisfying interpretation of (Π) ∪ ( ), we can put the set of values assigned by in one to one correspondence with the first || ordinals respecting the ordering. Then, if is the function defining the correspondence between the two sets, for each atom ∈ ⊥, define () = ( ( ())). By construction, for each , ∈ ⊥, () ≤ () if and only if ( ()) ≤ ( ()) and, thus, given the correspondence between (Π) and the definition of stable derivation, is a stable derivation in which is the set of atoms stably derived by .
According to the above theorem, stably derivable set of atoms of a program Π can be computed with diference logic solvers. We can also provide the corresponding translation for the al conditions holding for strict stable derivations. However, dificulties arise if we consider variables ranging over the rationals/reals. In fact, in such cases, when () < (⊥) we would like to impose additional conditions forcing () to be the “successor" value of some value () < (), and if () ranges over the rationals/reals there is no such successive value. Further, diference logic does not allow to impose that a given variable is greater or equal than a constant and the set of reals/rationals/integers do not have a minimum value.
A simple solution to all the above problems –providing a translation to the observations of the
previous section– is to modify condition (
Theorem 8. Let Π be a program in a finite set of atoms. For each ∈ , (Π) entails both () ≤ (⊥) and either (⊤) < (⊥) or () = (⊥).
Proof. () ≤ (⊥) is an easy consequence of (
strict stable derivation.
Example 6. Let Π be the set rules in (
Any model of the above formulas satisfies () < () < (⊥) ≤ ().
The formulas in (Π) encoding strict stable derivations are and they entail (⊤) = () = () − 1 < () = (⊥).
The proposed encoding in diference logic of (strict) stable derivations has thus | | + 1 numeric variables and size (||Π ||), as opposed to [16] encoding of (strong) level ranking which require | | Boolean variables and | | numeric variables. Given that we can restrict the range of strict stable derivation in [1, | | + 1] it is also possible to produce a corresponding encoding in propositional logic mimicking what has been done by [25]. Analogously, it is also possible to further improve the encoding by exploiting the strongly connected component of the positive dependency graph and/or provide “SAT modulo acyclity” encodings again mimicking what has been already proposed in the literature, see, e.g., [25, 16, 27, 26].
As mentioned in the Introduction, there have been several characterizations of stable models, with (possibly) corresponding reductions, and some of them are introduced through the paper. Here, we mention some of the main remaining charactizations/reductions to diference logic or other logicbased formalisms other than propositional satisfiability. [ 26] presented alternative target formalisms in which the acyclicity conditions can be checked using a linear representation. The input program is instrumented such that propositional models of its completion subject to an acyclicity condition checked on graph representation match the answer sets of the program. The required acyclicity can be represented as additional SAT formulas, including diference logic [ 27]. Such acyclicity conditions can be also linearly represented via SMT with Bit-Vector Logic [28], where the authors introduced additional constraints for atoms involved in SCCs by considering external and internal support for the rules, and Mixed Integer Programming [29]. [30] presented a reduction of programs with monotone and convex constraints to pseudo-Boolean constraints, based on loop formulas. The approach of [31] is based on a syntactic transformation which turns a logic program into a formula of secondorder logic similar to the formula from the definition of circumscription. Reductions have been also presented for CASP, an extension of ASP with linear constraints [32], but often limited to diference constraints due to their usefulness in, e.g., scheduling applications, in contrast to native approaches to handle such extension natively (e.g., [33] and solver clingo[DL]). Reduction-based approaches include those implemented in ezcsp [34] and ezsmt [35], which rely on CSP and some SMT logics, including diference logic, respectively.
In this paper we strengthen the relation between ASP and classical logic [36, 37] by providing a new, simple proof-theoretic characterization of stable models, and a corresponding reduction from logic programs to diference logic, which does not rely on a previous computation of Clark’s completion, and it does not involve any Boolean variable. As future work, we would like to implement the reduction as SMT formulas, and test it employing SMT solvers for diference logic (see, e.g., [ 38, 39, 40]) on benchmarks from the last ASP Competitions [41], against state-of-the-art ASP solvers such as clingo [42], lp2diff [27], and wasp [43]. Fields of Logic and Computation, Essays Dedicated to Yuri Gurevich on the Occasion of His 70th Birthday, volume 6300 of Lecture Notes in Computer Science, Springer, 2010, pp. 488–503. [16] I. Niemelä, Stable models and diference logic, Annals of Mathematics and Artificial Intelligence 53 (2008) 313–329. [17] K. L. Clark, Negation as failure, in: Logic and data bases, Springer, 1978, pp. 293–322. [18] V. W. Marek, V. S. Subrahmanian, The relationship between stable, supported, default and autoepistemic semantics for general logic programs, Theoretical Computer Science 103 (1992) 365–386. [19] F. Fages, Consistency of clark’s completion and existence of stable models, Methods of Logic in
Computer Science 1 (1994) 51–60. [20] Y. Babovich, E. Erdem, V. Lifschitz, Fages’ theorem and answer set programming, CoRR cs.AI/0003042 (2000). URL: https://arxiv.org/abs/cs/0003042. [21] E. Erdem, V. Lifschitz, Tight logic programs, Theory and Practice of Logic Programming 3 (2003) 499–518. [22] R. Ben-Eliyahu, R. Dechter, Propositional semantics for disjunctive logic programs, Annals of
[23] F. Lin, J. Zhao, On tight logic programs and yet another translation from normal logic programs to propositional logic, in: Proceedings of the Eighteenth International Joint Conference on
[24] F. Lin, Y. Zhao, ASSAT: computing answer sets of a logic program by SAT solvers, Artificial
Intelligence 157 (2004) 115–137. [25] T. Janhunen, Representing normal programs with clauses, in: R. L. de Mántaras, L. Saitta (Eds.),
2004, pp. 358–362. [26] M. Gebser, T. Janhunen, J. Rintanen, Answer set programming as SAT modulo acyclicity, in:
tificial Intelligence (ECAI 2014), volume 263 of Frontiers in Artificial Intelligence and Applications , IOS Press, 2014, pp. 351–356. [27] T. Janhunen, I. Niemelä, M. Sevalnev, Computing stable models via reductions to diference logic, in: E. Erdem, F. Lin, T. Schaub (Eds.), Proceedings of the 10th International Conference on
in Computer Science, Springer, 2009, pp. 142–154. [28] M. Nguyen, T. Janhunen, I. Niemelä, Translating answer-set programs into bit-vector logic, in:
(WLP 2011) of Applications of Declarative Programming and Knowledge Management, volume 7773 of Lecture Notes in Computer Science, Springer, 2011, pp. 95–113. [29] G. Liu, T. Janhunen, I. Niemelä, Answer set programming via mixed integer programming, in:
on Principles of Knowledge Representation and Reasoning: Proceedings (KR 2012), AAAI Press, 2012. [30] L. Liu, M. Truszczynski, Properties and applications of programs with monotone and convex constraints, Journal of Artificial Intelligence Research 27 (2006) 299–334. [31] P. Ferraris, J. Lee, V. Lifschitz, A new perspective on stable models, in: M. M. Veloso (Ed.),
2007, pp. 372–379. [32] S. Baselice, P. A. Bonatti, M. Gelfond, Towards an integration of answer set and constraint solving, in: M. Gabbrielli, G. Gupta (Eds.), Proceedings of the 21st International Conference on
2005, pp. 52–66. [33] M. Banbara, B. Kaufmann, M. Ostrowski, T. Schaub, Clingcon: The next generation, Theory and
[34] M. Balduccini, Y. Lierler, Constraint answer set solver EZCSP and why integration schemas matter, Theory and Practice of Logic Programming 17 (2017) 462–515. [35] D. Shen, Y. Lierler, Smt-based constraint answer set solver EZSMT+ for non-tight programs, in:
[36] E. Giunchiglia, M. Maratea, On the Relation Between Answer Set and SAT Procedures (or,
[37] E. Giunchiglia, N. Leone, M. Maratea, On the relation among answer set solvers, Ann. Math.
Artif. Intell. 53 (2008) 169–204. [38] A. Armando, C. Castellini, E. Giunchiglia, M. Idini, M. Maratea, TSAT++: an open platform for satisfiability modulo theories, in: W. Ahrendt, P. Baumgartner, H. de Nivelle, S. Ranise, C. Tinelli (Eds.), Selected Papers from the Workshops on Disproving, D@IJCAR 2004, and the Second
125 of Electronic Notes in Theoretical Computer Science, Elsevier, 2004, pp. 25–36. [39] L. M. de Moura, N. S. Bjørner, Z3: an eficient SMT solver, in: C. R. Ramakrishnan, J. Rehof (Eds.),
2008, pp. 337–340. [40] B. Dutertre, Yices 2.2, in: A. Biere, R. Bloem (Eds.), Proc. of the Computer Aided Verification 26th International Conference (CAV 2014), volume 8559 of Lecture Notes in Computer Science, Springer, 2014, pp. 737–744. [41] F. Calimeri, M. Gebser, M. Maratea, F. Ricca, The design of the fifth answer set programming competition, CoRR abs/1405.3710 (2014). URL: http://arxiv.org/abs/1405.3710. arXiv:1405.3710. [42] M. Gebser, B. Kaufmann, T. Schaub, Conflict-driven answer set solving: From theory to practice,
[43] M. Alviano, G. Amendola, C. Dodaro, N. Leone, M. Maratea, F. Ricca, Evaluation of disjunctive programs in WASP, in: M. Balduccini, Y. Lierler, S. Woltran (Eds.), LPNMR, volume 11481 of LNCS, Springer, 2019, pp. 241–255.