On Computing World Views of Epistemic Logic Programs

1 Introduction

Epistemic logic programs (ELP) were proposed [Gelfond, 1991; 1994] for introspective reasoning through the use of modal operators K ("known") and M ("may be true"). For example, consider the following rules that were told to security guards of an extremely secret office:

• If you know that an individual breaks the data transmission rule then put him in a maximal secure prison.
• If you suspect that an individual breaks the data transmission rule but does not know that he/she breaks the rule then take him into custody and interview him.

If we were to encode these rules as a logic program that would be used by a guard to determine whether or not an individual, given a set of observations, is a felon or a suspect, which will then allow the guard to act appropriately. Let felon, suspect, and break rule denote that an individual is a felon, is a suspect, and breaks the rule, respectively. Then, an encoding of

Patrick Kahl and Anthony Leclerc

SPAWAR Atlantic

North Charleston, SC 29410, USA

these rules in ELP is as follows:

• felon ←K break rule (1)

where the K (resp. M) operator stands for know (resp. might know) respectively. The intuitive meaning of K is that if break rule is true in every belief set of the agent then K break rule is true and hence felon will be concluded. And, if break rule is true in some but not all belief sets of the agent then M break rule is true and hence suspect will be concluded. Observe that this reasoning process requires that the truth value of epistemic literals such as K break rule and M break rule is evaluated over all belief sets of the agent.

In the past two decades, several semantics for ELPs have been proposed [Gelfond, 1991; 1994; del Cerro et al., 2015; Kahl et al., 2015; Truszczy´nski, 2011; Shen and Eiter, 2016]. Roughly speaking, the semantics of an ELP program Π is defined by the notion of a world view which is a collection of answer sets of a logic programΠ′ without the literals containing the K and M operators (or subjective literals) obtained after a modal reduct of Π with respect to a set of literals (precise definition in the next section). As such, with the exception of the algorithm in [Kahl et al., 2015], other algorithms for computing world views follow a guess-and-check style algorithm and employ two steps: (i) guess the values of a set of literals for the modal reduct; (ii) compute the modal reduct, its answer sets using some answer set solver, and verify that the values of guessed literals with respect to the collection of answer sets of the modal reduct match the guessed values. The difference between these algorithms lies in which type of literals are selected for guessing and how their values are guessed. For instance, the algorithm developed in [Zhang and Zhao, 2014] starts with guessing the values of objective literals occurring in the subjective literals of the programs; the algorithm proposed in [Zhang, 2006] starts with the subjective literals; etc. The algorithm developed in [Kahl et al., 2015] starts with transforming an ELP program into a logic program without guessing the values of the subjective literals. It then searches for world views among the collection of answer sets of this program.

It is worth noticing that thus far, with the exception of the recently developed system ELPsolve described in [Kahl et al., 2016] that can compute world views of programs with millions of possible assignments of the subjective literals, none of the previously developed systems reaches this level of scalability. Perhaps the earliest attempt to develop an ELP-solver is the system Wviews described in [Kelly, 2007]. This system implemented the algorithm proposed in [Zhang, 2006]. ESmodels (see, e.g., [Zhang and Zhao, 2014]) is another system for computing world views that implements a guess-and-check algorithm that starts with guessing of values of literals occurring in subjective literals. The system also utilized some properties of world views to enhance its performance. ELPS [Balai and Kahl, 2014] is yet another system for computing an improved semantics of ELPs, called ES2014, proposed in [Kahl et al., 2015]. The difference between ELPS and ELPsolve lies in that ELPS computes all answer sets of the program resulting from the transformation mentioned earlier while ELPsolve implements a systematic search over the set of truth value assignments of the set of subjective literals that occur within the scope of a negation-as-failure operator. In this way, ELPsolve avoids the memory problem that frequently plagued other systems. ELPsolve also exploits parallelism to improve its performance. We observe that all previous developed ELP-solvers usually employ answer set solvers as a black box.

Our goal in this paper is to contribute to the development of ELP-solvers by proposing new algorithms that facilitate a tighter integration of world view computation and answer set solvers. We demonstrate the usefulness of the algorithms by developing two novel ELP-solvers for computing world views and show experimentally that the new solvers perform better than the state-of-the-art solvers. We also evaluate the use of these solvers in conformant planning by comparing it against DLV-K, one of the most efficient logic programming based conformant planners.

