Abstract Solvers for Computing Cautious Consequences of ASP programs

TL;DR

This paper introduces novel abstract solving techniques for cautious reasoning in Answer Set Programming, inspired by backbone computation in SAT, and demonstrates their effectiveness in ASP solvers.

Contribution

The paper develops new abstract algorithms for cautious reasoning in ASP, linking them to backbone computation in SAT, and implements these in the WASP solver.

Findings

Performance comparable to state-of-the-art solutions

New algorithms improve cautious reasoning in ASP

Formal connection between ASP cautious reasoning and SAT backbone computation

Abstract

Abstract solvers are a method to formally analyze algorithms that have been profitably used for describing, comparing and composing solving techniques in various fields such as Propositional Satisfiability (SAT), Quantified SAT, Satisfiability Modulo Theories, Answer Set Programming (ASP), and Constraint ASP. In this paper, we design, implement and test novel abstract solutions for cautious reasoning tasks in ASP. We show how to improve the current abstract solvers for cautious reasoning in ASP with new techniques borrowed from backbone computation in SAT, in order to design new solving algorithms. By doing so, we also formally show that the algorithms for solving cautious reasoning tasks in ASP are strongly related to those for computing backbones of Boolean formulas. We implement some of the new solutions in the ASP solver WASP and show that their performance are comparable to state-of-the-art solutions on the benchmark problems from the past ASP Competitions. Under consideration for acceptance in TPLP.

Tables

Table 1. Table 1: Numbers of solved instances and cumulative running time (in seconds; each timeout adds 600 seconds) on instances from benchmarks (i) and (ii) .

			clasp			wasp-cm			wasp-opt			wasp-cb			wasp-cb-20%
Benchmark	#		sol.	sum t		sol.	sum t		sol.	sum t		sol.	sum t		sol.	sum t
CQA-Q3	40		40	4354		40	1313		40	1276		40	1291		40	1303
CQA-Q6	40		40	8505		40	2149		40	1956		40	3544		40	1849
CQA-Q7	40		40	8929		40	1741		40	1681		40	1735		40	1724
MCSQ	73		60	12701		65	11007		73	1995		60	15757		73	5924
GracefulGraphs	1		1	51		1	45		1	32		1	44		1	57
GraphCol	1		0	600		0	600		0	600		0	600		0	600
IncrSched	6		5	857		2	2692		1	3016		1	3006		1	3004
KnightTour	2		2	62		0	1200		0	1200		0	1200		0	1200
Labyrinth	32		6	18377		0	19200		0	19200		0	19200		1	18912
NoMystery	2		1	1091		1	694		0	1200		1	706		1	721
PPM	15		15	264		15	81		15	76		15	113		15	76
QualSpatReas	18		18	1019		17	4537		7	7406		7	7083		14	5707
Sokoban	36		3	20529		3	20665		1	21102		1	21023		2	20918
VisitAll	2		2	80		2	408		1	757		2	348		2	396
Total	308		233	78584		226	66931		219	62097		208	76252		230	62993

Equations

