Better Paracoherent Answer Sets with Less Resources

TL;DR

This paper introduces an efficient method for computing improved paracoherent answer sets in ASP, enabling meaningful reasoning from incoherent programs with reduced computational resources.

Contribution

It presents a novel evaluation technique for split semi-equilibrium semantics that improves the efficiency of computing paracoherent answer sets.

Findings

Better paracoherent answer sets are computed with less resources.

The method outperforms existing approaches on hard benchmarks.

It extends ASP's applicability to incoherent programs effectively.

Abstract

Answer Set Programming (ASP) is a well-established formalism for logic programming. Problem solving in ASP requires to write an ASP program whose answers sets correspond to solutions. Albeit the non-existence of answer sets for some ASP programs can be considered as a modeling feature, it turns out to be a weakness in many other cases, and especially for query answering. Paracoherent answer set semantics extend the classical semantics of ASP to draw meaningful conclusions also from incoherent programs, with the result of increasing the range of applications of ASP. State of the art implementations of paracoherent ASP adopt the semi-equilibrium semantics, but cannot be lifted straightforwardly to compute efficiently the (better) split semi-equilibrium semantics that discards undesirable semi-equilibrium models. In this paper an efficient evaluation technique for computing a split semi-equilibrium model is presented. An experiment on hard benchmarks shows that better paracoherent answer sets can be computed consuming less computational resources than existing methods. Under consideration for acceptance in TPLP.

Equations

$$a_1\vee \cdots \vee a_l\leftarrow b_1,\dots ,b_m,not{c}_1,\dots ,not{c}_n,$$

$$\leftarrow b_1,...,b_m,not{c}_1,...,not{c}_n,$$

$$\gamma \leftarrow b_1,...,b_m,not{c}_1,...,not{c}_n,not\gamma ,$$

$${\lambda }_{r,1}\vee \dots \vee {\lambda }_{r,l}\vee K{c}_1\vee \dots \vee K{c}_n$$

$$a_i$$

$$\leftarrow {\lambda }_{r,i},c_j,$$

$${\lambda }_{r,i}$$

$$Ka$$

$$K{a}_1\vee ...\vee K{a}_l\vee K{c}_1\vee ...\vee K{c}_n$$

$$split(P)=P^{HT}\cup P_{\gamma }\bigcup _{i=1}^n\{:\sim \gamma a[1:n-i]\mid a\in C_i\}.$$

$$Penalty(M,l)=|\mathcal{G}(M)\cap C_{n-l}|.$$

$$Penalty(M,l)=\sum _{\omega \in \Omega (l),M\models B(\omega )}w=\sum _{:\sim \gamma a\in \Omega (l),M\models \{\gamma a\}}1=\sum _{a\in C_{n-l},\gamma a\in M}1=|\mathcal{G}(M)\cap C_{n-l}|.$$

Full text

1 Introduction

In the past decades, key advances in Artificial Intelligence research were made thanks to studies in the field of Knowledge Representation and Reasoning (KRR) [van Harmelen et al. (2008)]. Among the established paradigms of KRR is Answer Set Programming (ASP) [Baral (2003), Brewka et al. (2011), Gebser et al. (2012)], which is a well-known formalism for logic programming and non-monotonic reasoning. ASP is based on the stable model (or answer set) semantics [Gelfond and Lifschitz (1991)], and features efficient implementations [Lierler et al. (2016), Gebser et al. (2016)], such as clasp [Gebser et al. (2015), Gebser et al. (2019)], wasp [Alviano et al. (2015), Alviano et al. (2019)], and dlv [Leone et al. (2006), Alviano et al. (2017)]. Problem solving in ASP requires to write an ASP program whose answers sets correspond to solutions [Lifschitz (1999)], and then to compute these solutions resorting to an ASP solver. The availability of efficient implementations made possible the development of concrete applications, and as a matter of fact, ASP has been successifully applied to solve complex problems in Artificial Intelligence [Balduccini et al. (2001), Erdem et al. (2016), Gaggl et al. (2015), Dodaro et al. (2015)]; Bioinformatics [Campeotto et al. (2015)]; Databases [Arenas et al. (2003)], and industrial applications [Dodaro et al. (2016)].

The non-existence of answer sets for some ASP programs can be a modeling feature, but, as argued in [Amendola et al. (2016)], it turns out to be a weakness in many other applications, such as: debugging, model building, inconsistency-tolerant query answering, diagnosis, planning and reasoning about actions. To remedy to the non-existence of answer sets, paracoherent semantics extend the classical answer set semantics to draw meaningful conclusions also from incoherent programs. This ASP variant has been termed paracoherent reasoning [Eiter et al. (2010)]. In particular, Eiter, Fink and Moura improved the paracoherent semantics of semi-stable models [Sakama and Inoue (1995)] avoiding some anomalies with respect to basic modal logic properties by resorting to equilibrium logic [Pearce (2006)]. Thus, this paracoherent semantics is called semi-equilibrium model (SEQ) semantics [Eiter et al. (2010)]. More recently, [Amendola et al. (2016)] noticed that, although the SEQ semantics has nice properties, it may select models that do not respect the modular structure of the program. SEQ semantics use 3-valued interpretations where a third truth value besides true and false expresses that an atom is believed true. For instance, the incoherent logic program $P=\{b\leftarrow\mathit{not}\ a;\ c\leftarrow\mathit{not}\ a,\mathit{not}\ c\}$ admits two SEQ models, say $M_{1}$ and $M_{2}$. In $M_{1}$, $b$ is true, $c$ is believed true, and $a$ is false; whereas in $M_{2}$ $a$ is believed true and both $b$ and $c$ are false. Now, $M_{1}$ appears preferable to $M_{2}$, as, according with a layering (stratification) principle, which is widely agreed in logic programming, one should prefer $b$ rather than $a$, as there is no way to derive $a$ (note that $a$ does not appear in the head of any rule of the program). Therefore, [Amendola et al. (2016)] refine SEQ-models using splitting sequences [Lifschitz and Turner (1994)], the major tool for modularity in modeling and evaluating answer set programs. In particular, the refined semantics, called Split SEQ model semantics, is able to discard model $M_{2}$.