2 Background

We assume that the readers are familiar with the basic notations of logic programs under answer set semantics (or ASP programs) (see, e.g., [Gelfond and Lifschitz, 1991]). For an ASP program P, AS(P) denotes the set of all answer sets of P. Answer sets of ASP programs can be computed using ASP solvers such as CLINGO [Gebser et al., 2014]. Recently, CLINGO adds a feature, called multi-shot, for dealing with continuously changing logic programs. It is done by augmenting an ASP encoding with Python procedures controlling ASP solving processes along with the corresponding evolving logic programs. It includes methods for adding/grounding rules, setting truth values of (external) atoms, computing the answer sets of a current program, etc.

We assume a propositional language L. An objective literal (or literal, for short) ℓ in L is either an atom a ∈ L or its negation ¬a. A subjective literal in L is of the form Kℓ, Mℓ, not Kℓ, or not Mℓ where ℓ is an objective literal. An ELP is a set of rules of the form

where k ≥ 0, m ≥ 0, n ≥ m, each ℓi is a literal, and each gi is either a literal, or a subjective literal. Observe that an ELP that does not contain any occurrence of a subjective literal is an ASP program. We say that a set of literals in L is consistent if it does not contain a and ¬a for some a ∈ L.

Definition 1 (Satisfaction of a Subjective Literal) Let W be a non-empty set of consistent sets of literals, and ϕ be a subjective literal. W satisfies ϕ, denoted by W |= ϕ if

• ϕ = Kℓ and ∀A ∈W : ℓ ∈ A.
• ϕ = not Kℓ and ∃A ∈W : ℓ /∈ A.
• ϕ =Mℓ and ∃A ∈W : ℓ ∈ A.
• ϕ = notMℓ and ∀A ∈W : ℓ /∈ A.

Definition 2 (Modal Reduct) Let Π be an ELP and W be a non-empty set of consistent sets of ground literals. ΠW , the modal reduct of Π with respect to W, is defined as the ASP program 1 obtained from Π by replacing/removing subjective literals and/or deleting associated rules in Π as follows:

• ϕ = Kℓ and W |= ϕ then replace Kℓ with ℓ; otherwise, delete the rule fromΠ;
• ϕ = not Kℓ and W |= ϕ then remove not Kℓ from the rule; otherwise, replace not Kℓ with not ℓ;
• ϕ = Mℓ and W |= ϕ then remove Mℓ from the rule; otherwise, replace Mℓ with not not ℓ;
• ϕ = notMℓ and W |= ϕ then replace notMℓ with not ℓ; otherwise, delete the rule from Π.

Definition 3 (World View) Let Π be a ground ELP and W be a non-empty set of consistent sets of literals. W is a world view of Π if W = AS(ΠW ).

An ELP program might have multiple world views. For example, the program

has two world views {{p}, {q}} and {{q, r}}.

Given an ELP Π, world views of Π can be computed using an algorithm in [Kahl et al., 2015]. For simplicity of the presentation, the algorithm is simplified to only deal with ground programs.

• Step 1: Convert Π to a program Π′ without K and M operators.

For each objective literal ℓ occurring in a subjective literal, let k ℓ, k0 ℓ, k1 ℓ, m ℓ, m0 ℓ, or m1 ℓ be fresh atoms 2 obtained from ℓ by prefixing it with k , k0 , k1 , m , m0 , or m1 (respectively). These atoms are referred to as k-/matoms. Two sets S1 and S2 of literals with literals from these fresh atoms are said to share the same k-/m-atoms, denoted by S1 ∼k/m S2 if x ℓ ∈ S1 iff x ℓ ∈ S2 for all x ∈ {k, k0, k1, m, m0, m1} and objective literal ℓ.

Let Π′ be the program that consists of rules without subjective literals in Π and for each rule r in Π that contains some subjective literals, replace the subjective literals in r to create a new rule r′ in Π′ as follows 3 .

• Kℓ is replaced with not ¬k ℓ, ℓ and the following rules will be added to Π′ :

1 with nested expressions of the form not not ℓ (see, [Lifschitz et al., 1999])

2 Atoms that do not occur in L.