$$\begin{array}[]{llll}ruleName&S&\Longrightarrow\ S^{\prime}&\textrm{if}\left\{\ conditions\right.\end{array}$$

$$\begin{array}[]{llll}\mathit{Oracle}&{L}_{O,U,A}&\Longrightarrow\ {L^{\prime}}_{O,U,A}&\textrm{if}\left\{\ L=\emptyset\right.\end{array}$$

$$\begin{array}[]{llll}\lx@intercol\textrm{Return rules}\hfil\lx@intercol\\ \mathit{Fail}_{\mathit{over}}&{L}_{O,U,\mathit{over}}&\Longrightarrow{\mathit{Cont}}({O},{O})&\textrm{if}\left\{\begin{array}[]{l}L\textrm{ is inconsistent}\end{array}\right.\\ \mathit{Find}&{L}_{O,U,A}&\Longrightarrow{\mathit{Cont}}({O\cap L},{U})&\textrm{if}\left\{\begin{array}[]{l}L\textrm{ is consistent and }L\neq\emptyset\end{array}\right.\\ \\ \lx@intercol\textrm{Control rules}\hfil\lx@intercol\\ \mathit{Terminal}&{\mathit{Cont}}({O},{U})&\Longrightarrow\mathit{Ok}(O)&\textrm{if}\left\{\begin{array}[]{l}O=U\end{array}\right.\\ \mathit{OverApprox}&{\mathit{Cont}}({O},{U})&\Longrightarrow{\emptyset}_{O,U,\mathit{over}}&\textrm{if}\left\{\begin{array}[]{l}O\neq U\end{array}\right.\\ \end{array}$$

$$\begin{array}[]{llll}\lx@intercol\textrm{Return rule}\hfil\lx@intercol\\ \mathit{Fail}_{\mathit{under}}&{L}_{O,U,\mathit{under}_{S}}&\Longrightarrow{\mathit{Cont}}({O},{U\cup S})&\textrm{if}\left\{\begin{array}[]{l}L\textrm{ is inconsistent, and }S=\emptyset\mbox{ or }S=\{a\}\end{array}\right.\\ \\ \lx@intercol\textrm{Control rule}\hfil\lx@intercol\\ \mathit{UnderApprox}&{\mathit{Cont}}({O},{U})&\Longrightarrow{\emptyset}_{O,U,\mathit{under}_{\{a\}}}&\textrm{if}\left\{\begin{array}[]{l}a\in O\setminus U\end{array}\right.\\ \end{array}$$

$$\begin{array}[]{l|l}\begin{array}[]{ll}\lx@intercol\mathit{\Pi}=\mathit{\Pi}_{\{a,b,c\},\emptyset,\mathit{under}_{\emptyset}}=\left\{\begin{array}[]{l}a\leftarrow\neg b\\ b\leftarrow\neg a\\ c\leftarrow a\\ c\leftarrow b\end{array}\right\}\hfil\lx@intercol\\ \\ \\ \\ \lx@intercol\mathit{\Pi}_{\{a,c\},\emptyset,\mathit{under}_{\{c\}}}=\mathit{\Pi}\cup\{\leftarrow c\}\hfil\lx@intercol\\ \\ \vspace{4pt}\\ \lx@intercol\mathit{\Pi}_{\{a,c\},\{c\},\mathit{under}_{\{a\}}}=\mathit{\Pi}\cup\{\leftarrow a\}\hfil\lx@intercol\\ \\ \\ \end{array}\par&\begin{array}[]{ll}&{\emptyset}_{\{a,b,c\},\emptyset,\mathit{under}_{\emptyset}}\\ \mathit{Oracle}\mbox{ :}&{ac{\neg b}}_{\{a,b,c\},\emptyset,\mathit{under}_{\emptyset}}\\ \mathit{Find}:&{\mathit{Cont}}({\{a,c\}},{\emptyset})\\ \\ \mathit{UnderApprox}:&{\emptyset}_{\{a,c\},\emptyset,\mathit{under}_{\{c\}}}\\ \mathit{Oracle}\mbox{ :}&{\neg{c}\neg{a}bc}_{\{a,c\},\emptyset,\mathit{under}_{\{c\}}}\\ \mathit{Fail}_{\mathit{under}}:&{\mathit{Cont}}({\{a,c\}},{\{c\}})\\ \\ \mathit{UnderApprox}:&{\emptyset}_{\{a,c\},\{c\},\mathit{under}_{\{a\}}}\\ \mathit{Oracle}\mbox{ :}&{\neg{a}bc}_{\{a,c\},\{c\},\mathit{under}_{\{a\}}}\\ \mathit{Find}:&{\mathit{Cont}}({\{c\}},{\{c\}})\\ \mathit{Terminal}:&\mathit{Ok}(\{c\})\end{array}\end{array}$$

$$\begin{array}[]{llll}\lx@intercol\textrm{Return rules}\hfil\lx@intercol\\ \mathit{Fail}_{\mathit{chunk}}&{L}_{O,U,\mathit{chunk}_{N}}&\Longrightarrow{\mathit{Cont}}({O\setminus N},{U\cup N})&\textrm{if}\left\{\begin{array}[]{l}L\textrm{ is inconsistent}\end{array}\right.\\ \\ \lx@intercol\textrm{Control rules}\hfil\lx@intercol\\ \mathit{Chunk}&{\mathit{Cont}}({O},{U})&\Longrightarrow{\emptyset}_{O,U,\mathit{chunk}_{N}}&\textrm{if}\left\{\begin{array}[]{l}N\subseteq O\setminus U\textrm{ and }N\neq\emptyset\end{array}\right.\\ \end{array}$$

$$\begin{array}[]{l|l}\begin{array}[]{ll}\lx@intercol\mathit{\Pi}=\mathit{\Pi}_{\{a,b,c,d\},\emptyset,\mathit{chunk}}=\left\{\begin{array}[]{l}a\leftarrow\neg b\\ b\leftarrow\neg a\\ c\leftarrow a\\ c\leftarrow b\\ d\leftarrow c\end{array}\right\}\hfil\lx@intercol\\ \\ \\ \lx@intercol\mathit{\Pi}_{\{a,c,d\},\emptyset,\mathit{chunk}_{\{c,d\}}}=\mathit{\Pi}\cup\{\leftarrow c,d\ \}\hfil\lx@intercol\vspace{1cm}\\ \\ \lx@intercol\mathit{\Pi}_{\{a,c,d\},\{c,d\},\mathit{chunk}_{\{a\}}}=\mathit{\Pi}\cup\{\leftarrow a\}\hfil\lx@intercol\\ \\ \\ \end{array}\par&\begin{array}[]{ll}&{\emptyset}_{\{a,b,c,d\},\emptyset,\mathit{chunk}}\par\\ \mathit{Oracle}\mbox{ :}&{ac\neg bd}_{\{a,b,c,d\},\emptyset,\mathit{chunk}}\\ \mathit{Find}:&{\mathit{Cont}}({\{a,c,d\}},{\emptyset})\\ \\ \mathit{Chunk}:&{\emptyset}_{\{a,c,d\},\emptyset,\mathit{chunk}_{\{c,d\}}}\\ \mathit{Oracle}\mbox{ :}&{\neg{a}bcd\neg{d}}_{\{a,c,d\},\emptyset,\mathit{chunk}_{\{c,d\}}}\\ \mathit{Fail}_{\mathit{chunk}}:&{\mathit{Cont}}({\{a,c,d\}},{\{c,d\}})\\ \\ \mathit{Chunk}:&{\emptyset}_{\{a,c,d\},\{c,d\},\mathit{chunk}_{\{a\}}}\\ \mathit{Oracle}\mbox{ :}&{\neg{a}bcd}_{\{a,c,d\},\{c,d\},\mathit{chunk}_{\{a\}}}\\ \mathit{Find}:&{\mathit{Cont}}({\{c,d\}},{\{c,d\}})\\ \mathit{Terminal}:&\mathit{Ok}(\{c,d\})\\ \\ \end{array}\end{array}$$

$$\begin{array}[]{llll}\mathit{CoreOracle}&L_{O,U,\mathit{core}_{N}}&\Longrightarrow\ L^{\prime}_{O,U,\mathit{core}_{N}}&\textrm{if}\left\{\ L=\emptyset\right.\end{array}$$

$$\begin{array}[]{llll}\lx@intercol\textrm{Return rules}\hfil\lx@intercol\\ \mathit{Fail}^{1}_{pre}&L_{O,U,\mathit{core}_{N}}&\Longrightarrow\mathit{Pre}_{N\setminus\{l\}}(O,U\cup\{\bar{l}\})&\textrm{if}\left\{\begin{array}[]{l}L\mbox{ is inconsistent and }\widehat{L}\cap N=\{l\}\end{array}\right.\\ \mathit{Fail}^{2}_{pre}&L_{O,U,\mathit{core}_{N}}&\Longrightarrow\mathit{Pre}_{N\setminus\widehat{L}}(O,U)&\textrm{if}\left\{\begin{array}[]{l}L\mbox{ is inconsistent and }|\widehat{L}\cap N|>1\end{array}\right.\\ \mathit{Find}_{\mathit{pre}}&L_{O,U,\mathit{core}_{N}}&\Longrightarrow\mathit{Eval}(O\cap L,U)&\textrm{if}\left\{\begin{array}[]{l}\textrm{}L\mbox{ is consistent and }L\neq\emptyset\end{array}\right.\\ \\ \lx@intercol\textrm{Control rules}\hfil\lx@intercol\\ Main&\mathit{Pre}_{N}(O,U)&\Longrightarrow\mathit{Cont}(O,U)&\textrm{if}\left\{\begin{array}[]{l}N=\emptyset\end{array}\right.\\ Continue&\mathit{Pre}_{N}(O,U)&\Longrightarrow\emptyset_{O,U,\mathit{core}_{N}}&\textrm{if}\left\{\begin{array}[]{l}\textrm{}N\neq\emptyset\end{array}\right.\\ \mathit{NewSet}&\mathit{Eval}(O,U)&\Longrightarrow\emptyset_{O,U,\mathit{core}_{\overline{O}}}&\textrm{if}\left\{\begin{array}[]{l}O\neq U\end{array}\right.\\ \mathit{Final}&\mathit{Eval}(O,U)&\Longrightarrow\mathit{Ok}(O)&\textrm{if}\left\{\begin{array}[]{l}O=U\end{array}\right.\\ \end{array}$$

$$\begin{array}[]{l|l}\begin{array}[]{ll}\lx@intercol\Pi_{\{a,b,c\},\emptyset,\mathit{core}_{\{\lnot a,\lnot b,\lnot c\}}}=\left\{\begin{array}[]{l}a\leftarrow\neg b\\ b\leftarrow\neg a\\ c\leftarrow a\\ c\leftarrow b\end{array}\right\}\cup\left\{\begin{array}[]{l}\leftarrow a\\ \leftarrow b\\ \leftarrow c\end{array}\right\}\hfil\lx@intercol\\ \\ \\ \lx@intercol\Pi_{\{a,b,c\},\{c\},\mathit{core}_{\{\lnot a,\lnot b\}}}=\left\{\begin{array}[]{l}a\leftarrow\neg b\\ b\leftarrow\neg a\\ c\leftarrow a\\ c\leftarrow b\end{array}\right\}\cup\left\{\begin{array}[]{l}\leftarrow a\\ \leftarrow b\\ \end{array}\right\}\hfil\lx@intercol\\ \end{array}\par&\begin{array}[]{ll}&\emptyset_{\{a,b,c\},\emptyset,\mathit{core}_{\{\lnot a,\lnot b,\lnot c\}}}\\ \mathit{CoreOracle}\mbox{ :}&c\lnot c_{\{a,b,c\},\emptyset,\mathit{core}_{\{\lnot a,\lnot b,\lnot c\}}}\\ \mathit{Fail}^{1}_{pre}\mbox{ :}&\mathit{Pre}_{\{\lnot a,\lnot b\}}(\{a,b,c\},\{c\})\\ \mathit{Continue}\mbox{ :}&\emptyset_{\{a,b,c\},\{c\},\mathit{core}_{\{\lnot a,\lnot b\}}}\\ \\ \mathit{CoreOracle}\mbox{ :}&ab\lnot a\lnot b_{\{a,b,c\},\{c\},\mathit{core}_{\{\lnot a,\lnot b\}}}\\ \mathit{Fail}^{2}_{pre}\mbox{ :}&\mathit{Pre}_{\emptyset}(\{a,b,c\},\{c\})\\ \mathit{Main}\mbox{ :}&\mathit{Cont}(\{a,b,c\},\{c\})\end{array}\end{array}$$

Full text

In this paper, we design, implement and test novel abstract solutions for cautious reasoning tasks in ASP. We show how to improve the current abstract solvers for cautious reasoning in ASP with new techniques borrowed from backbone computation in SAT, in order to design new solving algorithms. By doing so, we also formally show that the algorithms for solving cautious reasoning tasks in ASP are strongly related to those for computing backbones of Boolean formulas. We implement some of the new solutions in the ASP solver wasp and show that their performance are comparable to state-of-the-art solutions on the benchmark problems from the past ASP Competitions. Under consideration for acceptance in TPLP.

1 Introduction

Abstract solvers are a method to formally analyse solving algorithms. In this methodology, the states of a computation are represented as nodes of a graph, the solving techniques as edges between such nodes, the solving process as a path in the graph, and formal properties of the algorithms are reduced to related graph properties. This framework enjoys some advantages w.r.t. traditional ways such as pseudo-code-based descriptions, e.g., being based on formal and well-known, yet simple, mathematical objects like graphs, which helps $(i)$ comparing solving algorithms by means of comparison of their related graphs, $(ii)$ mixing techniques in different algorithms in order to design novel (combination of) solving solutions, by means of mixing arcs in the related graphs, and $(iii)$ stating and proving formal properties of the solving algorithms, by means of reachability within the related graphs. Abstract solvers already proved to be a useful tool for formally describing, comparing and composing solving techniques in various fields such as Propositional Satisfiability (SAT) and Satisfiability Modulo Theories (SMT) [Nieuwenhuis et al. (2006)], Quantified SAT [Brochenin and Maratea (2015b)], Answer Set Programming [Lierler (2011), Lierler and Truszczynski (2011), Brochenin et al. (2014)], and Constraint ASP [Lierler (2014)]. In ASP, such methodology led even to the development of a new ASP solver, sup [Lierler (2011)]; however, abstract solvers have been so far mainly applied to ASP solvers for brave reasoning tasks where, given an input query and a knowledge base expressed in ASP, answers are witnessed by ASP solutions, i.e., stable models [Baral (2003), Eiter et al. (1997), Gelfond and Lifschitz (1988), Gelfond and Lifschitz (1991), Marek and Truszczyński (1998), Niemelä (1999)].

However, in ASP, also cautious reasoning has been deeply studied in the literature: answers here must be witnessed by all stable models. This task has found a significant number of interesting applications as well, including consistent query answering [Arenas et al. (2003), Manna et al. (2013)], data integration [Eiter (2005)], multi-context systems [Brewka and Eiter (2007)], and ontology-based reasoning [Eiter et al. (2008)]. Two well-known ASP solvers, i.e., dlv [Leone et al. (2006)] and clasp [Gebser et al. (2012)], have been extended for computing cautious consequences of ASP programs. More recently, \citeNAlvianoDR14 presented a unified, high-level view of such solving procedures, and designed several algorithms for cautious reasoning in ASP, including those implemented in dlv and clasp, borrowed from the backbone computation of Boolean formulas [Janota et al. (2015)]: all these techniques are implemented (and tested) on top of the ASP solver wasp [Alviano et al. (2015)].

In this paper we design, implement and test novel abstract solutions for cautious reasoning tasks in ASP. We show how to improve the current abstract solvers [Brochenin and Maratea (2015a)] for cautious reasoning in ASP with further techniques borrowed from backbone computation in SAT, in order to design new solving algorithms. In particular, we import a technique called “chunk”, which generalizes over- and under-approximation by testing a set soft atoms simultaneously for being added in the under-approximation, and core-based algorithms, which can be considered either a solution per se, or a way for pruning the set of atoms to be considered, given that they can not guarantee completeness. By doing so, we also formally show, through a uniform treatment, that the algorithms for solving cautious reasoning tasks in ASP are strongly related to those for computing backbones of Boolean formulas. Finally, we implement some of the new solutions in the ASP solver wasp: results of a wide experimental analysis confirm that abstract solvers are a useful tool also for designing abstract solving procedures, given the performances of the related implementations are overall comparable to state-of-the-art solutions on the benchmark problems from the past ASP Competitions.

The paper is structured as follows. Section 2 introduces needed preliminaries, including a review in Section 2.3 of current algorithms for cautious reasoning trough abstract solving methodology. Section 3 shows how the algorithms for computing backbones of Boolean formulas can be imported into ASP, to design new solving algorithms. It also contains a general theorem showing the relation between backbones computation in SAT and cautious reasoning in ASP. Section 4 then presents the results of the new solutions on devoted ASP benchmarks. The paper ends by discussing related work in Section 5, and by drawing conclusions in Section 6.

2 Preliminaries

In this section, we first recall basics on (ground) non-disjunctive answer set programming (ASP) and Boolean logic formulas in Conjunctive Normal Form (CNF). Then, we introduce the abstract solvers framework and its methodology. Finally, we recall existing abstract solvers for computing cautious consequences of ASP programs.

2.1 Boolean Formulas and Answer Set Programs

We define (ground) non-disjunctive ASP programs and CNF formulas so as to underline similarities, in order to make it easier in later sections to compare algorithms working on CNF formulas with those working on ASP programs.

Syntax.

Let $\Sigma$ be a propositional signature. An element $a\in\Sigma$ is called atom or positive literal. The negation of an atom $a$, in symbols $\neg a$, is called negative literal. Given a literal $l$, we define $|l|=a$, if $l=a$ or $l=\neg a$, for some $a\in\Sigma$. For a set of atoms $X\subseteq\Sigma$, a literal relative to $X$ is a literal $l$ such that $|l|\in X$, and $\mathit{lit}(X)$ is the set of all literals relative to $X$. We set $\bar{l}=a$, if $l=\neg a$, and $\bar{l}=\neg a$, if $l=a$. A clause is a finite set of literals (seen as a disjunction). A CNF formula is a finite set of clauses (seen as a conjunction). Given a set of literals $M$, we denote by $M^{+}$ the set of positive literals of $M$, by $M^{-}$ the set of negative literals of $M$, and by $\overline{M}$ the set $\{\bar{l}\mid l\in M\}$. We say that $M$ is consistent if it does not contain both a literal and its negation. A (non-disjunctive) rule is a pair $(A,B)$, written $A\leftarrow B$, where $B$ is a finite set of literals and $A$ is an atom or the empty set. We may write a rule as $A\leftarrow B^{+},B^{-}$, as an abbreviation for $A\leftarrow B^{+}\cup B^{-}$, and $A\leftarrow l,B$ as an abbreviation for $A\leftarrow\{l\}\cup B$. A program is a finite set of rules. Given a set of literals $M$, a program $\Pi$, and a CNF formula $\Phi$, we denote by ${\mathit{atoms}(M)}$, ${\mathit{atoms}(\mathit{\Pi})}$, and ${\mathit{atoms}(\Phi)}$ the set of atoms occurring in $M$, $\mathit{\Pi}$, and $\Phi$, respectively. It is important to emphasize here that the interpretation of negation is different in propositional formulas and in ASP programs. Indeed, in propositional formulas $\neg$ represents the classical negation, while in ASP programs it represents the negation by default.

Semantics.

An assignment to a set $X$ of atoms is a total mapping from $X$ to $\{\bot,\top\}$. We identify a consistent set $M$ of literals with an assignment to ${\mathit{atoms}(M)}$ such that $a\in M$ iff $a$ is mapped to $\top$, and $\neg a\in M$ iff $a$ is mapped to $\bot$. A classical model of a CNF formula $\Phi$ is an assignment $M$ to ${\mathit{atoms}(\Phi)}$ such that for each clause $C\in\Phi$, $M\cap C\neq\emptyset$. A classical model of a program $\mathit{\Pi}$ is an assignment $M$ to ${\mathit{atoms}(\mathit{\Pi})}$ such that for each rule $(A,B)$ $\in$ $\mathit{\Pi}$, $A\cap M\neq\emptyset$ or $B\not\subseteq M$. We denote $M(\Phi)$ (resp. $M(\Pi)$) the set of all classical models of $\Phi$ (resp. $\Pi$). The reduct $\mathit{\Pi}^{X}$ of a program $\mathit{\Pi}$ w.r.t. a set of atoms $X$ is obtained from $\mathit{\Pi}$ by deleting each rule $A\leftarrow B^{+},B^{-}$ such that $X\cap{\mathit{atoms}(B^{-})}\neq\emptyset$ and replacing each remaining rule $A\leftarrow B^{+},B^{-}$ with $A\leftarrow B^{+}$. An answer set (or stable model) of a program $\mathit{\Pi}$ is an assignment $M$ to ${\mathit{atoms}(\mathit{\Pi})}$ such that $M^{+}$ is minimal among the $M_{0}^{+}$ such that $M_{0}$ is a classical model of $\mathit{\Pi}^{M^{+}}$. We denote by $AS(\Pi)$ the set of all answer sets of $\Pi$. Given a formula $\Phi$ and a program $\Pi$, we define $\mathit{backbone}(\Phi)=\bigcap_{M\in M(\Phi)}M^{+}$and $\mathit{cautious}(\mathit{\Pi})=\bigcap_{M\in AS(\Pi)}M^{+}$.

Example 1

Consider the following program $\mathit{\Pi}=\{a\leftarrow\neg b,\ b\leftarrow\neg a,\ c\leftarrow a,\ c\leftarrow b\}$. $\Pi$ has two answer sets, namely $A_{1}=\{\neg a,b,c\}$ and $A_{2}=\{a,\neg b,c\}$. Hence, $A_{1}^{+}=\{b,c\}$ and $A_{2}^{+}=\{a,c\}$. Therefore, $\mathit{cautious}(\mathit{\Pi})=\{b,c\}\cap\{a,c\}=\{c\}$. Now, consider the following CNF formula $\Phi=\{a\vee b,\neg a\vee c,\neg b\vee c\}$. $\Phi$ has three classical models, namely $M_{1}=\{\neg a,b,c\}$, $M_{2}=\{a,\neg b,c\}$, and $M_{3}=\{a,b,c\}$. Hence, $M_{1}^{+}=\{b,c\}$, $M_{2}^{+}=\{a,c\}$, and $M_{3}^{+}=M_{3}$. Therefore, $\mathit{backbone}(\Phi)=\{b,c\}\cap\{a,c\}\cap\{a,b,c\}=\{c\}$.

2.2 Abstract Solvers for Solving CNF Formulas and ASP Programs

Now, we introduce the abstract solvers framework and its methodology employed later on in Section 2.3 and Section 3 for computing cautious consequences of ASP programs. As we have mentioned in the introduction, abstract solvers are graphs that represent the status of the computation, and how it changes in response to an application of a technique in a search for a solution with certain properties, e.g., the satisfiability of a formula. Correspondingly, in the next paragraphs we first present the concept of a state, i.e., all possible paths of the computation in terms of assignments, then the transition rules are introduced, that showing how the state changes as a consequence of an application of a search technique if some conditions are met. The last paragraph of this subsection introduces abstract solver graphs, where the states are the possible nodes of the graph, while transition rules define arcs among reachable nodes.

States.

Given a set of atoms $X$, an action relative to $X$ is an element of the set $\mathcal{A}(X)=\{\mathit{over},\mathit{under}_{\emptyset}\}\cup\{\mathit{under}_{\{a\}}\mid a\in X\}$. For a set $X$ of atoms, a record relative to $X$ is a string $L$ from $\mathit{lit}(X)$ without repetitions. A record $L$ is consistent if it does not contains both a literal and its negation. We may view a record as the set containing all its elements stripped from their annotations. For example, we may view $\neg ab$ as $\{\neg a,b\}$, and hence as the assignment that maps $a$ to $\bot$ and $b$ to $\top$. Given a set $X$ of atoms, the set of states relative to $X$, written $V_{X}$, is the union of:

• $(i)$

the set of core states relative to $X$, that are all ${L}_{O,U,A}$ such that $L$ is a record relative to $X$; $O$, $U$ $\in X$; and $A\in\mathcal{A}(X)$;

• $(ii)$

the set of control states relative to $X$, that are all the ${\mathit{Cont}}({O},{U})$ where $O$, $U$ $\in X$; and

• $(iii)$

the set of terminal states relative to $X$, that are all $\mathit{Ok}(W)$, where $W\in X$.

Intuitively, these states represent computation steps of the algorithms that search for assignments with certain properties, in our case being backbone or cautious consequence. The computation starts from a specific core state, called initial state, depending on the specific algorithm (concrete examples are given later when presenting the techniques). Other core states ${L}_{O,U,A}$ and the control states ${\mathit{Cont}}({O},{U})$ represent all the intermediate steps of the computation, where $L$ is the current state of the computation of a model; $O$ is the current over-approximation of the solution; $U$ is the current under-approximation of the solution; and $A$ is the action currently carried out: $\mathit{over}$ (resp. $\mathit{under}_{\emptyset}$ or $\mathit{under}_{\{a\}}$) if over-approximation (resp. under-approximation) is being applied. Intuitively, a core state represents the computation within a call to an ASP oracle, i.e., an ASP solver, while a control state controls the computation between different calls to ASP oracles, depending on over-approximation and under-approximation. The terminal states represent the end of the computation, i.e., the termination of the algorithm.

For instance, consider the following set of atoms $X=\{a,b,c\}$. Hence, $lit(X)=\{a,b,c,\neg a,$ $\neg b,\neg c\}$. Therefore, $\neg ab_{\{a,b\},\emptyset,\mathit{over}}$ is an example of core state relative to $X$ where $a$ is assigned to false and $b$ to true, the over-approximation is the set $\{a,b\}$ while the under-approximation is empty, and the action executed is over. Other examples of core states are $\emptyset_{\{a\},\{b\},\mathit{under}_{\emptyset}}$ and $\neg a\neg b\neg c_{\emptyset,\emptyset,\mathit{under}_{\{a\}}}$. Instead, $\mathit{Cont}(\{a,b\},\{a\})$, $\mathit{Cont}(\{a,b,c\},\emptyset)$, $\mathit{Cont}(\emptyset,\emptyset)$ are examples of control states relative to $X$, where e.g., in the first example the over-approximation is the set $\{a,b\}$ and the under-approximation is $\{a\}$. $\mathit{Ok}(\{a,b,c\})$ and $\mathit{Ok}(\emptyset)$ are examples of terminal states relative to $X$, where set $\{a,b,c\}$ and $\emptyset$ are solutions.

Transition Rules.

Transition rules are represented with the following structure:

[TABLE]

where, $(i)$ $ruleName$ is the name of the rule; $(ii)$ $S\Longrightarrow S^{\prime}$ represents a transition from the starting state $S$ to the arriving state $S^{\prime}$ (if the rule is applied); and $(iii)$ $conditions$ is a set of conditions for the rule to be applicable.

We also consider a special transition rule, called $\mathit{Oracle}$, which starts from a state $L_{O,U,A}$ and arrives to a state $L^{\prime}_{O,U,A}$, if $L=\emptyset$. In symbols:

[TABLE]

Intuitively, the $\mathit{Oracle}$ rule represents an oracle call to an ASP [resp., SAT] solver by providing as result a set of literals $L^{\prime}$ corresponding to the output of an ASP [resp., SAT] solver, i.e., $L^{\prime}$ will correspond to an answer set of a logic program [resp., a classical model of a Boolean formula], if such an answer set [resp. classical model] exists, and to an inconsistent set of literals, otherwise. Transition rules in our paper are organized into $\mathit{Return}$ and ${Control}$ rules. Return rules deal with the outcome of an oracle call, or the application of a given technique, depending on the status of the set of literals $L$ returned, while Control rules start from a control state an direct the computation depending on the content of the over- and under-approximation.

Abstract Solver Graphs.

Given a set of atoms $X$ and a set of transition rules $T$, we define an abstract solver graph $G_{X,T}=\langle V_{X},E_{T}\rangle$, where $(S,S^{\prime})\in E_{T}$ if, and only if, a transition rule of the form $S\Longrightarrow S^{\prime}$ can be applied. We also denote the set of edges $E_{T}$ by the set of transition rules $T$. We say that a state $S\in V_{X}$ is reachable from a state $S^{\prime}\in V_{X}$, if there is a path from $S^{\prime}$ to $S$. Every state reachable from the initial state is called reachable state, and represents a possible state of a computation. Each path starting from the initial state represents the description of possible search for a certain model. We say that no cycle is reachable if there is no reachable state which is reachable from itself. Finally, note that transition rules $T$ and the set $X$ will depend from the specific input program $\Pi$, thus instead of writing $G_{X,T}$, we will write just $G_{\Pi}$.

2.3 Naive Abstract Solvers for Computing Cautious Consequences

In this section, we recall the abstract over-approximation, under-approximation and mixed strategies for computing cautious consequences of ASP programs.

Definition 1

Given a program $\Pi$ [resp., a CNF formula $\Phi$], we say that an abstract solver graph $G_{\Pi}$ [resp., $G_{\Phi}$] solves cautious reasoning [resp., backbone computation], if $(i)$ $G_{\Pi}$ [resp., $G_{\Phi}$] is finite and no cycle is reachable; and $(ii)$ the unique terminal reachable state in $G_{\Pi}$ [resp., $G_{\Phi}$] is $Ok(cautious(\Pi))$ [resp., $Ok(backbone(\Pi))$].

In the following, without loss of generality, we only focus on the computation of cautious consequences for an ASP program $\Pi$.

General Structure.

Given a program $\Pi$, over-approximation is set to all atoms in the program, i.e., $O={\mathit{atoms}(\Pi)}$, while the under-approximation is empty, i.e., $U=\emptyset$. Note that $U\subseteq\mathit{cautious}(\Pi)\subseteq O$. Iteratively either under-approximation or over-approximation are applied. When they coincide, i.e., $U=O$, the set of cautious consequences, i.e., $O$, has been found and the computation terminates. It means that the state $\mathit{Ok}(O)$ is a reachable state. Hence, the full extent of states relative to $X$ becomes useful. The unique terminal state is $\mathit{Ok}(W)$, where $W$ is the set of all cautious consequences of $\Pi$.

Over-approximation.

Let $\mathit{\Pi}_{O,U,\mathit{over}}$ $=$ $\mathit{\Pi}\cup\{\leftarrow O\}$. The initial state is ${\emptyset}_{{\mathit{atoms}(\mathit{\Pi})},\emptyset,\mathit{over}}$. We call $\mathit{ov}$ the set of all the rules reported in Figure 1, that is $\mathit{ov}=\{\mathit{Fail}_{\mathit{over}},\linebreak[1]\mathit{Find},\linebreak[1]\mathit{Terminal},\linebreak[1]\mathit{OverApprox}\}$. Intuitively, $\mathit{Fail}_{\mathit{over}}$ means that a call to an oracle did not find an answer set, so $O$ is the solution. If $\mathit{Find}$ is triggered, instead, we go to a control state where $O$ is updated according to the answer set found: then, if $O=U$ a solution is found through $\mathit{Terminal}$, otherwise the search is restarted ($L=\emptyset$) in an oracle state with $\mathit{OverApprox}$. For any $\mathit{\Pi}$, the graph $\mathit{OS}_{\mathit{\Pi}}$ is $(V_{{\mathit{atoms}(\mathit{\Pi})}},\{\mathit{Oracle}\}\cup\mathit{ov})$. Thus, in $\mathit{OS}_{\mathit{\Pi}}$, the oracle is called to find answer sets that reduce the over-approximation $O$ in the $\mathit{over}$ action, unless no answer set exists. If an answer set $M$ is found, then $M\cap\overline{O}\neq\emptyset$, as $\mathit{\Pi}_{O,U,\mathit{over}}$ $=$ $\mathit{\Pi}\cup\{\leftarrow O\}$.

Indeed, assume by contradiction that $M\cap\overline{O}=\emptyset$, then $O\subseteq M$. Hence, $M$ is not a model of the rule $(\emptyset,O)$, as $M\cap\emptyset=\emptyset$ and $O\subseteq M$. Therefore, $M$ should not be a model of $\mathit{\Pi}_{O,U,\mathit{over}}$, against the assumption that $M$ is an answer set of $\mathit{\Pi}_{O,U,\mathit{over}}$.

Under-approximation.

Let $\mathit{\Pi}_{O,U,\mathit{under}_{\{a\}}}$ $=$ $\mathit{\Pi}\cup\{\leftarrow a\}$ and $\mathit{\Pi}_{O,U,\mathit{under}_{\emptyset}}$ $=$ $\mathit{\Pi}$. The initial state is ${\emptyset}_{{\mathit{atoms}(\mathit{\Pi})},\emptyset,\mathit{under}_{\emptyset}}$. We call $\mathit{un}$ the set $\{\mathit{Fail}_{\mathit{under}},\linebreak[1]\mathit{Find},\linebreak[1]\mathit{Terminal},\linebreak[1]\mathit{UnderApprox}\}$ containing the rules presented in Figure 2 plus $\mathit{Find}$ and $\mathit{Terminal}$ from Figure 1. Intuitively, $\mathit{Fail}_{\mathit{under}}$ updates over- and under-approximations in case a test on the atom $a$ failed, and leads to a control state, while $\mathit{UnderApprox}$ restarts a new test if $\mathit{Find}$ is not applicable. For any $\mathit{\Pi}$, the graph $\mathit{US}_{\mathit{\Pi}}$ is $(V_{{\mathit{atoms}(\mathit{\Pi})}},\{\mathit{Oracle}\}\cup\mathit{un})$. In $\mathit{US}_{\mathit{\Pi}}$, again, a first oracle call takes place with the action $\mathit{under}_{\emptyset}$, which provides first over-approximation, then calls with actions $\mathit{under}_{\{a\}}$, where the element $a$ is the tested atom. Figure 3 shows a possible path in $\mathit{US}_{\mathit{\Pi}}$ for the program $\Pi$ of Example 1. For compactness, the syntax in which the path is presented is slighly different, with “$\Longrightarrow$” replaced by “:”, and with the initial state not explicitly tagged.

Mixed strategy.

An abstract mixed strategy can be obtained by defining $\mathit{MixS}_{\mathit{\Pi}}$ as $(V_{{\mathit{atoms}(\mathit{\Pi})}},$ $\{\mathit{Oracle}\}\cup\mathit{un}\cup\mathit{ov})$. Therefore, it is possible to combine techniques described by the graph for over-approximation and those in the graph for under-approximation, by envisaging the design of new additional algorithms. Here, we have two potential initial states, i.e., $\emptyset_{\mathit{atoms}(\Pi),\emptyset,A}$, where $A\in\{\mathit{over},\mathit{under}_{\emptyset}\}$, i.e., depending whether over-appoximation or under-approximation is first applied.

3 Advanced Abstract Solvers for Computing Cautious Consequences

In this section we import in ASP further algorithms from [Janota et al. (2015)] through abstract solvers. First, we generalize the concepts of under- and over-approximation via chunks, which consider a set of atoms simultaneously. Then, we model core-based algorithms. Finally, we state a general theorem, which includes all previous results, that shows how the techniques presented can be combined to design new solving methods for finding cautious consequences of ASP programs, and states a strong analogy between algorithms for computing cautious consequences of ASP programs and those for backbones of CNF formulas.

The sets of states now include also the following: $\{\mathit{chunk}_{N}|N\subseteq{\mathit{atoms}(\mathit{\Pi})}\}$, ${\mathit{chunk}}$ and $\{\mathit{core}_{N}|N\subseteq lit({\mathit{atoms}(\mathit{\Pi})})\}$.

3.1 Chunking

In [Janota et al. (2015)] a more general technique for under-approximation that allows to test multiple literals at once is presented (see, Algorithm 5 in [Janota et al. (2015)]). We define $\mathit{ch}$ as the set $\{\mathit{Fail}_{\mathit{chunk}},\linebreak[1]\mathit{Find},\linebreak[1]\mathit{Terminal},\linebreak[1]\mathit{Chunk}\}$ containing the rules presented in Figure 4 plus $\mathit{Find}$ and $\mathit{Terminal}$ from Figure 1. The newly introduced rules in Figure 4 model the new technique. In particular, $\mathit{Fail}_{\mathit{chunk}}$ updates the over- and under-approximations accordingly in case the test on the set $N$ fails (the ASP oracle call failed, thus all literals in $N$ must be cautious consequences), and goes to a control state. Meanwhile, $\mathit{Chunk}$ restarts a new ASP oracle call with a new (nonempty) set $N$ such that $N\subseteq O\setminus U$ in case the computation must continue (cf. condition of this transition rule). For any $\mathit{\Pi}$, the graph $\mathit{CS}_{\mathit{\Pi}}$ is $(V_{{\mathit{atoms}(\mathit{\Pi})}},\{\mathit{Oracle}\}\cup\mathit{ch})$. The initial state is ${\emptyset}_{{\mathit{atoms}(\mathit{\Pi})},\emptyset,\mathit{chunk}}$. We define $\mathit{\Pi}_{O,U,\mathit{chunk}_{N}}$ as $\mathit{\Pi}\cup\{\leftarrow N\}$.

Theorem 1

Let $\Pi$ be a program. Then, the graph $\mathit{CS}_{\mathit{\Pi}}$ solves cautious reasoning.

In order to design a meaningful example of Chunk, we slightly modify our running example adding the rule $d\leftarrow c$. Figure 5 shows a possible path in $\mathit{CS}_{\mathit{\Pi}}$ for the new defined program.

3.2 Designing New Abstract Solvers

The composition of techniques described in Section 2.3 and 3.1 can be readily applied to computing cautious consequences of a program, but actually is not included in any solver. This outlines another important feature of the abstract solvers methodology, i.e., its capability to design new solutions by means of combination of techniques implemented in different solvers.

More generally, it is possible to mix under-approximation, over-approximation, and chunking technique, and apply them for computing either cautious consequences or backbones. We next state a general theorem that subsumes all the techniques previously described, showing a strong analogy among the algorithms for computing cautious consequences and those for backbones.

Theorem 2

For any program $\mathit{\Pi}$, and for any set $S\subseteq\{\mathit{un},\mathit{ov},\mathit{ch}\}$ such that $S\neq\emptyset$, the graph $(V_{{\mathit{atoms}(\mathit{\Pi})}},$ $\{\mathit{Oracle_{ASP}}\}\cup\bigcup_{x\in S}x)$ solves cautious reasoning, and the graph $(V_{{\mathit{atoms}(\mathit{\Pi})}},$ $\{\mathit{Oracle_{SAT}}\}\cup\bigcup_{x\in S}x)$ solves backbone computation, where $\mathit{Oracle_{ASP}}$ and $\mathit{Oracle_{SAT}}$ represent an oracle call to an ASP solver and to a SAT solver, respectively.

3.3 Core-based Methods

We now model core-based algorithms from [Janota et al. (2015)] in terms of abstract solvers, in particular Algorithm 6, and apply it to the computation of cautious consequences of ASP programs. First, note that $\Pi_{O,U,\mathit{core}_{N}}$ is $\Pi\cup\{\leftarrow\overline{l}|l\in N\}$, and $\emptyset_{atoms(\Pi),\emptyset,\mathit{core}_{\overline{atoms(\Pi)}}}$ is the initial state. Moreover, given a logic program $\Pi$, we say that a set $C\subseteq lit(atoms(\Pi))$ is a core of $\Pi$, if $\Pi\cup\{\leftarrow\overline{l}|l\in C\}$ is incoherent. It is important to emphasize here that this definition is in line with the one proposed by \citeNAlvianoDJMP18. In particular, unsatisfiable cores have two important properties:

• •

if $C$ is an unsatisfiable core of $\Pi$ then all of its supersets are also unsatisfiable cores of $\Pi$;

• •

an atom $p\in atoms(\Pi)$ is a cautious consequence of $\Pi$ if and only if $\{\neg p\}$ is an unsatisfiable core (Proposition 4.1 of [Alviano et al. (2018)]).

Moreover, in general unsatisfiable cores are not guaranteed to be minimal, albeit several strategies can be used to obtain a minimal unsatisfiable core [Lynce and Silva (2004), Alviano and Dodaro (2016), Alviano et al. (2018)].

Example 2

Consider the program $\Pi$ of the Example 1 and let $N=\{\lnot a,\lnot b,\lnot c\}$. Hence, $\{\lnot c\}$, $\{\lnot a,\lnot c\}$, $\{\lnot b,\lnot c\}$, $\{\lnot a,\lnot b\}$, and $\{\lnot a,\lnot b,\lnot c\}$ are all cores of $\Pi_{O,U,\mathit{core}_{N}}$.

First, we consider a transition rule, called $\mathit{CoreOracle}$, which starts from a state $\emptyset_{O,U,\mathit{core}_{N}}$ and arrives to a state $L^{\prime}_{O,U,\mathit{core}_{N}}$. In symbols:

[TABLE]

The $\mathit{CoreOracle}$ rule represents an oracle call to compute a set of literals $L^{\prime}$, which is an inconsistent set of literals such that the set $\widehat{L^{\prime}}=\{\neg a\mid\{a,\neg a\}\subseteq L^{\prime}\}$ is a core of $\Pi_{O,U,\mathit{core}_{N}}$ and a subset of $N$, whenever $\mathit{\Pi}_{O,U,\mathit{core}_{N}}$ is incoherent; and is an answer set of $\Pi_{O,U,\mathit{core}_{N}}$, otherwise. Then, we define $\mathit{in}$ as the set of rules of Figure 6. Therefore, we consider a graph $\mathit{FS}_{\mathit{\Pi}}=(V_{\mathit{atoms}(\mathit{\Pi})},\{\mathit{CoreOracle}\}\cup\mathit{in})$ which represents Algorithm 6 in [Janota et al. (2015)]. Here, we need to introduce two intermediate control states: $\mathit{Pre}_{N}$ and $\mathit{Eval}$. In particular, $\mathit{Pre}_{N}$ is reached in case of inconsistency, where $N$ is the set of literals that may be used for the potential upcoming $\mathit{core}$ action; while $\mathit{Eval}$ is reached in case of consistency. From an outermost state, of the type $\mathit{Eval}$, a new $\mathit{core}$ is started with $\mathit{NewSet}$, whenever there is a gap between over- and under-approximation; otherwise, the $\mathit{Final}$ control rule leads to the terminal state. $\mathit{Fail}^{1}_{\mathit{pre}}$ and $\mathit{Fail}^{2}_{\mathit{pre}}$ lead to the intermediate type of control state, $\mathit{Pre}_{N}$, that can either restart a $\mathit{core}$ action with $Continue$, or continue with the $Main$ rule. Figure 7 shows a possible path in $\mathit{FS}_{\Pi}$ for the program $\Pi$ of Example 1.

Theorem 3

Let $\Pi$ be a program, and let $O$ and $U$ be two set of atoms. Then, $(i)$ the only reachable terminal states are either $Cont(O,U)$ or $Ok(O)$; $(ii)$ if $Ok(O)$ is reachable in $FS_{\Pi}$, then $FS_{\Pi}$ solves cautious reasoning; $(iii)$ if $Cont(O,U)$ is reachable in $FS_{\Pi}$, then $U\subseteq\mathit{cautious}(\Pi)\subseteq O$.

Chunking and core-based methods can be combined using our methodology to abstract Algorithm 7 from [Janota et al. (2015)]. Such a combination will be employed in the experiments.

4 Experimental Analysis

The abstract solvers reported in this paper have been used for implementing several algorithms in the ASP solver wasp [Alviano et al. (2015), Alviano et al. (2019)], resulting in the following new versions of wasp:

• •

wasp-chunk-2, i.e., wasp running the algorithm based on chunking, with the size of the chunk set to 2;

• •

wasp-chunk-20%, i.e., wasp running the algorithm based on chunking, with the size of the chunk set to the 20% of the initial number of candidates, where the initial set of candidates is the whole set of atoms;

• •

wasp-cb, i.e., wasp running the algorithm based on cores.

• •

wasp-cb-2, i.e., wasp running the algorithm based on cores and chunking, with the size of the chunk set to 2;

• •

wasp-cb-20%, i.e., wasp running the algorithm based on cores and chunking, with the size of the chunk set to the 20% of the initial number of candidates.

Benchmark selection.

The performance of these versions of wasp was measured on the benchmarks considered in [Alviano et al. (2018)]. In particular, [Alviano et al. (2018)] includes (i) all the 193 instances from the latest ASP Competitions [Calimeri et al. (2014), Calimeri et al. (2016), Gebser et al. (2017)] involving non-ground queries; (ii) 115 instances of ASP Competitions classified as easy, that is, those for which a stable model is found within 20 seconds of computation by mainstream ASP systems; and (iii) instances from abstract argumentation frameworks submitted to the 2nd International Competition on Computational Models of Argumentation. In this paper, instances from (iii) are not included since they are trivial for all tested solvers [Alviano et al. (2018)].

Compared approaches.

As a reference to the state of the art, we used clasp v. 3.3.3 [Gebser et al. (2012)], which implements algorithm or (i.e., over-approximation), and the best performing algorithms implemented by wasp [Alviano et al. (2014), Alviano et al. (2018)], namely or (i.e., over-approximation), ict (i.e., under-approximation), $\textsc{opt},$ and cm.

Algorithm opt was presented in [Alviano et al. (2018)]. The idea is as follows. Given a set of objective atoms $A$, the branching heuristic of the solver is forced to select $\neg p$ for $p\in A$, before any other unassigned literal. In this way, the search is driven to falsify as many atoms in $A$ as possible. When all atoms in $A$ are assigned, standard answer set search procedure is applied without further modifications to the branching heuristic. Therefore, whenever an answer set is found, it is guaranteed to be minimal with respect to the set of objective atoms [Di Rosa et al. (2010)]. When the current assignment to atoms in $A$ cannot be extended to an answer set, then the assignment of some atom in $A$ is flipped, and hence the procedure is repeated with a different assignment for the objective atoms. For cautious reasoning, $A$ is initialized to the set of all candidates and updated whenever an answer set is found.

Algorithm cm was also presented in [Alviano et al. (2018)] and is based on the property that an atom is a cautious consequence of a given program if and only if the negation of the atom is an unsatisfiable core. Hence, the algorithm searches for an answer set falsifying all candidates, with the aim of eliminating all remaining candidates at once. As soon as no such an answer set exists, the returned unsatisfiable core is either minimized to a singleton or used to discard candidates.

Note that all tested algorithms take advantage of the incremental interface of clasp and wasp, which is based on the concept of assumptions literals. The incremental interface allows the solver to reuse part of the computation among different calls, e.g., learned constraints and heuristic parameters.

The dlv solver is not considered here as its performance on cautious reasoning has been shown in earlier work to be dominated by the other approaches considered in [Alviano et al. (2014)].

Hardware configurations and limits.

The experiments were run on computing nodes with Intel Xeon 2.4-GHz processors and 16 GB of memory. Time and memory limits were set to 600 seconds and 15 GB, respectively.

4.1 Results

Concerning benchmark (i), results are shown in the cactus plot of Figure 8, where for each algorithm the number of solved instances in a given time is reported, producing an aggregated view of its overall performance. As a first observation, wasp cannot reach the performance of clasp on the execution of algorithm or, and indeed clasp solved 41 instances more than wasp-or. However, such a huge gap is completely filled by wasp-cb-20%, which actually solves 13 instances more than clasp. Indeed, wasp-cb-20% is able to solve all instances with an average running time of 56 seconds, and is comparable to the best performing algorithm, namely wasp-opt, which solves all instances with an average running time of 36 seconds. Notably, even a small size of the chunk may have a huge impact on the performance of the algorithms. Indeed, wasp-cb outperforms wasp-cb-2, solving 13 instances more. Finally, we observe that wasp-chunk-20% and wasp-chunk-2 are not competitive with algorithms based on cores.

Concerning benchmark (ii), results are shown in the cactus plot of Figure 9. It is possible to observe that clasp is the best performing solver on this benchmark, solving 53 instances overall. If we focus on wasp, the best performance is obtained by wasp-chunk-2, wasp-or, wasp-cm, and wasp-chunk-20% which are able to solve 41, 41, 41, and 40 instances, respectively. Moreover, wasp-cb cannot reach the same performance on this benchmark, solving only 25 instances. We observe that the poor performance depends on the first calls to the oracle, since they are expensive in terms of solving time. This negative effect is mitigated by chunking since wasp-cb-20% and wasp-cb-2 solve 37 and 39 instances, respectively.

Finally, detailed results of benchmarks (i) and (ii) are shown in Table 1, where we report the 5 algorithms solving the largest number of instances. In particular, for each algorithm we report the number of solved instances and the cumulative solving time (for each timeout we added 600 seconds). We also observe that wasp-cb-20% is comparable with clasp solving only 3 instances less.

5 Related Work

Abstract solvers methodology for describing solving procedures have been introduced for the dpll procedure with learning of SAT solving and for certain extensions implemented in SMT solvers [Nieuwenhuis et al. (2006)]. In ASP, \citeNlier08 introduced and compared the abstract solvers for smodels and cmodels on non-disjunctive programs, then in [Lierler (2011)] the framework has been extended by introducing transition rules that capture backjumping and learning techniques. \citeNlier11 presented a unifying perspective based on completion of solvers for non-disjunctive answer set solving. \citeNblm14 presented abstract solvers for disjunctive answer set solvers cmodels, gnt and dlv implementing plain backtracking, and \citeNlie14 defined abstract frameworks for Constraint ASP solvers.

All these papers describe ASP procedures for computing (one) stable models in abstract solvers methodology. In our paper we have, instead, focused on the description of ASP procedures for cautious reasoning tasks, possibly employing some of the solutions presented in related papers as ASP oracle calls. Our paper significantly extends the short technical communication [Brochenin and Maratea (2015a)] by $(i)$ designing more advanced solving techniques, like chunking and core-based algorithms, that lead to new solving solutions, $(ii)$ implementing and testing such new solutions, $(iii)$ adding further examples and a detailed related work, and $(iv)$ formally stating a strong analogy between backbones computation in SAT and cautious reasoning in ASP.

As far as the application of abstract solvers methodology outside ASP is concerned, the first application has been already mentioned and is related to the seminal paper [Nieuwenhuis et al. (2006)], where SMT problems with certain logics via a lazy approach [Sebastiani (2007)] are considered. Then, abstract solvers have been presented for the satisfiability of Quantified Boolean Formulas by \citeNbro15, and for solving certain reasoning taks in Abstract Argumentation under preferred semantics [Brochenin et al. (2018)]. Finally, in another number of papers, starting from a developed concept of modularity in answer set solving [Lierler and Truszczynski (2013)], abstract modeling of solvers for multi-logic systems are presented [Lierler and Truszczynski (2014), Lierler and Truszczynski (2015), Lierler and Truszczynski (2016)].

Another added, general, value of our paper is in its practical part, i.e., an implementation of new solutions designed through abstract solvers. In fact, while nowadays abstract solvers methodology has been widely used, often in the mentioned papers the presented results have rarely led to implementations, with the exception of [Nieuwenhuis et al. (2006)], where the related Barcelogic implementation won the SMT Competition 2005 on same logics, and [Lierler (2011)], where a proposed combination of smodels and cmodels techniques has been implemented in the solver sup, that reached positive results at the ASP Competition 2011 and, more recently, [Brochenin et al. (2018)], where the new designed solution, obtained as a modification of the cegartix solver, performed often better than the basic cergatix solver on preferred semantics, that was among the best solvers in the first ICCMA competition.

Finally, very recently improved algorithms for computing cautious consequences of ASP programs have been presented in [Alviano et al. (2018)]: such algorithms could be also modeled through abstract solvers and combined with the ones presented in this paper.

6 Conclusion

In this paper we modeled through abstract solvers advanced techniques for solving cautious reasoning tasks in ASP. Such advanced techniques have been borrowed from the computation of backbones of propositional formulas. We have then designed new solving procedures, and implemented them in wasp, that already included algorithms of [Alviano et al. (2014), Alviano et al. (2018)]. Experiments on devoted benchmarks have shown positive results for the new proposed solutions. At the same time, our work has formally stated, through an uniform treatment, a strong analogy among the algorithms for computing backbones of propositional formulas and those for computing cautious consequences of ASP programs. Finally, we remark that algorithms presented in this paper are independent with respect to the underlying solving strategies, and can be complemented with existing heuristics and optimization techniques [Giunchiglia et al. (2002), Giunchiglia et al. (2003), Giunchiglia et al. (2008)].

Appendix A Proofs

A.1 Correctness of the Oracle

Definitions.

For a program $\mathit{\Pi}$ and a type of model $w\in\{\mathit{cla},\mathit{sta}\}$, we say that $M$ is a $w$-model of $\mathit{\Pi}$ when either $w$ is $\mathit{sta}$ and $M$ is a stable model of $\mathit{\Pi}$ or $w$ is $\mathit{cla}$ and $M$ is a classical model of $\mathit{\Pi}$. We define $M_{\mathit{cla}}={\mathit{atoms}(\mathit{\Pi})}$ and $M_{\mathit{sta}}={\mathit{atoms}(\mathit{\Pi})}$. Also $T_{\mathit{cla}}=\mathit{backbone}(\mathit{\Pi})$ and $T_{\mathit{sta}}=\mathit{cautious}(\mathit{\Pi})$. We say that $(\mathit{\Pi},w,S,G)$ is a suitable quadruple when $\mathit{\Pi}$ is a program, $w\in\{\mathit{cla},\mathit{sta}\}$, $S\subseteq\{\mathit{un},\mathit{ov},\mathit{ch}\}$, and $G=(V_{{\mathit{atoms}(\mathit{\Pi})}},\{\mathit{Oracle}\}\cup\bigcup_{x\in S}x)$.

Lemma 1

Let $(\mathit{\Pi},w,S,G)$ be a suitable quadruple, and let ${L}_{O,U,A}$ be a reachable state from ${\emptyset}_{M_{w},\emptyset,B}$ in $G$, where $B\in\{\mathit{over},\mathit{under}_{\emptyset},\mathit{chunk}\}$. There is a path in $G$ from ${\emptyset}_{O,U,A}$ to ${L}_{O,U,A}$ that does not contain any control state.

Proof A.4**.**

Let ${L}_{O,U,A}$ be a state reachable from ${\emptyset}_{M_{w},\emptyset,B}$ in $G$, where $B\in\{\mathit{over},\mathit{under}_{\emptyset},\mathit{chunk}\}$. Assume it is reachable without going through any control state; in this case $A=B$, $U=\emptyset$ and $O=M_{w}$ as the $\mathit{Oracle}$ rule does not modify these. Otherwise a path $H$ leading to ${L}_{O,U,A}$ goes through some control state; and after the last control state in this path, a rule among $\{\mathit{UnderApprox},$ $\mathit{OverApprox},$ $\mathit{Chunk}\}$ has been applied, which involves that the state occurring right after applying this rule was ${\emptyset}_{O^{\prime},U^{\prime},A^{\prime}}$ for some $O^{\prime}$, $U^{\prime}$ and $A^{\prime}$. The $\mathit{Oracle}$ rule does not modify these components of oracle states, and additionally, by the choice of the last control state in $H$ as the predecessor of ${\emptyset}_{O^{\prime},U^{\prime},A^{\prime}}$, there is no control state in the part of $H$ from ${\emptyset}_{O^{\prime},U^{\prime},A^{\prime}}$ to ${L}_{O,U,A}$. So necessarily $O^{\prime}=O$, $U^{\prime}=U$ and $A^{\prime}=A$. Hence, in any case there is a path from ${\emptyset}_{O,U,A}$ to ${L}_{O,U,A}$ that does not contain any control state.

Lemma A.5**.**

Let $(\mathit{\Pi},w,S,G)$ be a suitable quadruple, and let ${L}_{O,U,A}$ be a reachable state from ${\emptyset}_{M_{w},\emptyset,B}$ in $G$, where $B\in\{\mathit{over},\mathit{under}_{\emptyset},\mathit{chunk}\}$. If the rule $\mathit{Fail}_{A}$ applies to ${L}_{O,U,A}$ in $G$, then $\mathit{\Pi}_{O,U,A}$ has no $w$-model; and, if the rule $\mathit{Find}$ applies, then $L$ is a $w$-model of $\mathit{\Pi}_{O,U,A}$.

Proof A.6**.**

By Lemma 1, there is a path from ${\emptyset}_{O,U,A}$ to ${L}_{O,U,A}$ that does not contain any control state. Hence, this path is justified exclusively by the $\mathit{Oracle}$ rule.

First, assume that $w=\mathit{cla}$. Applying the results from \citeNnie06, the lemma holds in this case. If the rule $\mathit{Fail}_{A}$ applies to ${L}_{O,U,A}$ in $G$, then $\mathit{\Pi}_{O,U,A}$ has no classical model, and if the rule $\mathit{Find}$ applies then $L$ is a classical model of $\mathit{\Pi}_{O,U,A}$.

Second, assume that $w=\mathit{sta}$. Then, by the results of \citeNLierlerT14 the Lemma also holds in this case. Indeed, if the rule $\mathit{Fail}_{A}$ applies to ${L}_{O,U,A}$ in $G$, then $\mathit{\Pi}_{O,U,A}$ has no stable model; and if the rule $\mathit{Find}$ applies, then $L$ is a stable model of $\mathit{\Pi}_{O,U,A}$.

A.2 Correctness of the Structure

Lemma A.7**.**

Let $(\mathit{\Pi},w,S,G)$ be a suitable quadruple, and if a state ${L}_{O,U,A}$ or ${\mathit{Cont}}({O},{U})$ is reachable from ${\emptyset}_{M_{w},\emptyset,B}$ in $G$, where $B\in\{\mathit{over},\mathit{under}_{\emptyset},\mathit{chunk}\}$, then $U\subseteq T_{w}\subseteq O$.

Proof A.8**.**

We prove this lemma by induction on the path leading from ${\emptyset}_{M_{w},\emptyset,B}$ to ${L}_{O,U,A}$ or ${\mathit{Cont}}({O},{U})$. So as to initialize this induction, we simply note that ${\emptyset}_{M_{w},\emptyset,B}$ is such that $\emptyset\subseteq T_{w}\subseteq M_{w}$. Now, assume that a state is reachable from ${\emptyset}_{M_{w},\emptyset,B}$ in $G$ and that for any state on the path the lemma holds, in particular on its predecessor. We are going to prove that for this state the lemma holds.

First case: assume that the state is a core state ${L}_{O,U,A}$. If its predecessor is a core state, then the predecessor is ${L^{\prime}}_{O,U,A}$ for some $L^{\prime}$, since the $\mathit{Oracle}$ rule does not modify these $O$, $U$ and $A$. By the induction hypothesis, the lemma holds. If its predecessor is a control state then note that the control rules that may link this predecessor to ${L}_{O,U,A}$ are $\mathit{OverApprox}$, $\mathit{UnderApprox}$ and $\mathit{Chunk}$, of which none modifies the over-approximation and under-approximation; hence, the predecessor is ${\mathit{Cont}}({O},{U})$ and by the induction hypothesis the lemma holds.

Second case: when the state is a control state. Then, its predecessor is a core state ${L}_{O,U,A}$. By the induction hypothesis, $U\subseteq T_{w}\subseteq O$. The rule applied is a return rule.

• •

If the rule is $\mathit{Terminal}$, then the state is ${\mathit{Cont}}({O\cap L},{U})$. By Lemma A.5, $L$ is a $w$-model of $\mathit{\Pi}_{O,U,A}$. So no element of $M_{w}\setminus L$ belongs to $T_{w}$, and no element of $L$ can be part of $T_{w}$. Hence, $U\subseteq T_{w}\subseteq O\cap L$.

• •

If the rule is $\mathit{Fail}_{\mathit{under}}$, then the state is ${\mathit{Cont}}({O},{U\cup\{a\}})$. By Lemma A.5, $\mathit{\Pi}_{O,U,A}$ has no $w$-model. So no $w$-model of $\mathit{\Pi}$ satisfies $a$. So $a$ belongs to $T_{w}$. Hence, $U\cup\{a\}\subseteq T_{w}\subseteq O$.

In all cases the lemma holds, which ends the proof by induction.

Lemma A.9**.**

Let $(\mathit{\Pi},w,S,G)$ be a suitable quadruple, and let ${L}_{O,U,A}$ be a reachable state from ${\emptyset}_{M_{w},\emptyset,B}$ in $G$, where $B\in\{\mathit{over},\mathit{under}_{\emptyset},\mathit{chunk}\}$. If $\mathit{Fail}_{\mathit{over}}$ applies to ${L}_{O,U,A}$, then $T_{w}=O$.

Proof A.10**.**

Assume that $\mathit{Fail}_{\mathit{over}}$ applies to some state ${L}_{O,U,A}$ reachable from ${\emptyset}_{M_{w},\emptyset,B}$. Then $A=\mathit{over}$. The path has to go through at least one control state so that $A\neq B$, and hence the rule $\mathit{Find}$ has to have been applied; so $\mathit{\Pi}$ has at least one $w$-model and $T_{w}$ is well defined. Also, by Lemma A.5, $\mathit{\Pi}_{O,U,\mathit{over}}$ has no $w$-model. In other words, $\mathit{\Pi}\cup\{\leftarrow O\}$ has no $w$-model. As the constraint added to $\mathit{\Pi}$ is monotonic, $\mathit{\Pi}$ has no $w$-model satisfying $\leftarrow O$. In other words, all the $w$-models of $\mathit{\Pi}$ satisfy $O$, so $O\subseteq T_{w}$. Since, by Lemma A.7, $T_{w}\subseteq O$, also $T_{w}=O$.

Lemma A.11**.**

Let $(\mathit{\Pi},w,S,G)$ be a suitable quadruple, and let ${L}_{O,U,A}$ be a reachable state from ${\emptyset}_{M_{w},\emptyset,B}$ in $G$, where $B\in\{\mathit{over},\mathit{under}_{\emptyset},\mathit{chunk}\}$. If there is a transition in $G$ from ${L}_{O,U,A}$ to ${\mathit{Cont}}({O^{\prime}},{U^{\prime}})$ and $A\neq B$, then $O^{\prime}\setminus U^{\prime}\subset O\setminus U$.

Proof A.12**.**

Assume that there is a transition in $G$ from ${L}_{O,U,A}$ to ${\mathit{Cont}}({O},{U})$ and $A\neq B$.

If this transition is justified by $\mathit{Fail}_{\mathit{chunk}}$ or $\mathit{Fail}_{\mathit{under}}$, then $A$ is $\mathit{chunk}_{N}$ or $\mathit{under}_{N}$ for some $N$. Also $O^{\prime}=O$ and $U^{\prime}=U\cup N$, so $O^{\prime}\setminus U^{\prime}\subseteq(O\setminus U)\setminus N$. The last control rule applied was necessarily $\mathit{Chunk}$, so that $N\subseteq O\setminus U$ and $N\neq\emptyset$. Then $(O\setminus U)\setminus N\subset O\setminus U$, so $O^{\prime}\setminus U^{\prime}\subset O\setminus U$.

If this transition is justified by $\mathit{Find}$, we first prove that $O\cap L\neq O$ and $U\subseteq L$. First, assume $A=\mathit{over}$. Then, by Lemma A.5, $L$ is a $w$-model of $\mathit{\Pi}_{O,U,\mathit{over}}=\mathit{\Pi}\cup\{\leftarrow O\}$. Therefore, $L$ is a $w$-model of $\mathit{\Pi}$ and a classical model of $\{\leftarrow O\}$. Since it is a $w$-model of $\mathit{\Pi}$ and $U\subseteq T_{w}$, by definition of $T_{w}$ also $U\subseteq L$. Since $L$ is a classical model of $\{\leftarrow O\}$, also $\overline{O}\cap L\neq\emptyset$. Hence, $O\cap L\neq O$. Now, assume $A=\mathit{chunk}_{N}$. The last control rule applied was necessarily $\mathit{Chunk}$, so that $N\subseteq O\setminus U$ and hence $N\subseteq O$. Also, by Lemma A.5, $L$ is a $w$-model of $\mathit{\Pi}_{O,U,\mathit{chunk}_{N}}=\mathit{\Pi}\cup\{\leftarrow N\}$, so $L$ is a $w$-model of $\mathit{\Pi}$ and a classical model of $\{\leftarrow N\}$, and $\overline{N}\cap L\neq\emptyset$. Since it is a $w$-model of $\mathit{\Pi}$ and $U\subseteq T_{w}$, by definition of $T_{w}$ also $U\subseteq L$. Since $L$ is a classical model of $\{\leftarrow N\}$, also $\overline{O}\cap L\neq\emptyset$, and hence $O\cap L\neq O$. The proof in the case of $\mathit{under}_{N}$ is identical to the case of $\mathit{chunk}_{N}$. So in any case $O\cap L\neq O$ and $U\subseteq L$. So $O^{\prime}\setminus U^{\prime}=(O\cap L)\setminus U$ is a strict subset of $O\setminus U$.

A.3 Finiteness and Lack of Reachable Cycles

Lemma A.13**.**

Let $\mathit{\Pi}$ be a program, and let $S\subseteq\{\mathit{un},\mathit{ov},\mathit{ch}\}$. Then, the graph $(V_{{\mathit{atoms}(\mathit{\Pi})}},\{\mathit{Oracle}\}\cup\bigcup_{x\in S}x)$ is finite.

Proof A.14**.**

Any core state relative to ${\mathit{atoms}(\mathit{\Pi})}$ is made of a record relative to ${\mathit{atoms}(\mathit{\Pi})}$, two sets of literals relative to ${\mathit{atoms}(\mathit{\Pi})}$, and one action relative to ${\mathit{atoms}(\mathit{\Pi})}$. The set $\mathit{lit}({\mathit{atoms}(\mathit{\Pi})})$ of literals relative to ${\mathit{atoms}(\mathit{\Pi})}$ is finite, and so is its powerset; hence there is only a finite amount of possibilities for the two sets of literals relative to ${\mathit{atoms}(\mathit{\Pi})}$. Also, since an action can only be $\mathit{over}$, $\mathit{chunk}_{M}$, or $\mathit{under}_{M}$ for $M$ a set of literals relative to ${\mathit{atoms}(\mathit{\Pi})}$, there is only a finite amount of possible actions. Finally, since the set of literals relative to ${\mathit{atoms}(\mathit{\Pi})}$ is finite, and so is its powerset; so there are only a finite amount of possible records relative to ${\mathit{atoms}(\mathit{\Pi})}$ since repetitions are not allowed in records. So there is a only finite amount of core states relative to $V_{{\mathit{atoms}(\mathit{\Pi})}}$. Since the other types of states are only made of a portion of what makes a core state, there is also a finite amount of them. As a consequence, $V_{{\mathit{atoms}(\mathit{\Pi})}}$ is finite, and hence the graph $(V_{{\mathit{atoms}(\mathit{\Pi})}},\{\mathit{Oracle}\}\cup\bigcup_{x\in S}x)$ is finite.

Lemma A.15**.**

Let $(\mathit{\Pi},w,S,G)$ be a suitable quadruple. Then, there is no cycle in $G$ reachable from the initial state ${\emptyset}_{M_{w},\emptyset,B}$, where $B\in\{\mathit{over},\mathit{under}_{\emptyset},\mathit{chunk}\}$.

Proof A.16**.**

We are going to define a partial order on $V_{{\mathit{atoms}(\mathit{\Pi})}}$.

First, we define an order on records as follows. For any record $L$, we consider the strings $L_{1},\dots,L_{i}$ such that each $L_{k}$, $1\leq k\leq i$, contains the literals assigned at level $i$. We define the order $<$ on string of integers as the lexicographic order on strings on integers. For any core state ${L}_{O,U,A}$ we define $0pt{{L}_{O,U,A}}$ as the string $2,0pt{L}$ if $A\neq B$, and $0,0pt{L}$ if $A=B$. We consider that any control state ${\mathit{Cont}}({O},{U})$ is such that $0pt{{\mathit{Cont}}({O},{U})}=1$, and any state $s$ that is a terminal state is such that $0pt{s}=3$.

We then define an order on the gap between over-approximation and under-approximation, which in general is $O\setminus U$. We define the functions $ove$ and $und$. For any state $s$, if $s$ is ${L}_{O,U,A}$ or ${\mathit{Cont}}({O},{U})$ then $ove(s)=O$ and $und(s)=U$, otherwise $ove(s)=\emptyset$ and $und(s)=\mathit{lit}({\mathit{atoms}(\mathit{\Pi})})$. For two sets of literals $M$ and $M^{\prime}$, we say that $M<M^{\prime}$ if $M^{\prime}\subseteq M$.

We write $\leq_{\mathit{lex}}$ to denote the lexicographic composition of orders. Then we define our order on states as follows. For any two states, $s<s^{\prime}$ iff $(ove(s)\setminus und(s),0pt{s})\leq_{\mathit{lex}}(ove(s^{\prime})\setminus und(s^{\prime}),0pt{s^{\prime}})$. The relations on $0pt{s}$ and $ove(s)\setminus und(s)$ are clearly partial orders. Hence the obtained lexicographic order is also a partial order. We are now going to show that any edge $(s,s^{\prime})$ in $\{\mathit{Oracle}\}\cup\bigcup_{x\in S}x$ such that $s$ is reachable from the initial state is such that $s<s^{\prime}$ and $s\neq s^{\prime}$. Assume that a state $s$ is reachable from the initial state and the rule $\mathit{Find}$, $\mathit{Fail}_{\mathit{under}}$ or $\mathit{Fail}_{\mathit{chunk}}$ applies to $s$ so as to create the edge $(s,s^{\prime})$. Then by Lemma A.11, $s<s^{\prime}$ and $s\neq s^{\prime}$. So, indeed, any edge $(s,s^{\prime})$ in $\{\mathit{Oracle}\}\cup\bigcup_{x\in S}x$ such that $s$ is reachable from the initial state is also such that $s<s^{\prime}$ and $s\neq s^{\prime}$. As a consequence, since the relation $<$ on states is a partial order and there is only a finite amount of ordered elements, there is no infinite path, and hence no cycle among the reachable elements of $(V_{{\mathit{atoms}(\mathit{\Pi})}},\{\mathit{Oracle}\}\cup\bigcup_{x\in S}x)$.

A.4 Proof of Theorem 2

By Lemmas A.13 and A.15, the graph $G=(V_{{\mathit{atoms}(\mathit{\Pi})}},\{\mathit{Oracle}\}\cup\bigcup_{x\in S}x)$ is finite and no cycle is reachable from the initial state. Assume a state ${L}_{O,U,A}$ is terminal in $G$; this is impossible since if no other rule applies then $\mathit{Find}$ applies. Similarly, assume a state ${\mathit{Cont}}({O},{U})$ is reachable and terminal in $G$. Either $O=U$ and $\mathit{Terminal}$ applies, or $O\neq U$ and, by Lemma A.7, $U\subset O$ so one of the rules of the nonempty set $\{\mathit{OverApprox},\mathit{UnderApprox},\mathit{Chunk}\}\cap\bigcup_{x\in S}x$ applies. In both cases a rule applies, which is a contradiction.

Therefore, the terminal state is $\mathit{Ok}(L)$ for some $L$. Hence, as to end the proof of the theorem we now study the type of state that can actually be terminal. Assume that $\mathit{Ok}(M)$ is the terminal state reachable from the initial state. Either it was reached by a transition justified by $\mathit{Fail}_{\mathit{over}}$ and, by Lemma A.9, in any state ${L}_{M,U,\mathit{over}}$ from which this transition may have originated holds $T_{w}=M$, or it was reached by a transition justified by $\mathit{Terminal}$ and, by Lemma A.7, in any state ${\mathit{Cont}}({M},{M})$ from which this transition may have originated holds $M\subseteq T_{w}\subseteq M$, hence $T_{w}=M$.