Query Answering in Propositional Circumscription

1 Introduction

Circumscription [McCarthy, 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 MaxSAT 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.

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 ΣP2 - 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 ≤PZ is defined as follows: for I, J interpretations of Γ, I ≤PZ 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 ≤PZ if there is no J ∈ models(Γ) such that I ̸≤PZ J and J ≤PZ I. Let CIRC(Γ, P, Z) denote the set of circumscribed models of Γ with respect to ≤PZ .

1 I ′ := ∅; 2 loop 3 I := solve(Γ∪ {q} ∪ (O ∩ I ′ )); 4 if I ̸= ⊥ then 5 I ′ := solve(Γ∪ {q} ∪ {∨ O \ I} ∪ (O ∩ I)); 6 if I ′ = ⊥ then return YES; 7 else 8 if I ′ = ∅ then return NO; 9 Γ := Γ ∪ {∨ O \ I ′ }; 10 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:

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 newmodel 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 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 ∨ 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 ∨ O \ I ′ (line 9), I ′ is reset (line 10), and the algorithm restarts from line 3.

Example 3 (Continuing Example 2). The execution of AnswerQuery(Γ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 ∨ 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: AnwerQuery(Γ, 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 |= ∨ O \ I ′ . Hence, AnswerQuery(Γ,O, q) = AnswerQuery(Γ ∪ {∨ 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 AnswerQuery(Γ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 Algorithm 3: AnwerQuery(Γ, O ∪ {q}, q)

1 loop 2 I := solve(Γ∪ {q}); 3 if I = ⊥ then return NO; 4 I ′ := solve(Γ∪ {q} ∪ (O ∩ I)); 5 if I ′ = ⊥ then return YES; 6 Γ := Γ∪ {∨ O \ I ′ };

Algorithm 4: IncompleteAnwerQuery(Γ, 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 ∨ 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 AnswerQuery(Γ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 IncompleteAnswerQuery(Γ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)} ∪

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 AnswerQuery(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 AnswerQuery(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 AnswerQuery(sst(G), {rx | x ∈ arg(G)}, x), while skeptical acceptance of x ∈ arg(G) in SST(G) can be tested by a call to AnswerQuery(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 ∨ O \ I ′ is added to the theory at line 9. The second solver, instead, processes the theory Γ∪{q}∪{∨ O \ I} and the set of assumption literals O∩I; clause ∨ O \ I is not removed after completing the model search, as the next call either adds ∨ O \ I ′′ for I ′′ ⊃ I (if I ′ ̸= ∅), or is preceded by the addition of ∨ 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 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.

8 RelatedWork

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 unitimplied 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 GNCSINdAM.