# query_answering_in_propositional_circumscription__2d7c0ac5.pdf

Query Answering in Propositional Circumscription

Mario Alviano University of Calabria alviano@mat.unical.it

Propositional circumscription defines a preference relation over the models of a propositional theory, so that models being subset-minimal on the interpretation of a set of objective atoms are preferred. The complexity of several computational tasks increases by one level in the polynomial hierarchy due to such a preference relation; among them there is query answering, which amounts to decide whether there is an optimal model satisfying the query. A complete algorithm for query answering is obtained by searching for a model, not necessarily an optimal one, that satisfies the query, and such that no model unsatisfying the query is more preferred. If the query or its complement are among the objective atoms, the algorithm has a simpler behavior, which is also described in the paper. Moreover, an incomplete algorithm is obtained by searching for a model satisfying both the query and an objective atom being unit-implied by the theory extended with the complement of the query. A prototypical implementation is tested on instances from the 2nd International Competition on Computational Models of Argumentation.

1 Introduction Circumscription [Mc Carthy, 1980] enforces the minimization of the extension of some predicates via a second order semantics. In the propositional case, such a minimization essentially selects subset minimal models. A revised version introduced the possibility to specify a set of atoms for grouping interpretations, and another set of atoms subject to minimization [Lifschitz, 1986]. In this form, circumscription is suitable for modeling several practical problems that are characterized by a preference relation over admissible solutions. Among them there are minimal diagnosis of faulty systems [Pereira et al., 1993; Jannach et al., 2016] and minimal correction subsets [Junker, 2004; Marques-Silva et al., 2013; Menc ıa et al., 2015]. The enumeration problem associated with propositional circumscription was recently addressed by modifying ONE [Alviano et al., 2015b; Alviano and Dodaro, 2016; 2017], an algorithm for Max SAT based on unsatisfiable core analysis

[Morgado et al., 2013]. Such an algorithm was implemented in CIRCUMSCRIPTINO and used by PYGLAF [Alviano, 2017a; 2017c] to solve several problems of the 2nd International Competition on Computational Models of Argumentation (ICCMA 17) [Gaggl et al., 2016] by means of linear translations into the framework of propositional circumscription. Among these problems there are credulous and skeptical acceptance of arguments, which essentially amount to decide whether a given argument belongs to respectively some or all extensions of the graph in input. Concerning acceptance problems, the contra of the strategy implemented by PYGLAF is that an enumeration algorithm provides a negative answer to credulous acceptance problems only after producing all models; a similar observation holds for positive answers to skeptical acceptance problems. This is in contrast with propositional logic and answer set programming, for which acceptance problems can be addressed efficiently by several algorithms [Alviano et al., 2014; 2018] implemented in WASP [Dodaro et al., 2011; Alviano et al., 2013; 2015a]. The pro of PYGLAF is that the underlying solver for circumscription is used as a black box, which means that a better solution for some computational problems of circumscription can be easily used also for argumentation reasoning. Motivated by the above analysis, the present paper provides algorithms for deciding the existence of a circumscribed model of the input theory satisfying a given query. More specifically, the framework is simplified in the form of a propositional theory associated with a set of objective literals subject to maximization (Section 2). A complete algorithm is obtained by searching for a model satisfying the query, and then by verifying that no model in which the query is unsatisfied is more preferred (Section 3); if this last check fails, a countermodel is identified, and the search for the next model satisfying the query is constrained to bypass the inhibition provided by the countermodel. An interesting aspect of this algorithm is that neither models nor countermodels are necessarily optimal models, and therefore queries may be answered without computing any optimal model. Moreover, the algorithm can be efficiently implemented by means of two SAT solvers, the first for producing models, and the second for producing countermodels (Section 6); the SAT solvers process propositional theories that are extended during the computation, and possibly subject to assumption literals, so that learned clauses are possibly reused in different computations.

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

The fact that the algorithm searches for a model and verifies the nonexistence of countermodels is justified by the complexity of query answering, which is in general ΣP 2 - complete for propositional circumscription [Eiter and Gottlob, 1993]. However, there are restricted cases for which the complexity of the problem drops by one level in the polynomial hierarchy. One of such cases is the occurrence of the query in the set of objective literals: any model I satisfying the query is sufficient to conclude the existence of an optimal model satisfying the query, as any model unsatisfying the query cannot be a countermodel of I. In this case, the second solver used by the algorithm immediately detects the nonexistence of any countermodel, and therefore does not add any overhead to the computation. A generalization of the previous case is obtained by noting that any objective literal ℓwhose complement is unit-implied by the theory extended with the complement of the query is such that the theory extended with ℓentails the query. Hence, any model satisfying ℓis sufficient to conclude the existence of an optimal model satisfying the query. Based on this observation, an incomplete algorithm is presented (Section 4), and possibly combined with the complete algorithm. Acceptance problems of abstract argumentation framework are mapped to query answering (Section 5), and the algorithms are tested empirically on instances of ICCMA 17 (Section 7). Specifically, preferred and semistable extensions are considered. The implemented solver is compared with ARGSEMSAT [Cerutti et al., 2013] and CEGARTIX [Dvor ak et al., 2014], reporting very positive results.

