Relevance for SAT(ID)

1 Introduction

Since the addition of conflict-driven clause learning [Marques-Silva and Sakallah, 1999], SAT solvers have made huge leaps forward. Now that these highly-performant SATsolvers exist, research often stretches beyond SAT by extending the language supported by SAT with richer language constructs. Research fields such as SAT Modulo Theories (SMT) [Barrett et al., 2009], Constraint Programming (CP) [Apt, 2003] in the form of lazy clause generation [Stuckey, 2010], or Answer Set Programming (ASP) [Marek and Truszczy´nski, 1999] could be seen as following this approach. In this paper, we focus on the logic PC(ID): the Propositional Calculus extended with Inductive Definitions [Mari¨en et al., 2007]. The satisfiability problem for PC(ID) encodings is called SAT(ID) [Mari¨en et al., 2008]. SAT(ID) can be formalised as SAT modulo a theory of inductive definitions and is closely related to answer set solving. In fact, all the work we introduce in this paper is also applicable to so-called generate-define-test answer set programs.

In this paper we introduce an alternative criterion to determine satisfiability of a PC(ID) theory. Instead of searching for a variable assignment that satisfies the PC(ID) theory, we search for a partial assignment that contains sufficient information to guarantee satisfiability. Our approach is based on the notion of justifications [Denecker and De Schreye, 1993;

Denecker et al., 2015]. As a small example, consider the following theory.

This theory contains one constraint, that pT must hold, and a definition (between '¶' and '♦') of pT in terms of variables a to i. One way to check satisfiability would be to generate an assignment of all variables that satisfies the above theory (this is the classical approach to solving such problems). What we do, on the other hand, is to search for a partial assignment to these variables such that pT is justified in that partial assignment. Consider for example the partial assignment where pT , a, b, c and d are true and everything else is unknown. In this assignment, a and b are justified because d and c hold respectively; pT is justified because both a and b are justified. This suffices to determine satisfiability of the theory, without considering the definition of e for instance.

We introduce the notion of relevance. Intuitively, a literal is relevant if it can contribute to justifying the theory. In the above example, as soon as d is assigned true, the variable e becomes irrelevant. From that point onwards, search should not take e's defining rule into account.

Based on this notion of relevance, we define two extensions of existing SAT(ID) solvers. The first is to modify the decision heuristics: we show that deciding on irrelevant literals never affects any possible justification for pT . Hence, we propose to only choose on relevant literals, otherwise leaving the heuristics unchanged. The second is to implement an early stopping criterion that allows a solver to decide the theory is satisfiable in a partial assignment.

The main contributions of this paper are (1) the formal identification of the set of relevant literals, (2) showing that assigning a value to an irrelevant literal does not affect satisfiability, (3) proving correctness of the new early stopping criterion, and (4) experimentally evaluating the proposed approach.

The rest of this paper is structured as follows. In Section 2 we present some necessary preliminaries. In Section 3, we present our new theory, essentially introducing relevance, the new algorithms and the associated correctness theorems. We experimentally evaluate our proposed approach in Section 4 and conclude in Section 5.

2 Preliminaries

PC(ID)

In this section, we briefly recall the syntax and semantics of Propositional Calculus extended with Inductive Definitions (PC(ID)) [Mari¨en, 2009].