3 Note that if a rule r contains more than one subjective literals then multiple replacements/deletions and multiple sets of rules are introduced in the creation of r′ .

• not Kℓ is replaced with ¬k ℓ and the rules (3)-(6) are added to Π′ .
• Mℓ is replaced with m ℓ and the following rules will be added to Π′ :

• notMℓ is replaced with notm ℓ and the rules (7)-(9) and the next rule will be added to Π′ :

• Step 2: Group the answer sets of Π′ by common k-/matoms of the form k0 ℓ, k1 ℓ, m0 ℓ, and m1 ℓ, i.e., for each group of answer sets W, it holds that ∀ S1, S2 ∈ W.[S1 ∼k/m S2]. Each group W of answer sets is said to represent (i.e., if its k-/m-literals are removed) a candidate world view of Π.
• Step 3: For each W representing a candidate world view of Π, check that the following conditions are met for all its k-/m-atoms:
• (a) if k1 ℓ is in the sets of W, then ℓ is in every set of W;
• (b) if k0 ℓ is in the sets of W, then ℓ is missing from at least one set of W;
• (c) if m1 ℓ is in the sets of W, then ℓ is in at least one set of W; and
• (d) if m0 ℓ is in the sets of W, then ℓ is missing from every set of W.

W\KM = {S\KM | S ∈ W} is a world view of Π if the conditions (a)-(d) above are met where S\KM is obtained from S by removing all fresh atoms from S.

In the following, we will denote with ASP (Π) the program obtained from Π after Step 1 of the above algorithm.

3 Algorithms for ComputingWorld Views

In this section, we describe three algorithms. One algorithm computes at most k world views of an ELP. The second/third one computes a world view that satisfies a certain objective literal without/with using heuristics, respectively. We begin with a discussion of the theoretical foundation underlying these algorithms which depends on several properties of ASP (Π). Before we present these properties, let us recall two important entailment notions in ASP. Given an ASP program P and a literal ℓ in the language of P, ℓ is said to be skeptically (resp. credulously) entailed by P, denoted by P |=S ℓ (resp. P |=C ℓ), if ℓ ∈ S for every S ∈ AS(P) (resp. for some S ∈ AS(P)).

Because a world view of an epistemic program Π is a nonempty subset of AS(ASP(Π)), the next property is trivial.

Proposition 1 Let Π be an epistemic program. If ASP(Π) has no answer set then Π has no world view.

The next property makes use of the properties of the skeptical and credulous entailment relation in ASP programs.

Proposition 2 Let Π be an epistemic program. Then,

• For an objective literal ℓ such that ASP(Π) skeptically entails ℓ then Kℓ must be true in all world views of Π.
• For an objective literal ℓ such that ASP (Π) does not credulously entail ℓ then notMℓ must be true in all world views of Π.

The above two propositions are useful in preprocessing Π since ASP solver provides options for computing skeptically and credulously entailment consequences of an ASP program (e.g., cautious and brave options of CLINGO). For example, if ℓ is skeptically entailed by ASP(Π)(Π) then k1 ℓ must be in every world view of Π. In order to present other properties, we need some extra notations. Let X be a set of literals in the language of ASP(Π). We define

To continue, we introduce some new rules involving the atoms of the form k1 ℓ, k0 ℓ, m1 ℓ, or m0 ℓ as follows. In the following, nok is a fresh atom as well as okα, for each k-/m- atom α, is a fresh atom in the language of ASP(Π).

The next observation will be important in the proofs of the useful properties of ASP(Π). Let km(Π) be the set of all expressions of the form Kℓ or Mℓ occurring in Π.

Observation 1 Let Π be an epistemic logic program and S be an answer set of ASP(Π). Then, for every Kℓ (resp. Mℓ) that appears in Π, S contains exactly one element of {k1 ℓ, k0 ℓ} (resp. {m1 ℓ,m0 ℓ}).

The correctness of this observation rests on the rules (3)-(4) and (7)-(8) in ASP(Π) which are responsible for generating the fresh atoms in answer sets of ASP(Π). Furthermore, a consequence of this observation and the definition of world views of Π constructed from ASP(Π), if a world view W containing an answer set S of ASP(Π) exists then every answer set S′ ∈ W must satisfy that k1 m0(S) = k1 m0(S′ ) and k0 m1(S) = k0 m1(S′ ). The next proposition relates world views of Π and answer sets of ASP(Π) through the atoms in km(Π).