2 Background

Let A be a fixed, countable set of atoms. A literal is an atom possibly preceded by the connective . For a literal ℓ, let ℓ denote its complementary literal, that is, p = p and p = p for all p A; for a set L of literals, let L be {ℓ| ℓ L}. Formulas are defined as usual by combining atoms and the connectives , , , , , , and . A theory is a set Γ of formulas; the set of atoms occurring in Γ is denoted by atoms(Γ). An assignment is a set A of literals such that A A = . An interpretation for a theory Γ is an assignment I such that (I I) A = atoms(Γ). Relation |= is defined as usual: I |= ; I |= ; for p A, I |= p if p I; for φ and ψ formulas, I |= φ if I |= φ, I |= φ ψ if I |= φ and I |= ψ, I |= φ ψ if I |= φ or I |= ψ, I |= φ ψ if I |= ψ whenever I |= φ, and I |= φ ψ if either I |= φ and I |= ψ, or I |= φ and I |= ψ. I is a model of a theory Γ if I |= Γ. Let models(Γ) denote the set of models of Γ. Circumscription applies to a theory Γ and disjoint sets P, Z of atoms; atoms in P are subject to minimization, while atoms in Z are irrelevant. Formally, relation P Z is defined as follows: for I, J interpretations of Γ, I P Z J if both (A \ (P Z)) I = (A \ (P Z)) J and P I P J. I models(Γ) is a circumscribed model of Γ with respect to P Z if there is no J models(Γ) such that I P Z J and J P Z I. Let CIRC(Γ, P, Z) denote the set of circumscribed models of Γ with respect to P Z.

Algorithm 1: Anwer Query(Γ, O, q)

3 I := solve(Γ {q} (O I ));

4 if I = then

5 I := solve(Γ {q} {W O \ I} (O I));

6 if I = then return YES;

8 if I = then return NO;

9 Γ := Γ {W O \ I };

Example 1. Let Γ1 be { r a, z a}. Hence, CIRC(Γ1, {a}, {z}) contains {r, a, z}, { r, a, z}, and { r, a, z}. Note that {r, a, z} is a model of Γ1, but {r, a, z} {a}{z} {r, a, z}; similar for {r, a, z}.

The framework of circumscription is simplified by focusing on a theory Γ and on a set O of objective literals subject to maximization. A model I of Γ is optimal with respect to O if there is no I models(Γ) such that O I O I. Abusing of notation, let models(Γ, O) denote the set of optimal models of Γ with respect to O. Note that Γ1 from Example 1 satisfies models(Γ1, { a, r, r}) = CIRC(Γ1, {a}, {z}), and such a result holds in general.

Proposition 1. For any theory Γ, and any disjoint sets P, Z of atoms, CIRC(Γ, P, Z) = models(Γ, P R R), where R is atoms(Γ) \ (P Z).

The computational problem addressed in this paper, referred to as query answering, is the following: Given a theory Γ, a set O of objective literals, and a literal q called query, decide whether there is an optimal model I models(Γ, O) such that I |= q.

Example 2. Let Γrun be the theory {ϕ1 ϕ2 ϕ3 ϕ4 ϕ5}, where ϕi are the following subformulas:

ϕ1 := a b c q ϕ4 := a b c q ϕ2 := a b c q ϕ5 := a b c q ϕ3 := a b c q

The models of Γrun are I1 = { a, b, c, q}, I2 = { a, b, c, q}, I3 = { a, b, c, q}, I4 = {a, b, c, q}, and I5 = { a, b, c, q}. Let Orun be {a, b, c}. Hence, models(Γrun, Orun) is {I4, I5}. The answer to query q over Γrun and Orun is YES because of I4.

3 Complete Algorithm for Query Answering

The proposed strategy to address query answering is reported in Algorithm 1. The idea is to compute a model I of the the input theory Γ such that I |= q, and then check whether there exists no model I of Γ such that both O I O I and I |= q, where O is the set of objective literals. If such a model I does exist, a new model I is searched, this time with the additional requirement that O I O I . This process is repeated until no such an I can be found, witnessing that this branch of the search space does not contain any optimal

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