A truth value is one of ¶t↪ f↪ u♦; t represents true, f false and u unknown. The truth order t on truth values is given by f t ut t, the precision order p is given by up f and u p t. Let ⌃ be a finite set of symbols called atoms. A literal l is an atom p or its negation ≻p. In the former case, we call l positive, in the latter, we call l negative. We use ⌃ to denote the set of all literals over ⌃. If l is a literal, we use ♣l♣ to denote the atom of l, i.e., to denote p if l = p or l = ≻p. We use ⇠l to denote the literal that is the negation of l, i.e., ⇠p = ≻p and ⇠≻p = p. A partial interpretation I is a mapping from ⌃ to truth values. We use the notation ¶pt1 ↪ ▷ ▷ ▷ ↪ ptn ↪ qf1 ↪ ▷ ▷ ▷ ↪ qfm♦ for the partial interpretation that maps the pi to t, the qi to f and all other atoms to u. We call a partial interpretation two-valued if it does not map any atom to u. If I and I 0 are partial interpretations, we say that I is less precise than I 0 (notation I p I 0 ) if for all p 2 ⌃, I(p)p I 0 (p). If ' is a propositional formula, we use 'I to denote the truth value (t, f or u) of ' in I, based on the Kleene truth tables [Kleene, 1938]. If I is a partial interpretation and l a literal, we use I[l : t] to denote the partial interpretation equal to I, except that it interprets l as t (and similar for f , u). With σ a set of symbols, we use the notation I♣σ to indicate the restriction of I to symbols in σ. I.e., I♣σ(p) = u if p ◁2 σ and I♣σ(p) = I(p) otherwise.

An inductive definition ∆ over ⌃ is a finite set of rules of the form p ' where p 2 ⌃ and ' is a propositional formula over ⌃. We call p the head of the rule and ' the body of the rule. We call p defined in ∆ if p occurs as the head of a rule in ∆. The set of all symbols defined in ∆ is denoted by defs(∆). All other symbols are called open in ∆. The set of open symbols in ∆ is denoted opens(∆). We say that a literal l is defined in ∆ if ♣l♣ 2 defs(∆). We use the parametrised well-founded semantics for inductive definitions [Denecker and Vennekens, 2007]. That is, interpretation I is a model of ∆ (denoted I ♣= ∆) if I is the well-founded model of ∆ in context I♣opens(∆). We call an inductive definition total if for every interpretation I of the open symbols, the well-founded model in context I is a two-valued interpretation.

A two-valued interpretation I is a subset of ⌃. We identify an interpretation I with the two-valued partial interpretation that maps p 2 I to t and p 2 ⌃ ∩ I to f .

A PC(ID) theory T over ⌃ is a set of propositional formulas, called constraints, and inductive definitions over ⌃. Interpretation I is a model of T if I is a model of all definitions and constraints in T . Without loss of generality [Mari¨en, 2009], we assume that every PC(ID) theory is in the DEFNF normalform, where T = ¶pT ↪ ∆♦ and

• ÷ ∆ is an inductive definition defining pT ,
• ÷ pT is an atom,
• ÷ every rule in ∆ is of the form p l1 ⊙ · · · ⊙ ln, where ⊙ is either ^ or _, p is an atom, and each of the li are literals,
• ÷ every atom p is defined in at most one rule of ∆.

It has been argued many times before [Denecker, 1998; Denecker and Ternovska, 2008; Denecker and Vennekens, 2014] that all sensible definitions in mathematical texts are total definitions. Following these arguments, in the rest of this paper we assume ∆ to be a total definition.

A rule in which ⊙ is ^, respectively _ is called a conjunctive, respectively disjunctive, rule. The rules in a definition ∆ impose a direct dependency relation, denoted dd∆, between literals, defined as follows. For literals from and to, it holds that (from↪ to) 2 dd∆ in∆ if there is a rule p l1⊙· · ·⊙ln in ∆ such that for some i, either from = p and to = li or from = ⇠p and to = ⇠li. The dependency graph of ∆ is the graph G∆ = (⌃↪ dd∆). For the remainder of the paper, we assume that some PC(ID) theory T = ¶pT ↪∆♦ is fixed; hence, we will often omit ∆ and/or T from the notations.

The satisfiability problem for PC(ID), i.e., deciding whether a PC(ID) theory has a model, is called SAT(ID). This problem is NP-complete [Mari¨en et al., 2008].

Justifications