The first efficient implementations of paracoherent semantics were proposed recently [Amendola et al. (2017), Amendola et al. (2018)], but they only support semi-stable and semi-equilibrium semantics. Although the Split SEQ semantics discards some undesirable SEQ models, the existing methods for computing SEQ models cannot be lifted straightforwardly to compute the refined semantics efficiently. Consequently, no implementation of Split SEQ semantics has been available up to now.

In this paper, we fill this lack presenting the first efficient strategy for computing a split SEQ model. In particular, we introduce an elegant program transformation, obtained by using weak constraints with levels [Buccafurri et al. (2000)], that allows for computing a split semi-equilibrium model using a single call to a plain ASP solver, and prove a non-obvious correctness result. Notably, we exploited the modularity property of split semi equilibrium models to simplify the transformation and avoid the introduction of some rules and symbols that are needed in state of the art epistemic-transformation-based methods for computing SEQ models.

We have implemented the new approach and run an experiment to validate it empirically. Actually, no direct comparison with an alternative methods can be done, since ours is the first implementation of split SEQ models. Nonetheless, since split SEQ models are also SEQ models, we could compare it against existing implementations for semi-equilibrium models. As done previoulsy in the literature [Amendola et al. (2017), Amendola et al. (2018)], we considered hard benchmarks from ASP competitions  [Calimeri et al. (2016)] modeling an application of paracoherent semantics to debugging [Cuteri et al. (2019)]. The experiment demonstrates that the new method outperforms state of the art methods for computing SEQ models consuming less computational resources, i.e., it uses less memory and terminates in less time.

The paper is structured as follows: preliminary notions on ASP and paracoherent answer sets are reported in Section 2; the description of strategies for computing split SEQ models is provided in Section 3; the empirical validation of our approach is presented in Section 4; related work is compared and discussed in Section 5; finally, we draw the conclusion in Section 6.

2 Preliminaries

We start with recalling answer set semantics, and then present the paracoherent semantics of semi-equilibrium models, and its refined version based on splitting sequences.

2.1 Answer Set Programming

We concentrate on logic programs over a propositional signature $\Sigma$. A disjunctive rule $r$ is of the form

[TABLE]

where all $a_{i}$, $b_{j}$, and $c_{k}$ are atoms (from $\Sigma)$; $l>0$, $m,n\geq 0$; \mathit{not}\represents negation-as-failure. The set $H(r)=\{a_{1},...,a_{l}\}$ is the head of $r$, while $B^{+}(r)=\{b_{1},...,b_{m}\}$ and $B^{-}(r)=\{c_{1},\ldots,c_{n}\}$ are the positive body and the negative body of $r$, respectively; the body of $r$ is $B(r)=B^{+}(r)\cup B^{-}(r)$. We denote by $At(r)=H(r)\cup B(r)$ the set of all atoms occurring in $r$. A rule $r$ is a fact, if $B(r)=\emptyset$ (we then omit $\leftarrow$); normal, if $|H(r)|\leq 1$; and positive, if $B^{-}(r)=\emptyset$. A (disjunctive logic) program $P$ is a finite set of disjunctive rules. $P$ is called normal [resp. positive] if each $r\in P$ is normal [resp. positive]. The set of all atoms occurring in the program $P$ is denoted by $At(P)=\bigcup_{r\in P}At(r)$.

The dependency graph of a program $P$ is the directed graph $DG(P)=\langle V_{P},E_{P}\rangle$ whose nodes $V_{P}$ are the atoms in $P$ and $E_{P}$ contains an edge $(a,b)$ if $a$ occurs in $H(r)$ and either $b$ occurs in $B(r)$ or in $H(r)\setminus\{a\}$. The strongly connected components (SCCs) of $P$, denoted $SCC(P)$, are the SCCs of $DG(P)$, which are the maximal sets of nodes $C$ such that every pair of nodes is connected by some path in $DG(P)$ with nodes only from $C$.

Any set $I\subseteq\Sigma$ is an interpretation; it is a model of a program $P$ (denoted $I\models P$) if and only if for each rule $r\in P$, $I\cap H(r)\neq\emptyset$ if $B^{+}(r)\subseteq I$ and $B^{-}(r)\cap I=\emptyset$ (denoted $I\models r$). A model $M$ of $P$ is minimal, if and only if no model $M^{\prime}\subset M$ of $P$ exists. We denote by $\mathit{MM}(P)$ the set of all minimal models of $P$ and by $AS(P)$ the set of all answer sets (or stable models) of $P$, i.e., the set of all interpretations $I$ such that $I\in\mathit{MM}(P^{I})$, where $P^{I}$ is the well-known Gelfond-Lifschitz reduct [Gelfond and Lifschitz (1991)] of $P$ w.r.t. $I$, i.e., the set of rules $a_{1}\vee...\vee a_{l}\leftarrow b_{1},...,b_{m}$, obtained from rules $r\in P$ of form (1), such that $B^{-}(r)\cap I=\emptyset$. We say that a program $P$ is coherent, if it admits some answer set (i.e., $AS(P)\neq\emptyset$), otherwise, it is incoherent.