model making the query true. Hence, the branch is discarded by means of a blocking clause based on the last computed I , so that the algorithm can restart from a different branch. The algorithm can conclude the falsity of the query when no I is found after blocking a branch of computation. More in detail, model searches are performed by means of function solve, whose input is a theory Γ, and whose output is either if models(Γ) = , or a model I models(Γ). A blocking clause for a set of objective literals O and an interpretation I is the clause W O \ I; such a clause enforces the satisfaction of at least one objective literal being false according to I. The blocking clause can be combined with the set O I of formulas in order to enforce the search of a model I such that O I O I; indeed, note that O I alone enforces the search of a model I such that O I O I. Summing up, Algorithm 1 initially sets I to the empty set (line 1), so that a model of Γ {q} is searched at line 3. If a model I is found (line 4), a countermodel is searched, that is, a model I of Γ such that O I O I and I |= q (line 5). If function solve returns , then the algorithm terminates providing a positive answer (line 6); note that I is not necessarily an optimal model of Γ, but any model I of Γ such that O I O I must necessarily be such that I |= q. Otherwise, function solve returns a model I , and the algorithm continues from line 3 by searching for a model of Γ {q} such that O I O I . When the search for I terminates with , the algorithm distinguishes two cases: if I = , no model of Γ {q} does exist, and a negative answer is provided (line 8); otherwise, the current branch of computation is discarded by the blocking clause W O \ I (line 9), I is reset (line 10), and the algorithm restarts from line 3.

Example 3 (Continuing Example 2). The execution of Answer Query(Γrun, Orun, q) initially searches for a model I of Γrun such that I |= q (line 3); say that I1 is returned. The call to function solve at line 5 returns either I2 or I5; say that I2 is returned, that is, I is I2 in the next check at line 3. Hence, Orun I = {b}, and either I3 or I4 is returned; say that I3 is returned, so that theory Γrun { q} {a c} {b} is processed at line 5. Since is returned, the algorithm terminates at line 6 answering YES. Note that I3 is not optimal, but there is sufficient evidence that an optimal model satisfying the query does exist (in this case, I4). As for an alternative execution, consider the case in which the first call to solve at line 3 returns I1, and the first call at line 5 returns I5. Hence, I is I5 in the next check at line 3, and is returned because no model of Γrun satisfies both q and c. Therefore, the theory is extended with W Orun \ I5 = a b, and I is reset (lines 9 10). The next check at line 3 returns either I3 or I4, and the algorithm continues as in the previous execution.

Theorem 1. Let Γ be a theory, O be a set of literals, and q be a literal. Algorithm 1 terminates, and returns YES if there is I models(Γ, O) such that I |= q, and NO otherwise.

Proof. We shall show the following properties: (P1) no optimal model of Γ is discarded by the new clauses added at line 9; (P2) if YES is returned, there is I models(Γ, O) such that I |= q; (P3) if NO is returned, there is no I

Algorithm 2: Anwer Query(Γ, O {q}, q)

1 if solve(Γ {q}) = then return YES;

2 return NO;

models(Γ, O) such that I |= q; (P4) one of the return instructions at lines 6 and 8 is eventually executed. Concerning (P1), line 9 is executed only if I models(Γ) is such that I |= q, and for all I models(Γ) such that O I O I , it holds that I |= q; stated differently, any model I containing q is such that O I I , and therefore I |= W O \ I . Hence, Answer Query(Γ, O, q) = Answer Query(Γ {W O \ I }, O, q). Concerning (P2), YES is returned at line 6 only if there is no I models(Γ) such that I |= q, and O I O I, where I models(Γ) is such that I |= q. Hence, I |= q holds for all I models(Γ) such that O I O I. If I models(Γ, O), the claim holds (for I = I). Otherwise, there is I models(Γ) such that O I O I, and therefore I |= q. Concerning (P3), NO is returned at line 8 only if I = , and there is no I models(Γ) such that I |= q. Since models(Γ, O) models(Γ), the claim holds. Concerning (P4), let Ii, I i be the values of variables I, I at iteration i 0. If the return instructions are not reached at iteration i, then the algorithm is in one of two possible cases. In the first case, Ii = and Ii = . Since the new clause added to Γ discards at least one model, and the number of models of Γ is finite, this case occurs finitely many times during any execution. In the second case, Ii = and I i = . Hence, either O Ii+1 O I i O Ii (which is possible at most |O| consecutive times), or Ii+1 = (and the first case can occur finitely many times).