Proposition 3 Let Π be an epistemic program and S be an answer set of ASP(Π). Let ∆ = ⋃α∈k1 m0(S) {rα, cα} ∪ ⋃α∈k0 m1(S) {rα}∪{← not nok}. Let Π′ = ASP(Π)∪∆. Then, if Π′ has some answer set then Π does not have a world view containing S\KM.

The above proposition allows for the development of a test that checks whether or not Π has a world view containing an answer set S of ASP(Π). This is encoded in Algorithm 1. Specifically, given S, the set ∆, defined in Proposition 3, is computed (Line 4) and an answer set of ASP (Π)∪∆ is computed (Line 5). The rules in ∆ stipulate that answer sets of ASP(Π) ∪ ∆ belong to the same group W of answer sets

Algorithm 1 TESTK1M0(ASP (Π), S)

% Can Π have a world view containing S?

• 1: Input: ASP(Π): ASP program of Π, S∈AS(ASP(Π))
• 2: Output: Π has world viewW, S∈W: true; else false
• 3: Compute k1 m0(S) and k0 m1(S)
• 4: ∆= ⋃α∈k1 m0(S) {rα, cα}∪ ⋃α∈k0 m1(S) {rα}∪{←not nok}.
• 5: if ASP(Π) ∪∆ has an answer set then return false
• 6: else return true

containing S (Step 2, Section 2) and contain nok. The presence of nok indicates that there exists some k-/m-atom α in S such that the check for condition (a) and (c) in Step 3 (Section 2) is not satisfied (e.g., k1 ℓ is in the sets of W but ℓ is not).

The next proposition is similar to Proposition 3. It provides a check for conditions (b) and (d) in verifying whether a candidate world view is indeed a world view.

Proposition 4 Let Π be an epistemic program and S be an answer set of ASP(Π). Let ∆ = ⋃α∈k1 m0(S) {rα} ∪ ⋃α∈k0 m1(S) {rα, cα}. Let Π′ = ASP(Π) ∪ ∆. Then, if Π′ does not credulously entail okα for some α ∈ k0 m1(S) then Π does not have a world view containing S\KM.

Algorithm 2 encodes Proposition 4. Similar to Algorithm 1, given S, the set ∆, defined in Proposition 4, is computed (Line 4). Line 5 of the algorithm aims at enforcing conditions (b) and (d) (Step 3, Section 2) for the collection of answer sets of ASP (Π) ∪ ∆.

Algorithm 2 TESTK0M1(ASP (Π), S)

% Can Π have a world view containing S?

• 1: Input: ASP(Π): ASP program of Π, S∈AS(ASP(Π))
• 2: Output: Π has world viewW, S∈W: true; else false
• 3: Compute k1 m0(S) and k0 m1(S)
• 4: ∆ = ⋃α∈k1 m0(S) {rα} ∪ ⋃α∈k0 m1(S) {rα, cα}.
• 5: if ASP(Π) ∪∆ ̸|=C okα for some α ∈ k0 m1(S) then return false
• 6: else return true

Utilizing Propositions 2-4, we can prove the following property of views of ELPs (proof omitted for space reason):

Proposition 5 Let Π be an epistemic program, S be an answer set of ASP(Π), and ∆ = {rα | α ∈ k1 m0(S) ∪ k0 m1(S)}. If TESTK1M0(ASP(Π), S) returns true and TESTK0M1(ASP (Π), S) returns true then W\KM is a world view of Π where W = {S | S ∈ AS(ASP (Π) ∪ ∆)}.

3.1 Computing k World Views

In this subsection, we describe an algorithm for computing at most k world views of an epistemic logic program. We need also the following notations. For a program Π and S ∈ AS(ASP(Π)), by C(S) we denote the constraint

where {α1, . . . , αt} = k1 m0(S) ∪ k0 m1(S). Also,

Algorithm 3 EP-ASP(Π, k): Compute k world views of Π

• 1: Input: an ELP programΠ, k: the number of world views
• 15: return Ω