In the following, we will also use constraints, which are of the form

[TABLE]

with $m,n\geq 0$, to be considered as a shorthand for a rule

[TABLE]

using a fresh atom $\gamma$ that is not occurring elsewhere in the program. Note that ASP solvers do normally not create any auxiliary symbols for constraints.

Moreover, we recall a useful extension of the answer set semantics by the notion of weak constraint [Buccafurri et al. (2000)]. A weak constraint $\omega$ is of the form:

$:\sim b_{1},\ldots,\ b_{m},\ \mathit{not}\ c_{1},\ldots,\ \mathit{not}\ c_{n}.\ [w@l]$,

where $w$ and $l$ are nonnegative integers, representing a weight and a level, respectively. Let $\Pi$ $=$ $P\cup\Omega$ , where $P$ is a set of rules and $\Omega$ is a set of weak constraints. We call $M$ an answer set of $\Pi$ if it is an answer set of $P$. We denote by $\Omega(l)$ the set of all weak constraints at level $l$. For every answer set $M$ of $\Pi$ and any $l$, the penalty of $M$ at level $l$, denoted by $\mathit{Penalty}_{\Pi}(M,l)$, is defined as $\sum_{\omega\in\Omega(l),\ M\models B(\omega)}w$. In case $\Pi$ is clear from the context, we omit the subscript. For any two answer sets $M$ and $M^{\prime}$ of $\Pi$, we say $M$ is dominated by $M^{\prime}$ if there is $l$ s.t. $(i)$ $\mathit{Penalty}_{\Pi}(M^{\prime},l)<\mathit{Penalty}_{\Pi}(M,l)$ and $(ii)$ for all integers $k>l$, $\mathit{Penalty}_{\Pi}(M^{\prime},k)$ $=$ $\mathit{Penalty}_{\Pi}(M,k)$. An answer set of $\Pi$ is optimal if it is not dominated by another one of $\Pi$. We denote by $AS^{O}(\Pi)$ the set of all optimal answer sets of $\Pi$.

2.2 Semi-Equilibrium Models

Here, we introduce the paracoherent semantics of the semi-equilibrium (SEQ) models introduced in [Eiter et al. (2010)]. Consider an extended signature $\Sigma^{\kappa}=\Sigma\cup\{Ka\mid a\in\Sigma\}$. Intuitively, $Ka$ can be read as $a$ is believed to hold. The SEQ models of a program $P$ are obtained from its epistemic ${HT}$-transformation ${P}^{{HT}}$, defined as follows.

Definition 1

Let $P$ be a program over $\Sigma$. Then its epistemic ${HT}$-transformation ${P}^{{HT}}$ is obtained from $P$ by replacing each rule $r$ of the form (1) in $P$, such that $B^{-}(r)\neq\emptyset$, with:

[TABLE]

for $1\leq i,k\leq l$ and $1\leq j\leq n$, where the $\lambda_{r,i}$, $\lambda_{r,k}$ are fresh atoms; and by adding the following set of rules:

[TABLE]

for $a\in\Sigma$, respectively for every rule $r\in P$ of the form (1).

Note that for any program $P$, its epistemic ${HT}$-transformation ${P}^{{HT}}$ is positive. For every interpretation $I^{\kappa}$ over $\Sigma^{\prime}\supseteq\Sigma^{\kappa}$, let $\mathcal{G}(I^{\kappa})=\{Ka\in I^{\kappa}\ \mid a\not\in I^{\kappa}\}$ denote the atoms believed true but not assigned true, also referred to as the gap of $I^{\kappa}$. Given a set ${\mathcal{F}}$ of interpretations over $\Sigma^{\prime}$, an interpretation $I^{\kappa}\in{\mathcal{F}}$ is maximal canonical in ${\mathcal{F}}$, if no ${J}^{\kappa}\in{\mathcal{F}}$ exists such that $\mathcal{G}(I^{\kappa})\supset\mathcal{G}({J}^{\kappa})$. By $\mathit{mc}({\mathcal{F}})$ we denote the set of maximal canonical interpretations in ${\mathcal{F}}$. SEQ models are then defined as maximal canonical interpretations among the answer sets of ${P}^{{HT}}$.

Definition 2

Let $P$ be a program over $\Sigma$, and let $I^{\kappa}$ be an interpretation over $\Sigma^{\kappa}$. Then, $I^{\kappa}\in\mathit{SEQ}(P)$ if, and only if, $I^{\kappa}\in\{M\cap\Sigma^{\kappa}\mid M\in\mathit{mc}(AS({P}^{{HT}}))\}$, where $\mathit{SEQ}(P)$ is the set of semi-equilibrium models of $P$.

2.3 Split SEQ Models