Algorithm 1 addresses query answering in the general setting. Interestingly, if either q or q is part of the objective literals, many calls to function solve are completed immediately because both q and q are formulas of the tested theory, which is therefore unsatisfiable. Specifically, if q O, the call to function solve at line 5 returns : q I because of line 3, and therefore q O I; hence, both q and q are part of the tested theory, which is trivially unsatisfiable. It turns out that in this case query answering can be achieved by a single call to function solve, as reported in Algorithm 2. Correctness of the algorithm follows from Theorem 1.

Corollary 1. Let Γ be a theory, O be a set of literals, and q be a literal. Algorithm 2 terminates, and returns YES if there is I models(Γ, O {q}) such that I |= q, and NO otherwise.

Example 4 (Continuing Example 3). The execution of Answer Query(Γrun, Orun {q}, q) initially searches for a model I of Γrun such that I |= q; as in the previous example, say that I1 is returned. The algorithm can already answer YES; in fact, Algorithm 1 would process the theory Γrun { q} {a b c} {q}, which is unsatisfiable.

On the other hand, if q O and I = , the call to function solve at line 3 of Algorithm 1 returns : q I because of line 5, and therefore q O I ; hence, both q and q

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

Algorithm 3: Anwer Query(Γ, O {q}, q)

2 I := solve(Γ {q});

3 if I = then return NO;

4 I := solve(Γ {q} (O I));

5 if I = then return YES;

6 Γ := Γ {W O \ I };

Algorithm 4: Incomplete Anwer Query(Γ, O, q)

1 for ℓ O such that solve(Γ {q} {ℓ}) = do

2 if solve(Γ {q} {ℓ}) = then return YES;

3 return UNKNOWN;

are part of the tested theory, which is trivially unsatisfiable. It turns out that blocking clauses can be immediately added after a countermodel is computed. Additionally, the theory processed at line 5 of Algorithm 1 can be simplified by removing the disjunction W O \ I, which necessarily contains q; similarly, blocking clauses at line 9 of Algorithm 1 necessarily contain q, which is necessarily false at line 3 and can be therefore removed. Such simplifications are reported in Algorithm 3, whose correctness follows from Theorem 1.

Corollary 2. Let Γ be a theory, O be a set of literals, and q be a literal. Algorithm 3 terminates, and returns YES if there is I models(Γ, O {q}) such that I |= q, and NO otherwise.

Example 5 (Continuing Example 3). The execution of Answer Query(Γrun, Orun { q}, q) initially searches for a model I of Γrun such that I |= q; as in the previous examples, say that I1 is returned. Say that the call to solve(Γrun { q} ) returns I2. The algorithm can already extend the theory with a c; in fact, Algorithm 1 would process the theory Γrun {q} {b, q}, which is unsatisfiable. After that, I4 is assigned to I, so that the next check at line 4 of Algorithm 3 returns , and the algorithm answers YES.

4 Incomplete Algorithm for Query Answering

The incomplete algorithm is based on the following property.

Lemma 1. Let Γ be a theory, O be a set of literals, and q be a literal. If there is O O such that models(Γ O {q}) = and models(Γ O {q}) = , then there is I models(Γ, O) such that I |= q.

Proof. Let I models(Γ O {q}). If I models(Γ, O), the claim holds (for I = I). Otherwise, consider any I models(Γ, O) such that O I O I O. Since models(Γ O {q}) = by assumption, and I |= Γ O , we conclude that I |= q.

Intuitively, the lemma above highlights a sufficient but not necessary condition to conclude that the query is true: if there is a set O of objective literals that can be extended to a model of Γ, and such that any extension to a model of Γ contains the query q, then there is also an optimal model of Γ with respect to O containing q.

The incomplete algorithm is reported as Algorithm 4. Since checking all subsets of O is impractical, the algorithm focuses on singletons. As will be clarified in Section 6, the algorithm can be further constrained to check only singletons {ℓ} such that models(Γ {q} {ℓ}) = is verifiable in polynomial time. Theorem 2. Let Γ be a theory, O be a set of literals, and q be a literal. Algorithm 4 terminates, and if it returns YES then there is I models(Γ, O) such that I |= q.

Proof. The algorithm performs at most 2 |O| satisfiability checks, so termination is guaranteed. It returns YES if there is ℓ O such that models(Γ {q} {ℓ}) = , and models(Γ {q} {ℓ}) = . Hence, correctness follows from Lemma 1 for O = {ℓ}.