Consider graph G = (V↪E), with V the set of nodes and E the set of edges. If the graph contains an edge from l to l0 (i.e., (l↪ l0 ) 2 E), we say that l is a parent of l0 in G and that l0 is a child of l in G. A node l is called a leaf of G if it has no children in G; otherwise it is called internal in G. Let G0 = (V 0 ↪ E0 ) be another graph. We define the union of two graphs (denoted G [ G0 ) as the graph with vertices V [ V 0 that contains only edges that were already in G or G0 .

Suppose l is a literal with p = ♣l♣ and p 2 defs(∆) with defining rule p l1 ⊙· · ·⊙ln. A set of literals Jd is a direct justification of l in ∆ if one of the following holds:

• ÷ l = p, ⊙ is ^, and Jd = ¶l1↪ ▷ ▷ ▷ ↪ ln♦,
• ÷ l = ≻p, ⊙ is ^, and Jd = ¶⇠li♦ for some i,
• ÷ l = p, ⊙ is _, and Jd = ¶li♦ for some i,
• ÷ l = ≻p, ⊙ is _, and Jd = ¶⇠l1↪ ▷ ▷ ▷ ↪⇠ln♦.

Note that a direct justification of a literal can only contain children of that literal in the dependency graph.

A justification [Denecker and De Schreye, 1993] J of a definition ∆ is a subgraph of G∆, such that each internal node l 2 J is a defined literal and the set of its children is a direct justification of l in ∆. We say that J contains l if l occurs as node in J. A justification is total if none of its leaves are defined literals. A justification can contain cycles.1 A cycle is called positive (resp. negative) if it contains only positive (resp. negative) literals. It is called a mixed cycle otherwise.

If J is a justification and I a (partial) interpretation, we define the value of J in I, denoted VI(J) as follows:

• ÷ VI(J) = f if J contains a leaf l with lI = f or a positive cycle (or both).
• ÷ VI(J) = u if VI(J) 6= f and J contains a leaf l with lI = u or a mixed cycle (or both).

1 In this text, we assume that ∆ is finite; in this case cycles are simply loops in the graph.The infinite case is a bit more subtle, and an adapted definition of cycle is required to maintain all results presented below.

• ÷ VI(J) = t otherwise (all leaves are t and cycles, if any, are negative).

A literal l is justified (in I, for T ) if there exists a total justification J (of ∆) that contains l such that VI(J) = t. In this case, we say that such a J justifies l (in I, for T ). We say that J minimally justifies l if J justifies l and there exists no subgraph J 0 of J that also justifies l.

Denecker and De Schreye [1993] showed that many semantics of logic programs can be captured by justifications. We recall their major result on the well-founded semantics.

Theorem 2.1 (Denecker and De Schreye [1993]). Let J be a justification of definition ∆.

• ÷ Suppose I and I 0 are partial interpretations. If I p I 0 then VI (J ) p VI 0 (J ).
• ÷ Suppose I is an opens(∆)-interpretation and I 0 is the well-founded model of ∆ in context I. For each defined literal l, it holds that

3 Relevance

Observations

The central observation in this paper is the fact that classical SAT(ID) solvers such as for example MINISAT(ID) [Mari¨en et al., 2008; De Cat et al., 2013] or the related ASP systems such as clasp [Gebser et al., 2012] or DLV [Leone et al., 2006] fail to exploit an important property. Recall that a PC(ID) theory T = ¶pT ↪∆♦ is assumed to be fixed throughout the text. Systems such as MINISAT(ID) search for an interpretation I such that I ♣= T , while in fact they could search for a partial interpretation I and a justification J that justifies pT in I. Our claim is that even though in theory both tasks are of the same complexity, for practical applications, the latter task possesses some important advantages. Before discussing these, we provide the formal basis for our theory.

Theorem 3.1. T is satisfiable if and only if there exists a partial interpretation I and a J that justifies pT in I.

Proof. First assume that T is satisfiable. Then there exists an interpretation I such that pT I = t and I ♣= ∆. Theorem 2.1 (2) then yields that t = maxt ¶VI(J) ♣ J is a total justification that justifies pT ♦. Hence, there must exist a justification J that contains pT for which VI(J) = t, i.e. J justifies pT in I. The result then follows by taking I = I and using J as justification.

On the other hand assume that there exists a partial interpretation I and a justification J such that J justifies pT in I. Now, let I 0 be any partial interpretation such that I 0 ≥p I and I 0 is two-valued in opens(∆). FromTheorem2.1 (1) follows that VI 0 (J)≥p VI(J), since I 0 ≥p I. Because J justifies pT , we also know VI(J) = t, which implies VI 0(J) = t. Further, VI 0 ♣opens(∆) (J) = VI 0(J) since the value of a justification only depends on the edge relations in J (unchanged) and the values of open atoms (also unchanged). Let I 0 denote the well-founded model of ∆ in context I 0 ♣opens(∆). I 0 exists because we assume ∆ to be a total definition. From Theorem 2.1 (2) we know that pT I 0 = t, because justification J already maps to the maximal value in the t order, thus the value of the set expression in the theorem is fixed. Hence T is indeed satisfiable: I 0 is a model of T .

We will now identify which literals are relevant.

Definition 3.2 (Relevant). Given a PC(ID) theory T = ¶pT ↪∆♦ and a partial interpretation I, we define the set of relevant literals, denoted RT (I), as follows

• ÷ if l 2 RT (I), (l↪ l0 ) 2 dd∆ and l0 is not justified, then l0 is relevant.
• ÷ pT is relevant if pT is not justified,

Intuitively, a literal is relevant if making it true can help justify pT . If a partial structure is made more precise, literals may become irrelevant because they can no longer contribute to any justification that justifies pT . Often, we assume T is clear from the context and simply state that l is relevant in I. We define the set of relevant literals and not the set of relevant atoms because, in a further stadium, one can exploit the information that e.g., a literal l is relevant, but ⇠l is not.

Using relevance, we aim to obtain three advantages over classical SAT(ID) solvers.

1. We can avoid irrelevant parts of the search space.
2. We can stop searching once a partial interpretation is found in which pT is justified, instead of searching for a total interpretation.
3. We can make solvers more robust for wrong choices. We illustrate each of these three advantages in the following example.

Example 3.3. Let T = ¶pT ↪∆♦ denote the theory where

Let I1 be the partial interpretation ¶pT t ↪ at ↪ bt ↪ dt ↪ ct ↪ gf ♦. In this case, d is justified in I1, hence so is a. This means that the value of e and f cannot influence whether or not a is justified. Hence, giving a value to e or to f cannot help justifying pT , illustrating advantage (1).

Let I2 be I1[j : t]. In this case pT is justified in I2, hence Theorem 3.1 yields that T is satisfiable and we do not need to search an assignment for the remaining (irrelevant) atoms, illustrating advantage (2).

Let I3 be I2[e : f]. It can be seen that there exists no model of T that is more precise than I3. Indeed, e is true in every model of T because i as well as ≻i make e true. It is possible that the solver make the choice ef early on. Theorem 3.1 shows that since pT is justified in I3 a model must exist (even though the current interpretation is incompatible with that model), illustrating advantage (3).

Example 3.4 (Example 3.3 continued). The set of relevant literals for I1 is RT (I1) = ¶pT ↪ b↪ ≻h↪ j↪ i♦. pT is relevant in I1 because it is not justified. b is relevant in I1 since it is not justified and since pT , which is not justified, depends on it. ≻h and j are relevant in I1 since they are not justified and potentially useful to justify b. i is relevant in I1 since it is not justified and might be used to justify ≻h. pT is justified in I2 and I3, which means there are no relevant literals in these partial interpretations.

Using these observations, we show how to exploit relevance to reduce the search space.

Exploiting Relevance

In order to exploit relevance, we assume that some search algorithm for SAT(ID) is given; we assume this algorithm searches for an interpretation I such that I ♣= T . We implemented our techniques in a conflict-driven clause learning DPLL solver. However, it deserves to be stressed that all ideas developed here are independent of the choice of search strategy or heuristic. We propose the following modification to such a solver: choose only on relevant literals and stop search early if there are no unassigned relevant literals in the current search state. Note that if there are no unassigned relevant literals left, pT is justified if and only if there is a model (according to Theorem 3.1). In order to prove correctness of our modification, we will use the following result.

Theorem 3.5. Let T = ¶pT ↪∆♦ be a PC(ID) theory. Suppose I is a partial interpretation and lirr a literal such that I(♣lirr ♣) = u and lirr is not relevant in I. If pT is justified in some partial interpretation I 0 more precise than I, then pT is also justified in I 0 [lirr : f] and in I 0 [lirr : t].

Proof. Let J be a justification that minimally justifies pT in I 0 . Note that leaves in J are open and true in I 0 ; cycles, if any, are negative.

J1 is derived from J as follows: for each defined literal x in J that is justified in I: remove the edges from x to its children. Finally, remove all parts not reachable from pT . By construction, the leafs of J 0 are either open literals, or defined literals justified in I.

Let J2 be a justification that contains only literals justified in I and that justifies all these literals. Now, define J 0 as J1 [ J2. Since J1's internal nodes are not justified in I, and all literals in J2 are justified in I, this union introduces no new loops not already in J1 or in J2. Additionally, J 0 only contains open literals already in J1 or in J2. This means J 0 is a justification that justifies pT in I 0 , since J 0 contains pT , leaves in J 0 are open and true in I 0 ; cycles, if any, are negative.

J 0 cannot contain lirr in the part that originated from J1, because those are all literals that were relevant in I. Any occurence of lirr in any part that originated from J2 has to be an internal node, since VI(J2) = t, which demands that all leafs are true. Hence, any occurrence of lirr cannot be a leaf in J 0 , which means that changing its interpretation does not affect the value of J 0 in I 0 . Therefore, pT is also justified in I 0 [lirr : f] and I 0 [lirr : t].

Theorem 3.5 shows that any search algorithm that can arrive in a state in which pT is justified by deciding on a literal l that is irrelevant in its current partial interpretation, can also arrive in such a state without deciding on l. Hence, if a literal l is irrelevant, it is useless to choose on that literal if the goal is to justify pT . This is exactly what our proposed solver modification does; we restrict the choices of a search algorithm to the set of relevant literals.

4 Experimental evaluation

In order to empirically evaluate our proposed approach, we adjusted the IDP3 system [De Cat et al., 2016] and its underlying solver MINISAT(ID) [De Cat et al., 2013] to take relevance into account. Integrating relevance into the search process is simple: it is a non-intrusive modification to the search heuristic to not choose on certain literals. However, calculating which literals are relevant requires a tight integration with the solver being adapted. Detailed information about the solver state, such as the dependency graph and the justification status for literals, are required in order to calculate which literals are relevant. For the purpose of this paper, we opted for a simple and non-intrusive implementation that had the drawback of significant overhead. Therefore, our experiments are based on search space metrics rather than absolute solving time. This performance overhead is not inherent to maintaining relevance. Large parts of the bookkeeping we do now is discovering information that is already present somewhere in the solver internally. However, extracting all the necessary information is an engineering task we did not complete yet. In this section, we will answer the following questions to evaluate whether it is worth investigating relevance further:

(Q1) How often does the VSIDS, the current state-of-the-art heuristic for SAT, make irrelevant decisions?

(Q2) Can we improve the performance of SAT(ID) solvers using relevance?

The complete set of experiments and information on how to run them can be found at https://dtai.cs.kuleuven.be/static/krr/ files/experiments/idp relevance experiments.tar.gz .

For these experiments we selected problems from previous ASP competitions that could be encoded without the use of aggregates and functions, since we do not yet support these language constructs. We ran these problems on an Intel(R) Xeon(R) CPU E5645 @ 2.40GHz CPU, using a time limit of 7200 seconds and a memory limit of 8GiB.

To answer (Q1) we ran all the above problems and their instances with a solver configuration that uses the VSIDS heuristic while keeping track of relevance. We keep track of whether the decision made by VSIDS is relevant without actually preventing decisions on irrelevant literals (i.e., the search behaviour is not affected). Table 1 shows the problems and their number of successfully solved versus total number of instances (second column). In this table we show the mean (θ) and variance (σ2 ) of (1) irrd : the ratio between the irrelevant decisions made by VSIDS and the total number of decisions, and (2) irrc : the ratio between the number of irrelevant decisions involved in conflicts and total number of decisions involved in conflicts. In order to obtain the latter statistic, we analyse the conflicts that occur during solving by applying full resolution on them. The resulting clause only contains decision literals. We then count the total number of decisions as well as the number of decision literals that were irrelevant at the time they were made.

Due to our significant performance overhead in keeping track of relevance, we were not able to solve a single instance of the Graceful Graphs and the Ricochet Robots problems. We observe that, on average, the VSIDS heuristics chooses a considerate amount of irrelevant literals. There is even an outlier in the Stable Marriage problem where more than 96% of the choices were irrelevant. Therefore we can say for (Q1) that, on average, VSIDS selects a significant amount of irrelevant choice literals on the classical benchmarks.

On the other hand, irrc is generally significantly lower than irrd , meaning that the irrelevant decisions that are made by VSIDS hardly ever lead to conflicts. In order to further inspect the behaviour of relevance we discuss cactusplots for the behaviour of the experimental runs in Table 1 for instances that were solved both by VSIDS (labeled "NR", for "No Relevance") and by our proposed solver modification (labeled "R", for "Relevance").

Figure 1 shows that we succeeded in reducing the number of decisions made, and Figure 2 shows that this did not affect the number of conflicts for these benchmarks. This initial observation is not encouraging, since the number of conflicts is often taken as a measure for the size of the search space traversed. In what follows, we

1. argue that in certain applications, reducing the number of decisions is itself already a desirable property
2. investigate why we observe no reduction in the number of conflicts.

Reducing decisions: a contribution on its own Even if we did not manage to significantly reduce the number of conflicts, reducing the number of decisions is already a significant achievement for certain applications. To illustrate this, we consider lazy model expansion [De Cat et al., 2015]. The approach of lazy model expansion is to interleave the grounding and the search space. That is, a first-order theory is not translated to propositional logic a priori. Instead, depending on the search of a SAT(ID) solver, certain parts of the grounding are generated. This approach works (roughly) as follows. A PC(ID) theory T is initialised as pT . Each time a literal that has no definition in T is assigned a value, some external procedure is called and the definition of that literal is added to T . This approach is particularly fruitful in applications with very large (possibly infinite) domains where it is simply infeasible to generate the entire grounding.

Adding more definitions to T is possibly a costly operation and should be avoided as much as possible. If we combine lazy grounding with our proposed relevance approach we will greatly benefit from the reduced number of decisions made, because avoiding non relevant decisions results in fewer variables that are assigned a value (also propagations that follow from irrelevant decisions!) and hence less grounding.

Analysing the conflict behaviour We noticed that, while VSIDS makes lots of choices on irrelevant literals, the number of conflicts did not increase significantly. One possible explanation for this behaviour is that in the examples we used, the irrelevant parts of the search space are not strongly constrained. One real-world example of a problem where irrelevant parts of the search space are still heavily constrained is a scheduling problem for a trucking company, such that each scheduled truck can solve a packing problem. Solutions to such problems are often hand-made in such a way that they take relevance into account (i.e., first solving the scheduling and then only trying to solve the relevant packing problems), because the current generation of solvers cannot handle this problem directly. An instance of such a problem and its solution is given by Verstichel [2013]. In order to test the hypothesis that underconstrained problems are indeed at the root of this behaviour, we construct a small encoding in which we force irrelevant literals to represent that a combinatorially hard probem is satisfiable:

Figure 3: Hand-made encoding showing the use of relevance. For ease of reading, a first-order version of the encoding is presented.

Figure 3 encodes the following problem. Predicates P and Q can be chosen freely (they are opens of the underlying definition). For each domain element d, XOR(d) holds if and only if exactly one of P (d) and Q(d) holds. Next, if XOR(d) is f , an encoding of an unsatisfiable pigeonhole must be satisfied. If XOR(d) is t, an encoding of a satisfiable pigeonhole problem must be satisfied. Thus, the problem can only be solved by making XOR(d) t for all instances. At any point during search, VSIDS can make choices on the variables occurring in the encoding of the pigeonhole problems. As soon as XOR is decided, the relevance heuristic, on the other hand, only makes choices on variables in the relevant subproblem. If unlucky, VSIDS behaviour can lead to a great deal of time wasted and a great number of unnecessary conflicts during search.

In order to test the behaviour of VSIDS on this problem we used the same setup as in Table 1. This time we also measured the solving time and memory needed, as well as the total number of decisions and conflicts. We ran the above encoding with the domain of size n = 250 and k = 9. The results, presented Table 2, show that there are problems where taking relevance leads to a greatly reduced number of conflicts, which means a reduction of the search space. Increasing the domain size only widened the gap between VSIDS and relevance. Runtime statistics of such additional experiments are omitted here, for brevity concerns. These observations lead to a definite positive answer to (Q2).

5 Conclusion

In this paper we formally identified a set of literals called relevant; we showed that irrelevant literals cannot influence the justification status of a PC(ID) theory and hence that making choices on irrelevant literals is useless with regards to proving the satisfiability of the given PC(ID) theory. We proposed two simple solver modifications: choosing only on relevant literals and stopping early. In this paper we provided a preliminary experimental evaluation using a simple and non-intrusive implementation of these proposed modifications. We compared our algorithms with the VSIDS heuristics, the current state-of-the-art heuristic for SAT-solvers.

Our conclusions are that, in the benchmarks that we ran, VSIDS was observed to choose on a significant amount of irrelevant literals; as such, our proposed solver modification to VSIDS successfully managed to decrease the number of decisions made. However, we were not able to significantly reduce the number of conflicts, which would mean a reduction in the search space. Our hypothesis as to why the number of conflicts did not decrease with the number of decisions was confirmed using a crafted example. Furthermore, we sketched situations in which the decrease in the number of decisions alone is significant enough to improve performance compared to the current state-of-the-art.

Our notion of irrelevance is closely related to "don't care atoms" in satisfiability solving [Fu et al., 2005]. However, there is an important difference between don't cares and irrelevant literals. To complete a partial structure with don't cares, any value may be assigned to a don't care literal; to an irrelevant literal, on the other hand, we only know that some value can be found for it. The value for irrelevant literals can be found as follows: first, any value can be assigned to the irrelevant atoms that are open in ∆. Given these values to the opens, the (parametrised) well-founded model of ∆ can be computed in polynomial time. The value of any other irrelevant literal is its value in the well-founded model. This is exactly what happens in the proof of Theorem 3.1.

We believe that further research into relevance will be of great value and see several topics for future work. First of all, the current theory is limited to PC(ID); further language extensions such as aggregates and arithmetic are not yet supported. Second, our theory also applies to generate-definetest ASP programs; experimentally evaluating relevance in a native ASP solver can yield interesting results. Third, engineering a more efficient algorithm to keep track of relevant literals can shed light on the possible (time-wise) performance gains from using relevance. Fourth, experimentally evaluating relevance in the context of lazy grounding is needed to verify our hypothesis that relevance can mean great improvements there.

Acknowledgements

This research was supported by project GOA 13/010 of the Research Fund KU Leuven and projects G.0489.10, G.0357.12, and G.0922.13 of the Research Foundation - Flanders. Bart Bogaerts is supported by the Finnish Center of Excellence in Computational Inference Research (COIN) funded by the Academy of Finland (under grant #251170).