A set $S\subseteq At(P)$ is a splitting set of $P$, if for every rule $r$ in $P$ such that $\mathit{head}(r)\cap S\neq\emptyset$ we have that $At(r)\subseteq S$. We denote by $b_{S}(P)=\{r\in P\mid At(r)\subseteq S\}$ the bottom part of $P$, and by $t_{S}(P)=P\setminus b_{S}(P)$ the top part of $P$ relative to $S$. A splitting sequence $S=(S_{1},\ldots,$ $S_{n})$ of $P$ is a sequence of splitting sets $S_{i}$ of $P$ such that $S_{i}\subseteq S_{j}$ for each $i<j$. Let $SCC(P)$ be the set of all strongly connected components of $P$, and let $(C_{1},\ldots,C_{n})$ be a topological ordering of $SCC(P)$. It is known that $\Gamma=(\Gamma_{1},\ldots,\Gamma_{n})$, where $\Gamma_{j}=C_{1}\cup\ldots\cup C_{j}$ for $j=1,\ldots,n$, is a splitting sequence of $P$. So that, we obtain a stratification for $P$ in subprograms $(P_{1},\ldots,P_{n})$ such that $P_{1}=b_{\Gamma_{1}}(P)$, and $P_{j}=b_{\Gamma_{j}}(P)\setminus P_{j-1}$, for $j=2,\ldots,n$. Given an interpretation $M_{i}$ over $C_{i}$, we denote by $\mathit{info}(M_{i})$ the set of rules $\{a\mid a\in M_{i}\}\cup\{\leftarrow not\ a\mid Ka\in M_{i}\}\cup\{\leftarrow a\mid a\in C_{i}\setminus M_{i}\}$.

Definition 3

Given a topological ordering $(C_{1},\ldots,C_{n})$ of $SCC(P)$, an interpretation $M$ over $At(P)$ is a semi-equilibrium model of $P$ relative to $\Gamma$ if there is a sequence of interpretations $M_{1},\ldots,M_{n}$ over $\Gamma_{1},\ldots\Gamma_{n}$, respectively, such that $(1)$ $M=M_{n}$; $(2)$ $M_{1}\in\mathit{SEQ}(P_{1})$; $(3)$ $M_{j}\in\mathit{SEQ}(P_{j}\cup\mathit{info}(M_{j-1}))$, for $j=2,\ldots,n$; and $(4)$ $M$ is maximal canonical among the interpretations over $At(P)$ satisfying conditions $(1)$, $(2)$ and $(3)$. The set of all semi-equilibrium models of $P$ relative to $\Gamma$ is denoted by $SEQ^{\Gamma}(P)$.

Since $SEQ^{\Gamma}(P)$ is independent by the given topological ordering of $SCC(P)$ (see, Theorem 5 in [Amendola et al. (2016)]), the $SCC$-models of $P$ have been defined as the set $M^{SCC}(P)$ $=$ $SEQ^{\Gamma}(P)$ for an arbitrary topological ordering of $SCC(P)$. We will refer to them as split semi-equilibrium models. Finally, note that $M^{SCC}(P)\subseteq SEQ(P)$.

Example 1

Consider the program

P=\left\{\begin{array}[]{rcl}b&\leftarrow&\mathit{not}\ a;\\ d&\leftarrow&b,\ \mathit{not}\ c;\\ c&\leftarrow&d\end{array}\right\}.**

Then, $(\{a\},\{b\},\{c,d\})$ is a topological ordering of $SCC(P)$, so that $\Gamma=(\{a\},$ $\{a,b\},$ $\{a,b,c,$ $d\})$ is a splitting sequence for $P$. Hence, $\mathit{SEQ}^{\Gamma}(P)=\{\{b,Kb,Kc\}\}$. Indeed $P_{1}=b_{\Gamma_{1}}(P)=\emptyset$ and thus $\mathit{SEQ}(P_{1})=\{\emptyset\}$. Then, $P_{2}\cup\mathit{info}(\emptyset)=\{b\leftarrow\mathit{not}\ a,\;\leftarrow a\}$ and thus $\mathit{SEQ}(P_{2}\cup\mathit{info}(\emptyset))=\{\{b\}\}$. Finally, $P_{3}\cup\mathit{info}(\{b\})=\{d\leftarrow b,\mathit{not}\ c;\ c\leftarrow d;\ b;\ \leftarrow a\}$ and thus $\mathit{SEQ}(P_{3}\cup\mathit{info}(\{b\}))=\{\{b,Kb,Kc\}\}$.

In the following, we will refer to both SEQ models and split SEQ models as paracoherent answer sets.

2.4 Complexity Considerations

The complexity of various reasoning tasks with paracoherent answer sets has been analyzed in [Amendola et al. (2016)]. In the general case, checking whether an atom $a$ is true in some paracoherent answer set (brave reasoning) is ${\Sigma}_{3}^{P}$-complete; whereas checking whether an atom $a$ is true in all paracoherent answer sets (cautious reasoning) is ${\Pi}_{3}^{P}$-complete. However, computing a paracoherent answer set is feasible in F$\Delta^{P}_{3}$, because it is sufficient to find a paracoherent answer set that is cardinality minimal with respect to the gap.

3 On the Computation of Split SEQ Models

We start to note that an efficient computation of a split semi-equilibrium model requires a deep theoretical understanding of the paracoherent semantics. Indeed, a naive implementation of the split semi-equilibrium semantics considers each possible path that can be generated through the splitting sequence. Since each subprogram could have more than one answer set, one should explore an exponential number of paths. Note that, each path generated through the splitting sequence leads to obtain a paracoherent answer set of the last program (i.e., $P_{n}\cup\mathit{info}(M_{n-1})$), which is not necessarily a paracoherent answer set of the entire program $P$ because it must also be gap-minimal.

Example 2

Consider the program

P=\left\{\begin{array}[]{rcl}a&\leftarrow&not\ b;\\ b&\leftarrow&not\ a;\\ c&\leftarrow&a,\ not\ c\end{array}\right\}.**