Example 6 (Continuing Example 3). The execution of Incomplete Answer Query(Γrun, Orun, q) detects that solve(Γrun { q} {a}) = , and solve(Γrun {q} {a}) = I4. Hence, the algorithm returns YES.

5 Argumentation Acceptance Problems An abstract argumentation framework (AF) is a directed graph G whose nodes arg(G) are arguments, and whose arcs att(G) represent an attack relation. An extension E is a set of arguments, and its range is E+ := E {x | yx att(G) with y E}. Let CO(G) contain any extension E of G having the following properties: there are no x, y E with xy att(G) (conflict-free); for all yx att(G) such that x E, there is zy att(G) such that z E (admissible); if x arg(G) is such that for all yx att(G) there is zy att(G) with z E, then x E (complete). E is preferred if E CO(G), and there is no E CO(G) such that E E. E is semi-stable if E CO(G), and there is no E CO(G) such that E + E+. Let PR(G) and SST(G) denote respectively the set of preferred and semistable extensions of G. An argument x arg(G) is credulously accepted in a set S of extensions, denoted S |=c x, if there is E S such that x E. Argument x is skeptically accepted in S, denoted S |=s x, if x E for all E S. For an AF G, let pr(G) := { x y | xy att(G)} n ax W yx att(G) y, x V yx att(G) ay x arg(G) o ,

sst(G) := pr(G) n rx x W

yx att(G) y x arg(G) o .