2: Output: At most k world views of Π 3: Compute ASP(Π) fromΠ 4: Let ASP(Π) = ASP(Π) ∪SΠ ∪CΠ 5: Ω = ∅; Γ = ASP(Π); n = 0 6: while n < k and Γ is consistent do 7: Let S be an answer set of Γ 8: ∆= {rα | α ∈ k1 m0(S) ∪ k0 m1(S)} 9: if TESTK1M0(ASP(Π), S) = true then 10: if TESTK0M1(ASP(Π), S) = true then 11: W = AS(ASP(Π) ∪∆) 12: Ω = Ω ∪ W\KM; n = n + 1 13: Γ = Γ∪C(S) 14: end while

Algorithm 3 computes at most k world views of program Π.

The correctness of Algorithm 3 follows from Proposition 5. We note that the addition of the constraint C(S) to Γ (Line 13) is to eliminate any answer set Y of ASP(Π) with the property k1 m0(S) = k1 m0(Y ) and k0 m1(S) = k0 m1(Y ) from consideration for computing a world view (Line 7) after S has been considered, i.e., this prevents S from being selected repeatedly and thus guarantees that Alg. 3 terminates and computes at most k world views of Π.

3.2 Goal Directed Computing

We now propose a modification of Algorithm 3 that enables the computation of world views satisfying a given objective literal. In other words, given an ELP Π and an objective literal ℓ in the language of Π, we would like to compute one (or at most k) world view(s) W such that W |= Kℓ. This is interesting and has a wide range of applications. For instance, it has been shown that epistemic logic programs can be used for conformant planning (e.g., [Kahl et al., 2015]). It is customary that a conformant planning problem P is translated into an epistemic logic program E(P) with an atom goal for encoding the goal condition such that each world view W of E(P) with W |= Kgoal contains a solution to the problem P. As such, to compute solutions of P, it is sufficient to compute world views satisfying W |= Kgoal. As it turns out, only a slight modification of Algorithm 3 will be sufficient: replacing Line 7 of Algorithm 3 with

Line 7G: Let S be an answer set of Γ∪{← not k1 ℓ}. The purpose of the change is to focus on answer set satisfying k1 ℓ of Γ which are also answer sets of ASP(Π). The new condition requires that k1 ℓ is true in the answer set S which, by the condition (a) in Step 2 of second section, forces ℓ to be in every set of the world view containing S.

3.3 Adding Heuristics

A further enhancement of the solver can be done by providing it with a way to select a promising answer set that results in the successful identification of a world view. In general, this can be expressed by replacing Line 7 of Algorithm 3 with

Line 7H: Let S be an answer set of Γ ∪ {← not ℓ | ℓ ∈ H}

where H is a set of literals which could be viewed as a means to represent a heuristic to the solver. Although it might be difficult to identify such heuristics in general, it can be defined for conformant planning. Specifically, we implemented a heuristic for conformant planning that is based on the approach in [Kurien et al., 2002; Nguyen et al., 2012]. Given a conformant planning problem P, the system computes solutions of planning problems whose initial states are completions of the initial state of P , extracts action occurrences from these solutions to create H, and uses this as a heuristic to guide the search.

3.4 Implementing a Different Semantics

The semantics of ELPs used in this paper (Section 2) is defined in [Kahl et al., 2015]. It is shown in [Kahl et al., 2016] that with only a slight modification, this semantics is equivalent to the newest semantics defined in [Shen and Eiter, 2016]. Indeed, the newest semantics can be computed by replacing Line 7 of Algorithm 3 with

Line 7M: Let S be an answer set of Γ such that Γ ∪MC(S) does not have an answer set.

where MC(S) is a set of rules aimed at selecting answer set S′ of ASP(Π) such that k0 m1(S) ⊂ k0 m1(S′ ). More precisely, MC(S) contains (i) rα and in(α) ← for α ∈ k0 m1(S); (ii) okm ← β, not in(β) for β of the form k0 ℓ or m1 ℓ and β ̸∈ k0 m1(S); and (iii) ← not okm. In the following, we refer to answer sets satisfying the Line 7M as those satisfying the SE-maximality condition.

4 Implementation and Evaluation