In the first layer of $P$, we have the subprogram $P_{1}$ $=$ $\{a\leftarrow not\ b;\ b\leftarrow not\ a\}$ whose (paracoherent) answer sets are $\{a,Ka\}$ and $\{b,Kb\}$. So that, considering $\mathit{info}(\{a,Ka\})\cup\{c\leftarrow a,\ not\ c\}$, we obtain the paracoherent answer set $\{a,Ka,Kc\}$, while considering $\mathit{info}(\{b,Kb\})\cup\{c\leftarrow a,\ not\ c\}$, we obtain the (paracoherent) answer set $\{b,Kb\}$. Hence, $\{a,Ka,Kc\}$ cannot be a paracoherent answer set of $P$, because it has a larger gap w.r.t. $\{b,Kb\}$. Indeed, $\mathcal{G}(\{a,Ka,Kc\})=\{Kc\}\supset\mathcal{G}(\{b,Kb\})=\emptyset$.

From a computational view point, a naive approach is very expensive, as one has to enumerate all possible paracoherent models obtainable from each path to make feasible a final phase of gap minimization.

Hence, we developed a clever strategy to compute a split SEQ model. Given a program $P$ and a topological ordering $(C_{1},\ldots,C_{n})$ of $SCC(P)$, we construct a new program $\mathit{split}(P)$ which is the union of ${P}^{{HT}}$ with the program $P_{\gamma}=\{\gamma a\leftarrow Ka,not\ a\ |\ a\in At(P)\}$, and the following set $\Omega$ of weak constraints. For each $i=1,\ldots,n$, and for each atom $a\in C_{i}$, the weak constraint $:\sim\gamma a\ [1:n-i]$ belongs to $\Omega$. Then, we define

[TABLE]

We will show that an optimal answer set of $\mathit{split}(P)$ is a split SEQ model of $P$. Hence, in particular, it is also a SEQ model of $P$. First, we highlight a fundamental relation between the penalty of a model at a fixed level and the set of gap atoms of that model belonging to a strongly connected component.

Proposition 1

Let $M$ be an optimal answer set of $\mathit{split}(P)$. Then, for $l=0,...,n-1$,

[TABLE]

Proof 3.1** (Proof Sketch).**

Since $\Omega(l)$ $=$ $\{:\sim\gamma a\ [1:l]\mid a\in C_{n-l}\}$, we obtain that

[TABLE]

Now we can prove our main result.

Theorem 3.2**.**

Let $P$ be a program and $M$ be an optimal answer set of $\mathit{split}(P)$. Then, $M\setminus\{\gamma a\ |\ a\in At(P)\}$ is a split SEQ model of $P$.

Proof 3.3**.**

We prove the claim by induction on the cardinality of $|SCC(P)|$.

In case of $|SCC(P)|=1$, we have a unique strongly connected component, say $C$, of $P$. Hence, we have to consider the unique topological ordering $(C)$. It leads to have the following set of weak constraints $\Omega=\Omega(1)=\{:\sim\gamma a\ [1:0]\mid a\in C\}$. Hence, $M$ is an answer set of $P^{HT}\cup P_{\gamma}$ such that a minimum number of weak constraints in $\Omega$ is violated. This means that $M$ is cardinality minimal with respect to the gap atoms. Therefore, it is also subset minimal with respect to the gap atoms, and so, $M^{\prime}=M\setminus\{\gamma a\ |\ a\in At(P)\}$ is a semi-equilibrium model of $P$. As for $n=1$, the split semi-equilibrium models of $P$ coincide with the semi-equilibrium models of $P$, then $M^{\prime}$ is a split semi-equilibrium model of $P$.

Now, assume the claim holds in case of programs with $n-1$ strongly connnected components, and we want to prove that it also holds for programs with $n$ strongly connected components. Let $SCC(P)=\{C_{1},\ldots,C_{n}\}$, and let $(P_{1},\ldots,P_{n})$ be the corresponding stratification for $P$. Let $M_{n-1}=M\cap(C_{n-1}\cup\{Ka\ |\ a\in C_{n-1}\})$. By construction, $M_{n-1}\in AS^{O}((P^{HT}\setminus P_{n}^{HT})\cup P_{\gamma}\cup(\Omega\setminus\Omega(n)))$. Hence, by inductive hypothesis, $M_{n-1}\setminus\{\gamma a\ |\ a\in At(P)\}$ is a split semi-equilibrium model of $P\setminus P_{n}$. Now, we have to prove that $M^{\prime}=M\setminus\{\gamma a\ |\ a\in At(P)\}\in SEQ(P_{n}\cup\mathit{info}(M_{n-1}))$. Consider the program $\Pi=P_{n}^{HT}\cup\mathit{info}(M_{n-1})\cup\Omega(n)$. First, $(i)$ $M\in AS(P_{n}^{HT}\cup\mathit{info}(M_{n-1}))$, as $M\in AS(P^{HT})$. Second, $(ii)$ $M$ violates a minimum number of weak constraints in $\Omega(n)$. Indeed, by contradiction, there exists $I$ violating a strictly less number of weak constraints in $\Omega(n)$ than $M$. So that, such a $I$ dominates $M$ with respect to $split(P)$, against the assumption that $M$ is an optimal answer set of $split(P)$. Then, by $(i)$ and $(ii)$, it holds that $M\in AS^{O}(\Pi)$. Therefore, $M^{\prime}\in SEQ(P_{n}\cup\mathit{info}(M_{n-1}))$. Finally, we claim that $M^{\prime}$ is maximal canonical among the interpretations over $At(P)$ satisfying conditions $(1)$, $(2)$ and $(3)$ in Definition 3. Assume, by contradiction, that there is an interpretation $I$ satisfying conditions $(1)$, $(2)$ and $(3)$ in Definition 3 such that $\mathcal{G}(I)\subset\mathcal{G}(M)$. Hence, by Proposition 1, there is some nonnegative integer $l$ such that $(i)$ $\mathit{Penalty}(I,l)<\mathit{Penalty}(M,l)$ and $(ii)$ for all integers $k>l$, $\mathit{Penalty}(I,k)$ $=$ $\mathit{Penalty}(M,k)$. Then, $M$ is dominated by $I$. Thus, $M$ is not an optimal answer set of $\mathit{split}(P)$, against the hypothesis.