Proposition 2. For any AF G, PR(G) = {I arg(G) | I models(pr(G), arg(G))}, and SST(G) = {I arg(G) | I models(sst(G), {rx | x arg(G)}). Credulous acceptance of x arg(G) in PR(G) can be tested by a call to Answer Query(pr(G), arg(G), x); note that the query is an objective literal, and therefore Corollary 1 applies. Skeptical acceptance of x arg(G) in PR(G) can be tested by a call to Answer Query(pr(G), arg(G), x), and by properly reverting the answer; note that x = x is an objective literal, and therefore Corollary 2 applies. Similarly, credulous acceptance of x arg(G) in SST(G) can be tested by a call to Answer Query(sst(G), {rx | x arg(G)}, x), while skeptical acceptance of x arg(G) in SST(G) can be tested by a

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

call to Answer Query(sst(G), {rx | x arg(G)}, x), and by properly reverting the answer.

6 Implementation Algorithm 1 has been implemented in the solver CIRCUMSCRIPTINO [Alviano, 2017b]. Model searches (i.e., function solve) are performed by means of the SAT solver GLUCOSE 4.1 [Audemard and Simon, 2009], with its default configuration. More in detail, two instances of the SAT solver are used, one for the calls performed at line 3, and one for the calls performed at line 5. Specifically, the first solver processes the theory Γ {q} and the set of assumption literals O I ; clause W O \ I is added to the theory at line 9. The second solver, instead, processes the theory Γ {q} {W O \ I} and the set of assumption literals O I; clause W O \ I is not removed after completing the model search, as the next call either adds W O \ I for I I (if I = ), or is preceded by the addition of W O \ I at line 9 for I such that O I O I. Possibly, the complete algorithm is aided by the incomplete algorithm. However, checking solve(Γ {q} {ℓ}) = and solve(Γ {q} {ℓ}) = for all ℓ O may require significant computational resources. Hence, a weaker version of the algorithm is implemented by checking solve(Γ {q} {ℓ}) = only for those literals ℓ O such that models(Γ{q} {ℓ}) = is easily detectable; intuitively, ℓ is considered only if ℓis derived by (unit) propagation on Γ {q}. For example, if Γ is {q a, q a b}, a and b are derived by (unit) propagation on Γ {q}; if O is {a, b}, then solve(Γ {q} {b}) = is checked. On the other hand, if Γ is {q a b, q a b}, no literal is derived by (unit) propagation on Γ {q}, even if models(Γ {q} {b}) = . Since the underlying theory Γ is modified during the execution of the complete algorithm, it may be the case that some new literal is derived by (unit) propagation. For this reason, the incomplete algorithm can be run either once at the beginning of the computation, or each time I is reset, giving two different strategies to address query answering.

7 Experiment The experiment comprises instances from ICCMA 17 related to credulous (DC) and skeptical (DS) acceptance problems for preferred (PR) and semi-stable (SST) semantics, and was run on an Intel Xeon 2.4 GHz with 16 GB of memory, and time and memory were limited to 10 minutes and 15 GB, respectively. Each benchmark comprises 350 testcases. The new version of CIRCUMSCRIPTINO is used by PYGLAF, and the execution time of the full pipeline is measured. A cactus plot of the overall performance is shown in Figure 1. The best performance is reached by PYGLAF with the incomplete algorithm disabled. Specifically, it solved 71 instances more than ARGSEMSAT and 127 more than CEGARTIX. The plot also highlights an initial overhead of PYGLAF with respect to ARGSEMSAT due to the construction of the propositional theory, which is implemented in Python. The scatter plots in Figure 2 provide an instance by instance comparison in terms of execution time. The comparison with ARGSEMSAT and CEGARTIX shows that there are

900 1,000 1,100 1,200 1,300 0

Number of solved instances

Running time (seconds)

PYGLAF: C + IO

PYGLAF: C + IR

Figure 1: Solved instances within a time budget; C is the complete algorithm, IO is the incomplete algorithm used once, and IR is the incomplete algorithm reiterated.

Solver PR SST PR SST Overall

ARGSEMSAT 331 291 306 289 1217 (11.3) (24.2) (19.3) (20.0) (18.5) CEGARTIX 322 311 264 264 1161 (33.9) (54.8) (63.8) (62.0) (52.7) PYGLAF: C 324 323 316 325 1288 (31.3) (35.0) (36.4) (34.7) (34.4) PYGLAF: C+IO 326 324 298 325 1273 (31.2) (33.4) (35.3) (35.1) (33.7) PYGLAF: C+IR 326 324 296 325 1271 (30.6) (32.7) (32.1) (34.7) (32.5)

Table 1: Solved instances and average execution time (in seconds, shown in parenthesis), and best performance emphasized in bold; C is the complete algorithm, IO is the incomplete algorithm used once, and IR is the incomplete algorithm reiterated.

several instances for which PYGLAF is not the fastest system, but it is still able to provide the correct answer within the allotted resources. Distinguishing on the different computational problems, the main advantage of PYGLAF emerges on the semi-stable semantics, which stimulates all features of Algorithm 1. Figure 2 also compares the different variants of PYGLAF, highlighting that the addition of the incomplete algorithm deteriorates the performance of the system for skeptical acceptance over preferred semantics, and otherwise it does not provide any influence.

Finally, a summary of the experiment is reported on Table 1, where the number of instances solved by each tested system within the allotted resources is shown. The table confirms that the main advantage of Algorithm 1 emerges on the semi-stable semantics, and that the addition of the incomplete algorithm deteriorated the performance of the system only for skeptical acceptance over preferred extensions.

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

DC-PR DC-SST DS-PR DS-SST

0 200 400 600 0

0 200 400 600 0

0 200 400 600 0

PYGLAF: C + IO

0 200 400 600 0

PYGLAF: C + IR

Figure 2: Instance by instance comparison on execution time; C is the complete algorithm, IO is the incomplete algorithm used once, and IR is the incomplete algorithm reiterated.

8 Related Work

The notion of query answering considered in this paper is the one addressed by ASPRIN [Romero et al., 2016], a system for knowledge bases subject to arbitrary preference relations, where knowledge bases and preference relations are expressed by means of answer set programs. Four different algorithms were implemented in ASPRIN, all of them based on the enumeration of optimal models, or on the enumeration of models followed by an optimality check. Hence, those algorithms are different from the algorithms proposed in this paper, whose main characteristic is essentially to not focus on optimal models. Answer set programming was also used to implement circumscription [Oikarinen and Janhunen, 2005] and argumentation frameworks [Egly et al., 2010]. ARGSEMSAT searches for optimal models of a propositional theory encoding the target semantics until one satisfies the query [Cerutti et al., 2013], and CEGARTIX searches for an optimal model of the theory extended with the query and being an optimal model of the original theory [Dvor ak et al., 2014]. Hence, again the optimality requirement is the main difference with the algorithms proposed in this paper. CEGARTIX also implements some semantic shortcuts, as for example for skeptical acceptance over preferred extensions the system first checks the existence of a complete extension attacking the query argument, which is sufficient to conclude the existence of a preferred extension violating the query. Indeed, in this case any extension being more preferred must also attack the query argument, which therefore cannot be part of the extension. Such a shortcut is obtained and generalized by the incomplete algorithm introduced in Section 4, as in fact arguments attacking the query argument are unit-

implied at line 1, possibly among other arguments. On the other hand, the shortcut of CEGARTIX only requires a single consistency check, which may be convenient in some cases.

9 Conclusion Querying models of circumscribed propositional theories is a computational task in the second level of the polynomial hierarchy, and therefore naturally addressed by procedures involving two SAT solvers. However, the two SAT solvers can be combined in several ways, and previous techniques in the literature focused on the computation of optimal models. On the other hand, the complete algorithm proposed in this paper does not enforce the search of optimal models, but focuses on models satisfying the query and (counter)models not satisfying the query. Empirical evidence of the performance gain of the proposed approach is given. The same empirical analysis highlights that the incomplete algorithm instead deteriorates the performance of the complete algorithm for skeptical acceptance over preferred extensions. Such a behavior suggests that the incomplete algorithm has to be run as a heuristic approach, and therefore subject to some restriction, as for example within a budget on the number of conflicts. The development of a heuristic strategy for limiting the execution of the incomplete algorithm is left as future work.

Acknowledgments This work was partially supported by the POR CALABRIA FESR 2014-2020 project DLV Large Scale (CUP J28C17000220006), by the EU H2020 PON I&C 2014-2020 project S2BDW (CUP B28I17000250008), and by GNCSINd AM.

References [Alviano and Dodaro, 2016] Mario Alviano and Carmine Dodaro. Anytime answer set optimization via unsatisfiable core shrinking. TPLP, 16(5-6):533 551, 2016. [Alviano and Dodaro, 2017] Mario Alviano and Carmine Dodaro. Unsatisfiable core shrinking for anytime answer set optimization. In Carles Sierra, editor, IJCAI 2017, Melbourne, Australia, August 19-25, 2017, pages 4781 4785, 2017. [Alviano et al., 2013] Mario Alviano, Carmine Dodaro, Wolfgang Faber, Nicola Leone, and Francesco Ricca. WASP: A native ASP solver based on constraint learning. In Pedro Cabalar and Tran Cao Son, editors, LPNMR 2013, Corunna, Spain, September 15-19, 2013. Proceedings, volume 8148 of LNCS, pages 54 66. Springer, 2013. [Alviano et al., 2014] Mario Alviano, Carmine Dodaro, and Francesco Ricca. Anytime computation of cautious consequences in answer set programming. TPLP, 14(4-5):755 770, 2014. [Alviano et al., 2015a] Mario Alviano, Carmine Dodaro, Nicola Leone, and Francesco Ricca. Advances in WASP. In Francesco Calimeri, Giovambattista Ianni, and Miroslaw Truszczynski, editors, LPNMR 2015, Lexington, KY, USA, September 27-30, 2015. Proceedings, volume 9345 of LNCS, pages 40 54. Springer, 2015.

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)