We implement the algorithms described in Section 3 in a prototype called EP-ASP and evaluate (i) the capabilities of EPASP in computing world views of an ELP against ELPsolve using the benchmarks provided in [Kahl et al., 2016]; and (ii) the effectiveness of directed reasoning of EP-ASP, e.g., in computing world views satisfying a given goal by comparing against DLV-K [Eiter et al., 2003], a logic program based system for conformant planning, using the well-known "bomb in the toilet" problem [Reichgelt, 1987] and its variations. We also implemented a version of EP-ASP that computes the semantics of ELPs given in [Shen and Eiter, 2016] and denote it with EP-ASPse .

4.1 EP-ASP and EP-ASPse

The implementation of EP-ASP and EP-ASPse is in Python. It uses the library provided in the distribution of CLINGO to modify the ASP program and the mode of computation (e.g., cautious or brave reasoning). Its code is omitted for space reason and is downloadable from https://github.com/ tiep/EP-ASP. EP-ASPse differs from EP-ASP in the implementation of Line 7 (Subsection 3.4). In the following, we write "EP-ASP(se )" and mean "EP-ASP or EP-ASPse ."

4.2 ELPsolve

ELPsolve [Kahl et al., 2016] computes world views of an ELP using semantics given in [Shen and Eiter, 2016]. ELPsolve guesses a collection of atoms (⊆ maximal) of the forms not Kℓ or Mℓ, translates it into a collection of atoms of the form k1 ℓ, k0 ℓ, m1 ℓ, or m0 ℓ, adds them to ASP(Π), and verifies if the set of answer sets of the new program is a world view.

4.3 Experimental Results

All experiments are performed on an Intel Core i7 2.8GHz machine with 16GB memory. Runtimes are reported in second; and '-' indicates that an algorithm fails to solve a problem after one hour. We use an implementation of ELPsolve provided by their authors and a publicly-available implementation of DLV-K. 4 Results are detailed in Table 1(a)-(b). All three systems use the program ELPS [Balai and Kahl, 2014] to convert an ELP Π to ASP (Π).

EP-ASP(se ) versus ELPsolve: The benchmarks in [Kahl et al., 2016] contain two problems, the Scholarship Eligibility Problems [Gelfond, 1991] (represented by E-XX) and Yale Shooting Problems [Hanks and McDermott, 1987] (represented by Y-XX). "XX" indicates the number of distinct ground subjective literals in the problem. The ELP encodings of these problems come with the ELPsolve's system.

In E-XX problems, in/eligibility for scholarship of students needs to be determined; and, if it cannot be determined then an interview needs to be scheduled. The difficulty in computing world views for E-XX depends on how many students need to be interviewed. The Y-XX problems are variations of the Yale shooting problem with additional actions and incomplete initial state. Note that in both sets of problems, the semantics in Section 2 is identical to the semantics computed by ELPsolve, i.e., all systems compute the same world view.

Table 1(a) details the runtimes of ELPsolve and EPASP(se ) for computing one world view of E/Y-XX problems. We note that for Y-XX problems, the planning option is turned on for EP-ASP(se ). The number between the brackets in the EP-ASP(se ) column indicates the number of iterations or the number of calls to CLINGO (Lines 7-14, Algorithm 3) that EP-ASP(se ) needs to do to find the first world view. This number for EP-ASPse , however, does not include the number of calls to CLINGO before an answer set satisfying the SE-maximality condition described in Subsection 3.4, i.e., checking for maximality of the set of not Kℓ and Mℓ of the answer set.

We observe that both versions of EP-ASP (i) can solve more problems in E-XX problems and (ii) consistently faster than ELPsolve. In most problems, they are an order of magnitude faster than ELPsolve. We believe their better performance lies in the efficient way of identifying candidate world views and its ability to utilize the pre-processor results to prune the search space.

The behavior of EP-ASPse shows that verifying the SEmaximality condition does affect the performance of the system but not significantly (see, E-18/20, E-26, and E-30/32 or Y-20). Its trend seems to be exactly as that of ELPsolve as both look for answer sets satisfying the SE-maximality condition before checking for the existence of a world view. On the other hand, EP-ASP behaves a bit different from ELPsolve Table 1: Experimental Results (E+: ELPsolve, S1: EP-ASP, S2: EP-ASPse ; ∗ : problem without world view)

4 DLV-K is obtained from www.dlvsystem.com/dlv/.