Note that the split semi-equilibrium model (hence the semi-equilibrium model) that such an algorithm will find, generally, is not cardinality minimal among the split semi-equilibrium models of the given program. This is coherent with complexity results, indeed computing optimal answer sets of ASP programs with weak constraints is known to be a $F\Delta^{P}_{3}$ task for disjunctive programs [Buccafurri et al. (2000)], and our technique can be implemented by an algorithm that runs in polynomial time (indeed, it consists of two polynomial tasks: the construction of the epistemic transformation and the computation of the SCCs).

Example 3.4**.**

Consider, for instance, the following program

P=\left\{\begin{array}[]{rcl}a&\leftarrow&not\ b;\\ b&\leftarrow&not\ a;\\ c&\leftarrow&b,\ not\ c;\\ d&\leftarrow&a,\ not\ c,\ not\ d;\\ e&\leftarrow&d\\ \end{array}\right\}.

Hence, we have to consider the stratification of $P$ given by $P_{1}=\{a\leftarrow not\ b;$ $b\leftarrow not\ a\}$; $P_{2}=\{c\leftarrow b,\ not\ c\}$; $P_{3}=\{d\leftarrow a,\ not\ c,\ not\ d\}$; and $P_{4}=\{e\leftarrow d\}$. At the first step, we obtain $\{a,Ka\}$ and $\{b,Kb\}$ as SEQ models of $P_{1}$. At the second step, $\{a,Ka\}$ is the SEQ model of $P_{2}\cup\mathit{info}(\{a,Ka\})$, and $\{b,Kb,Kc\}$ is the SEQ model of $P_{2}\cup\mathit{info}(\{b,Kb\})$. At the third step, $\{a,Ka,Kd\}$ is the SEQ model of $P_{3}\cup\mathit{info}(\{a,Ka\})$, and $\{b,Kb,Kc\}$ is the SEQ model of $P_{3}\cup\mathit{info}(\{b,Kb,Kc\})$. At the fourth and final step, $\{a,Ka,Kd,Ke\}$ is the SEQ model of $P_{4}\cup\mathit{info}(\{a,Ka,Kd\})$, and $\{b,Kb,Kc\}$ is the SEQ model of $P_{4}\cup\mathit{info}(\{b,Kb,Kc\})$. Therefore, $\{a,Ka,Kd,Ke\}$ and $\{b,Kb,Kc\}$ are the split SEQ models of $P$. However, $\{a,Ka,Kd,Ke\}$ is preferred to $\{b,Kb,Kc\}$. Indeed, $\{b,Kb,Kc\}$ violates the weak constraint $:\sim\gamma c$, that is at a lower level than $:\sim\gamma d$ and $:\sim\gamma e$, that are violated by $\{a,Ka,Kd,Ke\}$.

Moreover, the split SEQ semantics allows to make a fundamental simplification of symbols in the ${HT}$-epistemic transformation of the program. Indeed, given a program $P$ and a stratification for $P$ in subprograms $(P_{1},\ldots,P_{n})$, whenever $P_{1}$, …, $P_{k}$, with $k<n$, are coherent programs, we have no need to compute the ${HT}$-epistemic transformation of $P_{1}$, …, $P_{k}$, but we can directly compute the answer sets of $P_{1}\cup\cdots\cup P_{k}$. So that, if $M\in AS(P_{1}\cup\cdots\cup P_{k})$, then $M\cup\{Ka\ |\ a\in M\}$ is a paracoherent answer set of $P_{1}\cup\cdots\cup P_{k}$.

Theorem 3.5**.**

Let $P$ be a program, $(P_{1},\ldots,P_{n})$ be a stratification for $P$, and $k$ be the maximal number so that $P_{j}$ is coherent, for each $j=1,...,k$. Then,

$M^{SCC}(P)=\{I^{K}\cup J\ |\ I\in AS(P_{coh})\wedge J\in M^{SCC}(P_{inc}^{I})\}$,

where $I^{K}=I\cup\{Ka\ |\ a\in I\}$; $P_{coh}=P_{1}\cup\cdots\cup P_{k}$; $P_{inc}=P_{k+1}\cup\cdots\cup P_{n}$; and $P_{inc}^{I}$ comes from $P_{inc}$ by removing each rule $r$ s.t. $B^{-}(r)\cap I\neq\emptyset$, and each atom in $At(P_{inc})\cap I$.

Finally, note that to check if a program is coherent, is a well-known $\Sigma^{P}_{2}$-complete problem. Hence, in the implementation we need to consider a sufficient condition to detect coherent programs in polynomial time. It is known that, if a program has no cycle in the dependency graph having an odd number of negated arcs, then it is coherent.

Proposition 3.6**.**