[Alviano et al., 2015b] Mario Alviano, Carmine Dodaro, and Francesco Ricca. A maxsat algorithm using cardinality constraints of bounded size. In Qiang Yang and Michael Wooldridge, editors, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 2677 2683. AAAI Press, 2015. [Alviano et al., 2018] Mario Alviano, Carmine Dodaro, Matti J arvisalo, Marco Maratea, and Alessandro Previti. Cautious reasoning in ASP via minimal models and unsatisfiable cores. Co RR, abs/1804.08480, 2018. [Alviano, 2017a] Mario Alviano. The ingredients of the argumentation reasoner pyglaf: Python, circumscription, and glucose to taste. In Marco Maratea and Ivan Serina, editors, RCRA 2017, Bari, Italy, November 14-15, 2017, volume 2011 of CEUR Workshop Proceedings, pages 1 16. CEUR-WS.org, 2017. [Alviano, 2017b] Mario Alviano. Model enumeration in propositional circumscription via unsatisfiable core analysis. TPLP, 17(5-6):708 725, 2017. [Alviano, 2017c] Mario Alviano. The pyglaf argumentation reasoner. In Ricardo Rocha, Tran Cao Son, Christopher Mears, and Neda Saeedloei, editors, ICLP 2017, August 28 to September 1, 2017, Melbourne, Australia, volume 58 of OASICS, pages 2:1 2:3. Schloss Dagstuhl - Leibniz Zentrum fuer Informatik, 2017. [Audemard and Simon, 2009] Gilles Audemard and Laurent Simon. Predicting learnt clauses quality in modern SAT solvers. In Craig Boutilier, editor, IJCAI 2009, Pasadena, California, USA, July 11-17, 2009, pages 399 404, 2009. [Cerutti et al., 2013] Federico Cerutti, Paul E. Dunne, Massimiliano Giacomin, and Mauro Vallati. Computing preferred extensions in abstract argumentation: A sat-based approach. In Elizabeth Black, Sanjay Modgil, and Nir Oren, editors, TAFA 2013, Beijing, China, August 3-5, 2013, Revised Selected papers, volume 8306 of LNCS, pages 176 193. Springer, 2013. [Dodaro et al., 2011] Carmine Dodaro, Mario Alviano, Wolfgang Faber, Nicola Leone, Francesco Ricca, and Marco Sirianni. The birth of a WASP: preliminary report on a new ASP solver. In Fabio Fioravanti, editor, CILC 2011, Pescara, Italy, August 31 - September 2, 2011, volume 810 of CEUR Workshop Proceedings, pages 99 113. CEUR-WS.org, 2011. [Dvor ak et al., 2014] Wolfgang Dvor ak, Matti J arvisalo, Johannes Peter Wallner, and Stefan Woltran. Complexitysensitive decision procedures for abstract argumentation. Artif. Intell., 206:53 78, 2014. [Egly et al., 2010] Uwe Egly, Sarah Alice Gaggl, and Stefan Woltran. Answer-set programming encodings for argumentation frameworks. Argument & Computation, 1(2):147 177, 2010. [Eiter and Gottlob, 1993] Thomas Eiter and Georg Gottlob. Propositional circumscription and extended closedworld reasoning are iip2-complete. Theor. Comput. Sci., 114(2):231 245, 1993.