and EP-ASPse when XX increases. EP-ASP guesses an answer set and tries to verify for a world view while the other systems execute the verification only for answer set satisfies the SE-maximality condition. In this sense, EP-ASP uses a greedy algorithm whose performance relies on the heuristic of (CLINGO) in computing answer sets. On the other hand, ELPsolve (EP-ASPse ) systematically searches through all subsets of the set of atoms of the form not Kℓ or Mℓ (answer sets satisfying the SE-maximality condition).

EP-ASP versus DLV-K: We conduct this experiment to evaluate the performance of EP-ASP in computing a world view that satisfies a predefined goal. We compare EP-ASP with DLV-K since DLV-K is one of the most efficient logic programming based implementations for conformant planning. We did not run ELPsolve in this experiment since its current implementation has a limit of 34 subjective literals and this number is exceeded in all problems in this experiment.

The experiments are conducted using the "bomb in the toilet" (BT) problem [Reichgelt, 1987] and its variations, denoted BT(p), B1TC(p), B2TC(p), B3TC(p), and BTUC(p) where p indicates the number of packages in a problem. The key idea is that to be safe, one needs to dunk all the packets in one of the available toilets (BT). Furthermore, dunking a packet might or might not clog the toilet (C and UC), and one needs to flush the clogged toilet before one can dunk another packet into it. The ELP encoding of these problems are derived from the world-state encoding in [Eiter et al., 2003]. We did not use the knowledge-state encoding because it uses a different semantics that was not implemented in the generic conformant planning module of EP-ASP(se ).

The runtimes of the systems are detailed in Table 1(b). In this experiment, we use EP-ASP(se ) with the heuristic described in Subsection 3.3. Without the heuristic, EPASP(se ) performs significantly slower and does not scale up well. While DLV-K always finds optimal length solution, EPASP(se ) does not because of its heuristic. The length of the solution computed by EP-ASP(se ) is given between the parentheses in the column EP-ASP(se ).

We observe that EP-ASP(se ) is able to solve more problems (in B2TC(p), B3TC(p), and BTUC(p) domains) than DLV-K. It is faster than DLV-K when the problem becomes more complex (i.e., increasing p) while DLV-K is faster than EP-ASP(se ) for problems with small p. The reason is that, in these problems, the times for computing the heuristic dominates the times saved from using the heuristic.

5 Conclusions and FutureWork

We present an algorithm for computing world views of epistemic logic programs. The new algorithm exploits the relationship between world views and the subjective literals of the program Π to avoid the need of computing all answer sets of a modal reduct of Π for verifying whether or not a collection of answer sets of the equivalent ASP program ASP(Π) is indeed a world view of Π. We discuss different variations of the algorithm such as the use of heuristics, the computation of world views satisfying a given properties, and the computation of different semantics.

We present two implementations of the algorithm, called EP-ASP and EP-ASPse , that take advantage of the multi-shot feature of the answer set solver CLINGO and provide a tight integration of the two processes: world view computation and answer set computation. EP-ASP implements the semantics of ELPs in [Kahl et al., 2015] and EP-ASPse computes the newest semantics of ELPs proposed in [Shen and Eiter, 2016]. Both systems perform exceptionally well comparing to state-of-the-art epistemic logic program solvers in benchmarks from the literature. We also experimentally evaluate the goal directed feature of these systems by comparing it against DLV-K. The experimental results show that they can be competitive with DLV-K in solving conformant planning problems given a good heuristic. It is worth noticing that even though conformant planning has been often mentioned as one of the ideal applications of ELPs, to the best of our knowledge, EP-ASP (or EP-ASPse ) with heuristic is the first implementation based on ELP that is competitive with DLV-K.

The experimental evaluation shows that epistemic logic program solver can be efficient and could reach the mature level needed to be useful in practical applications that require strong inspection. A particular situation that is of great interest to us is the following problem. Consider an agent who needs to guard a system. The guard knows possible actions that could affect the state of the system. The guard also know that if an enemy does not know the truth value of some proposition p then the system is safe. This type of problem could be represented by a conformant planning problem with the goal equivalent to not Kp. To the best of our knowledge, such problem has not been considered before in the planning community. None of the current conformant planners can solve this type of problem although all will solve the problem of finding plans achieving K p. This will be our focus in the near future.