Given a program $P$, detecting a cycle in the dependency graph of $P$ having an odd number of negated arcs, can be done in linear time with respect to $|E_{P}|$.

Proof 3.7** (Proof Sketch).**

Let $DG(P)$ be the dependency graph of $P$. We consider a directed graph $G^{\prime}$ such that for each positive arc in $DG(P)$, namely $(a,b)$, we introduce a fresh node, namely $ab$, and replace $(a,b)$, by two edges $\{a,ab\}$ and $\{ab,b\}$. Hence, if $DG(P)$ contains a cycle having an odd number of negated arcs then $G^{\prime}$ contains a cycle of odd length. The claim holds by the fact the a directed graph does not contain a directed cycle of odd length if, and only if, it is bipartite when treated as an undirected graph, i.e., it can be colored with two colors. This check can be done in linear time with respect to the number of arcs in the input graph [Kleinberg and Tardos (2006)].

We conclude this section observing that Theorem 3.2 and Theorem 3.5 hold (without modifications) also if one considers the extended externally supported program $P^{es}$, introduced in [Amendola et al. (2018)] to characterize semi-equilibrium models, in place of the ${HT}$-epistemic transformation.

4 Experiments

In this section we present the results of an experimental analysis conducted to analyze the performance of the new strategy for computing a split semi-equilibrium model presented in the previous section.

4.1 Implementation

To compute a split semi-equilibrium model we have implemented in a rewriter tool a program transformation that takes as input an ASP program $P$ and produces as output an optimized version of $\mathit{split}(P)$. In particular, the rewriter implements the efficient epistemic transformation $P^{es}$ of  [Amendola et al. (2018)], which is known to be much more efficient than the classic $HT$-epistemic transformation, and implements the Tarjan algorithm (see e.g., [Kleinberg and Tardos (2006)]) to compute a topological order of the $SCC(P)$ and build the weak constraints $\Omega$. During the rewriting process, the components are also subject to a (modified) two-colorability check (see Proposition 3.6) applied following the topological order to optimize the output as indicated in Theorem 3.5. Thus, a split semi-equilibrium model is computed by evaluating the optimized $\mathit{split}(P)$ with the ASP solver wasp [Alviano et al. (2015), Alviano and Dodaro (2016)].

4.2 Experimental Setting

A practical approach for the computation of a split semi-equilibrium model has been presented for the first time in this paper. Therefore, it is not possible to compare the performance of our implementation with alternative approaches for computing split semi-equilibrium models. Since all split semi-equilibrium models are semi-equilibrium models, we focus on the task of computing a semi-equilibrium model, and compare our implementation with the state of the art ones presented in [Amendola et al. (2018)], namely: split, min, and weak. Note that, the labels correspond to the algorithm names used in [Amendola et al. (2018)], where split is in no way related to the split semi equilibrium semantics; rather, the name split was chosen to remind the behavior of the algorithm that “splits” the set of gap atoms of a candidate solution to perform gap minimization (for details see [Amendola et al. (2018)]). In the following, our implementation is labeled sseq, since its distinguishing feature is to compute a split semi equilibrium model.

In order to perform a fair comparison, in this experiment we used the same version of the wasp solver, and the same experimental settings described in [Amendola et al. (2018)]. In particular, we considered all the incoherent instances from the latest ASP Competition [Gebser et al. (2017)] that feature neither aggregates, nor choice rules, nor weak constraints, since such features are not supported by the paracoherent semantics [Amendola et al. (2016)]. This benchmark setting is of particular interest for paracoherent reasoning since it consists of debugging hard ASP programs, one of the main motivations of paracoherent ASP. In particular, the problem to be solved is the computation of an explanation for the non-existence of answer sets. Execution times and memory usage were limited to 1200 seconds and 8 GB, respectively.

4.3 Results

The results of the experiment show that the new technique is better than state-of-the-art-approaches. In the vast majority of considered instances the improvements are significant, as seen from the cactus plots in Figure 1. In more detail, sseq solves overall 104 instances, whereas the performance achieved by min, split, and weak is considerably worse, solving 13, 16, and 65 instances in the allotted time, respectively.

Figures 2(a) and 2(b) show instance-by-instance comparisons for the two best-performing algorithms, i.e. sseq and weak. We recall that each plotted point represent an instance, and a point $(x,y)$ is plotted if the two systems take $x$ and $y$ execution time (resp. memory usage) for evaluating the instance. Therefore, points below the diagonals represent instances where the system reported on the $x$-axis was slower (resp. uses more memory) than the system reported on the $y$-axis. The graphs confirm the better performance of sseq. Indeed, in Figure 2(a), only few instances are on the left of the diagonals, meaning that are only few instances where sseq is slower than weak. Concerning the memory usage, Figure 2(b) clearly shows sseq uses consistently less memory than weak. We also mention that sseq and weak exceed the allotted memory limited in 1 and 83 instances, respectively. It is worth reporting that disabling the optimization of Theorem 3.5, which is specific of split SEQ semantics, the resulting method could only solve 6 instances, and expectedly the performance w.r.t. memory consumption was also poorer, i.e., it exceeded 51 times the memory limits.

5 Related Work