[Gaggl et al., 2016] Sarah Alice Gaggl, Thomas Linsbichler, Marco Maratea, and Stefan Woltran. Introducing the second international competition on computational models of argumentation. In Matthias Thimm, Federico Cerutti, Hannes Strass, and Mauro Vallati, editors, SAFA, Potsdam, Germany, September 13, 2016., volume 1672 of CEUR Workshop Proceedings, pages 4 9. CEUR-WS.org, 2016. [Jannach et al., 2016] Dietmar Jannach, Thomas Schmitz, and Kostyantyn M. Shchekotykhin. Parallel model-based diagnosis on multi-core computers. J. Artif. Intell. Res. (JAIR), 55:835 887, 2016. [Junker, 2004] Ulrich Junker. QUICKXPLAIN: preferred explanations and relaxations for over-constrained problems. In Deborah L. Mc Guinness and George Ferguson, editors, Proceedings of the Nineteenth National Conference on Artificial Intelligence, Sixteenth Conference on Innovative Applications of Artificial Intelligence, July 25-29, 2004, San Jose, California, USA, pages 167 172. AAAI Press / The MIT Press, 2004. [Lifschitz, 1986] Vladimir Lifschitz. On the satisfiability of circumscription. Artif. Intell., 28(1):17 27, 1986. [Marques-Silva et al., 2013] Jo ao Marques-Silva, Federico Heras, Mikol as Janota, Alessandro Previti, and Anton Belov. On computing minimal correction subsets. In Francesca Rossi, editor, IJCAI 2013, Beijing, China, August 3-9, 2013, pages 615 622. IJCAI/AAAI, 2013. [Mc Carthy, 1980] John Mc Carthy. Circumscription - A form of non-monotonic reasoning. Artif. Intell., 13(1-2):27 39, 1980. [Menc ıa et al., 2015] Carlos Menc ıa, Alessandro Previti, and Jo ao Marques-Silva. Literal-based MCS extraction. In Qiang Yang and Michael Wooldridge, editors, IJCAI 2015, Buenos Aires, Argentina, July 25-31, 2015, pages 1973 1979. AAAI Press, 2015. [Morgado et al., 2013] Ant onio Morgado, Federico Heras, Mark H. Liffiton, Jordi Planes, and Jo ao Marques-Silva. Iterative and core-guided maxsat solving: A survey and assessment. Constraints, 18(4):478 534, 2013. [Oikarinen and Janhunen, 2005] Emilia Oikarinen and Tomi Janhunen. circ2dlp - translating circumscription into disjunctive logic programming. In Chitta Baral, Gianluigi Greco, Nicola Leone, and Giorgio Terracina, editors, LPNMR 2005, Diamante, Italy, September 5-8, 2005, volume 3662 of LNCS, pages 405 409. Springer, 2005. [Pereira et al., 1993] Lu ıs Moniz Pereira, Carlos Viegas Dam asio, and Jos e J ulio Alferes. Debugging by diagnosing assumptions. In Peter Fritszon, editor, AADEBUG 93, Link oping, Sweden, May 3-5, 1993, Proceedings, volume 749 of LNCS, pages 58 74. Springer, 1993. [Romero et al., 2016] Javier Romero, Torsten Schaub, and Philipp Wanko. Computing diverse optimal stable models. In Manuel Carro, Andy King, Neda Saeedloei, and Marina De Vos, editors, ICLP 2016 TCs, October 16-21, 2016, New York City, USA, volume 52 of OASICS, pages 3:1 3:14. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.

Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence (IJCAI-18)