Semantics for non-monotonic logic programs [Przymusinski (1991), van Gelder et al. (1991), You and Yuan (1994), Sakama and Inoue (1995), Eiter et al. (1997), Seipel (1997), Balduccini and Gelfond (2003), Pereira and Pinto (2007), Alcântara et al. (2005), Galindo et al. (2008), Amendola et al. (2016), Costantini and Formisano (2016)] that relax the definition of answer set to overcome the absence of answer sets can be considered in broader terms paracoherent semantics. Nonetheless, the first approach to the problem of handling inconsistency in ASP programs is the semi-stable semantics by [Sakama and Inoue (1995)]. Later [Eiter et al. (2010)] identified some anomalies of semi-stable semantics with respect to some epistemic properties, and proposed the semi-equilibrium semantics. Notably, [Eiter et al. (2010)] also introduced the term paracoherent for the semantics that provide a remedy to the absence of answer sets due to cyclic negation. In [Amendola et al. (2016)] it was demonstrated that semi-equilibrium semantics features a number of highly desirable theoretical properties for a knowledge representation language, that are not all fulfilled by previous proposals: (i) every consistent answer set of a program corresponds to a paracoherent answer set (answer set coverage); (ii) if a program has some (consistent) answer set, then its paracoherent answer sets correspond to answer sets (congruence); (iii) if a program has a classical model, then it has a paracoherent answer set (classical coherence); (iv) a minimal set of atoms should be undefined (minimal undefinedness); (v) every true atom must be derived from the program (justifiability). The first two properties ensure that the notions of answer sets and paracoherent answer sets should coincide for coherent programs; the third states that paracoherent answer set should exist whenever the programs admits a (classical) model; the last two state that the number of undefined atoms should be minimized, and every true atom should be derived from the program, respectively. At the same time, it was observed that semi-equilibrium models do not enjoy the same nice modular composition properties of stable models (e.g., the splitting set [Lifschitz and Turner (1994)] modularity tool cannot be used straightforwardly). Notably, modular composition is used in ASP for simplifying the modeling of problems (actually, the guess and check programming methodology [Eiter et al. (2009)] is based on this property) and is a principle underlying the architectures of ASP systems [Lierler et al. (2016)]. The split semi-equilibrium semantics [Amendola et al. (2016)] solves this problem by using splitting sequences to decompose the program into hierarchically organized subprograms. Split semi-equilibrium models are semi equilibrium models that enjoy a modularity property.

Concerning the implementation of semi-stable and semi-equilibrium semantics, we observe that they have been implemented efficiently only recently. In particular, in [Amendola et al. (2017)] a number of algorithms has been proposed, that compute paracoherent answer sets in two steps: $(i)$ an epistemic transformation of programs is applied, and $(ii)$ a strategy for computing answer sets of minimum gap is implemented by calling (possibly multiple times) an ASP solver. The same strategy has been improved in [Amendola et al. (2018)] by replacing the classic epistemic transformations by more parsimonious ones (that we also adopt). The new transformations are based on the characterization of paracoherent answer sets in terms of externally supported models. Neither [Amendola et al. (2017)] nor [Amendola et al. (2018)] support SSEQ semantics that is the focus of this paper.

For the sake of completeness, we mention that the algorithms used for computing paracoherent answer sets are strictly related to the computation of minimal models of propositional theories [Niemelä (1996), Bry and Yahya (2000), Koshimura et al. (2009), Janota and Marques-Silva (2016), Angiulli et al. (2014)]; the reader si referred to [Amendola et al. (2017)] for a detailed discussion.

6 Conclusion and Future Work

Paracoherent answer set semantics can draw meaningful conclusions also from incoherent programs, and in this way increase the applicability of ASP for solving AI problems [Eiter et al. (2010)]. Practical applications are possible once efficient implementations are available, and the complex task of computing efficiently a paracoherent answer set has been approached only recently [Amendola et al. (2017), Amendola et al. (2018)]. State of the art solutions supported the semi-equilibrium semantics but cannot compute the (better) split semi-equilibrium semantics; notably, existing evaluation techniques cannot be adapted straightforwardly to accomplish this task. We remark that, as mentioned previously, split semi-equilibrium models have to be considered better in the sense that they are models that respect the modular structure of the program (as observed in [Amendola et al. (2016)]), and, thus, they better fit the intentions of a programmer which usually exploits modularity to produce programs (e.g., by applying the guess and check methodology).

In this paper we presented a novel optimized program transformation that allows for computing a split semi-equilibrium model using a plain ASP solver. The transformation is elegant and independent from the epistemic transformation used to define semi-equilibrium models. Moreover, the modularity property of split semi equilibrium models allowed us to devise an optimization that further simplifies the transformed program and improves performance. We implemented the optimized transformation and run an experiment comparing it against existing implementations for semi-equilibrium models. Our implementation outperformed the state of the art methods in terms of both memory consumption and solving times, and it was able to solve 160% more instances than the best alternative solution using the same ASP solver. In conclusion, the paper shows how better semi equilibrium models can be computed also more efficiently.

The availability of efficient methods for computing one paracoherent answer set makes reasonable to start approaching more complex reasoning problems connected with the enumeration of paracoherent answer sets. Thus, as far as future work is concerned, we plan to investigate the extension of our techniques to the implementation of cautious and brave reasoning, e.g., on the lines of [Alviano (2018)]. Notably, this will not be a straightforward porting.

Finally, we mention that an interesting feature work is to investigate how to extend paracoherent rewriting techniques to non-ground ASP programs. Actually, our implementation supports non-ground ASP programs by simply disabling grounding simplifications and then using the resulting instantiation as input for the rewriting techniques applied later on. However, this may cause a deterioration of the performance since grounding simplifications have been shown to be useful for improving the performance of ASP solvers. Therefore, we plan to investigate if more sophisticated rewriting techniques can be directly applied to non-ground ASP programs.