# on_the_computational_complexity_of_model_reconciliations__e188b418.pdf

On the Computational Complexity of Model Reconciliations

Sarath Sreedharan1 , Pascal Bercher2 and Subbarao Kambhampati1

1School of Computing & AI, ASU 2The Australian National University sarath.sreedharan@colostate.edu, pascal.bercher@anu.edu.au, rao@asu.edu

Model-reconciliation explanation is a popular framework for generating explanations for planning problems. While the framework has been extended to multiple settings since its introduction for classical planning problems, there is little agreement on the computational complexity of generating minimal model reconciliation explanations in the basic setting. In this paper, we address this lacuna by introducing a decision-version of the model-reconciliation explanation generation problem and we show that it is ΣP 2 -complete.

1 Introduction The problem of generating intuitive and concise explanations for plans generated by AI agents has been receiving a lot of attention in recent years [Hoffmann and Magazzeni, 2019; Fox et al., 2017; Chakraborti et al., 2020]. Model reconciliation [Sreedharan et al., 2021] is an explanation generation framework popular in planning that frames explanation as a process of bringing human s expectation about the robot closer to the robot s behavior by updating their beliefs about the robot model, i.e., the human s theory of mind about the robot. While the original work does present a clear definition of the central explanatory challenge, namely, identifying a set of model updates of minimal length, we are unaware of any works that successfully establish the computational complexity of this problem. This is particularly unfortunate since solution strategies for model-reconciliation explanation tend to rely on extremely general, but computationally expensive model-space search. An exact characterization of the complexity of the problem could help us determine whether such methods are truly warranted in the case of model-reconciliation explanation. In this paper, we focus on the basic problem studied by Chakraborti et al. [2017]. We formalize a decision-version of the minimal explanation problem studied there and show that this decision problem is in fact Σp 2-complete. The proof will focus on mapping the explanation problem to that of establishing the satisfiability of a particular subclass of quantified boolean formulas. Specifically, one where the quantification is restricted to a set of existentially quantified variables followed by a set of universally quantified variables. The re-

duction for the membership proof will leverage the universal quantification in the formula to capture the optimality test that is a central part of the explanation generation problem and the existentially quantified variables to capture the explanation. While in the case of the hardness proof, we will use the optimality test to capture the universal quantification and the explanation to capture the existential one.

2 Background We start by providing basic definitions for planning problems and model-reconciliation and will end the section by providing a brief introduction to some of the relevant complexity classes we will be considering in this paper.

2.1 Classical Planning We will focus on deterministic, goal-directed planning problems represented in the STRIPS planning problem formalism [Geffner and Bonet, 2013]. Specifically a STRIPS planning problem (henceforth referred to as planning model) may be formally represented by a tuple M = F M, AM, δM, IM, GM , where F M is a set of proposition fluents that define the state space associated with the planning problem (i.e., SM = 2F M); AM is a set of action names; δM = pre M + , pre M , add M, del M provides the functions that map a given action name to its positive precondition, negative precondition, add effects and delete effects, such that

pre M + : A 2F M add M : A 2F M

pre M : A 2F M del M : A 2F M

Note that when we refer to an action we usually mean its name a AM, not its precondition and effect tuple (pre M + (a), pre M (a), add M(a), del M(a)). IM SM is the initial state from which the agent is trying to achieve the goal; and GM F M is the goal specification, where SM G = {s SM | s GM} is the set of goal states. An action a AM is called executable in a state s SM when its preconditions are satisfied by the current state, formally represented by exe(a, s, M) = pre M + (a) s and s pre M (a) = . The effect of executing an action is represented by the function γ(a, s, M) defined as:

= (s \ del M(a)) add M(a), if exe(a, s, M) = true undefined otherwise

Proceedings of the Thirty-First International Joint Conference on Artiﬁcial Intelligence (IJCAI-22)

Executability of sequences of actions is defined by subsequent action application. The functions exe and γ take a model M as an additional parameter. The reason for this is that we will make changes to specific actions and thus require to consider action executability and its state transition function in different models. A (possibly empty) sequence of actions π = a1, ..., ak is called a solution (also: plan) if it is executable in the initial state and results into a goal state, i.e., γ(π, IM, M) = γ(ak, γ(...(γ(a1, IM, M))...) GM. Additionally, each action and by extension the plan can be associated with a cost. In this paper, we will specifically focus on models where each action has a unit cost. Thus the cost of the plan, denoted by C(π), is equal to the length of the plan. As usual for heuristics, we use a star to denote optimality. A plan π is said to be a optimal for a model M, if

π with γ(π , IM, M) GM, such that C(π ) < C(π ).

We will use the notation C M to capture the cost of an optimal plan for M, i.e., the length of any shortest solution for M.

2.2 Encoding Planning Problems as SAT A popular way of solving planning problems, particularly when there exists a planning horizon (say T), is to encode it as propositional satisfiability problems (SAT) [Kautz et al., 1996]. The most common encoding for the problem uses propositional variables to capture whether a fluent is true at each possible time step and whether an action was executed at a time step. If M is the planning model, then we would have T (|F M|+|AM|) variables. The encoding has three important classes for clauses (a) clauses that describe a component of a model, i.e, initial state, goal, or action definition, (b) explanatory frame axioms that enforce the requirement that any change in variable value should correspond to the execution of an action that could have caused the change and finally (c) clauses to enforce the fact that concurrent action execution is not possible. For example, let ai AM and p add M(a), then as part of class (a) of clauses you would have clause of the form at i pt+1, for all time steps t. Similarly, an example of an explanatory clause for p would be

pt pt+1 _ {at i|p add M(a)}

Effectively the clause asserts that p could only have been turned true if one of these actions was executed. Finally, we assert that the actions cannot be executed concurrently using the clause

aj A,aj =a at j)

2.3 Model Reconciliation Explanation The basic setting of model reconciliation explanation consists of an autonomous agent (henceforth referred to as the Robot R), using its model MR to come up with its plans. There is a human observer, who assumes the robot uses a model MR h (i.e., the robot model assumed by the human) and is trying to make sense of the robot s plan. If the model MR h is different from MR, the human may be confused by the robot s choice to follow some (robot s) plan πR, as it might appear

suboptimal or even invalid (i.e., not executable or not achieving all goals) according to the model MR h . Now the goal of the model reconciliation is to resolve this confusion by providing the human with information on how the human s assumed model differs from the actual (robot) model. Before we can formally define a model reconciliation explanation problem, we need to define a model parameterization function. We will follow a formalization slightly different from those used by Chakraborti et al. [2017] and Sreedharan et al. [2021] and define the formalization around a space of models that share the same fluent space and action names. Definition 1. Given a set of propositions F and a set of action names A, let M(F,A) be the space of models that can be defined over F and A, i.e., M M(F,A) there exist δ, I, and G, such that M = F, A, δ, I, G is a planning model. Now each model from a given model space can be uniquely identified by a so-called model parameterization function, based on the definition set up by Chakraborti et al. [2017]. Definition 2. The model parameterization function Γ : M(F,A) 2F(F,A) for a given space of models M(F,A), maps a model from M(F,A) to a subset of propositions F(F,A) (henceforth referred to as model parameters), where

F(F,A) = {init-has-f | f F} {goal-has-f | f F} [

a A {a-has-pos-prec-f, a-has-neg-prec-f, a-has-add-f, a-has-del-f | f F}.

For a model M = F M, AM, δM, IM, GM , the parameterization function Γ(M) is defined by

τ M I = {init-has-f | f IM}

τ M G = {goal-has-g | g GM}

τ M pre+(a) = {a-has-pos-prec-f | f pre M + (a)}

τ M pre (a) = {a-has-neg-prec-f | f pre M (a)}

τ M add (a) = {a-has-add-f | f add M(a)}

τ M del (a) = {a-has-del-f | f del M(a)}

τ M a = τ M pre+(a) τ M pre (a) τ M add (a) τ M del (a)

Γ(M) = τ M I τ M G τ M A

Note that Γ : M(F,A) 2F(F,A) is a bijective mapping and we will use the function Γ 1 to identify the model in M(F,A), corresponding to a specific subset of F(F,A). Definition 3. A model reconciliation explanation problem is defined by the tuple PMRE = MR, MR h , π R , where MR = F MR, AMR, δMR, IMR, GMR is a model that the robot is using in its decision-making; MR h = F MR h , AMR h , IMR h , GMR h is the model the human observer is associating with the robot; and π R is the robot s plan to be explained. We demand that the models share the same fluents and action names F MR = F MR h , AMR = AMR h , and that π R is optimal in the model MR.

Proceedings of the Thirty-First International Joint Conference on Artiﬁcial Intelligence (IJCAI-22)

Note that the requirement of using identical action names and fluents is not a restriction. Using the same action name set is a canonical requirement as we assume that the only confusion that might exist is due to misaligned action definitions, i.e., the human observer might not have a perfect understanding of an action s preconditions and effects, but does know which action is being observed. Requiring identical fluent sets is just for convenience, but not a restriction either, since we can always define this shared/identical fluent set as the union of the individual ones in case they are different. Having defined the problem definition formally, we still need to say what a solution to it is. Solutions to model reconciliation explanation problems are called explanations, which in turn are defined based on model updates, which we define next. A model update updates the human s model MR h to make it align with the actual model, i.e., the one of the robot, MR. Formally, such updates are defined as follows:

Definition 4. For a given model reconciliation problem PMRE = MR, MR h , π R , a model update is given by a tuple E = ϵ+, ϵ , such that ϵ+ Γ(MR) \ Γ(MR h ) and ϵ Γ(MR h ) \ Γ(MR). We will refer to the model MR h + E = Γ 1((Γ(MR h ) \ ϵ ) ϵ+) as the updated human model that results from applying E.

We can now define solutions for model reconciliation explanation problems. Note that we don t require a complete set of changes to the human model making it identical to the actual one. It suffices to explain the robot s plan, i.e., so that this plan becomes optimal in the human s model.

Definition 5. For a given model reconciliation explanation problem PMRE = MR, MR h , π R , a model update E = ϵ+, ϵ is considered to be a valid explanation if the plan π R is an optimal plan in MR h + E.

2.4 Relevant Complexity Classes

While many of the standard results related to classical planning tend to either fall into NP or PSPACE classes [Bylander, 1994], the problem studied in this paper focuses on a class that is placed between these classes. One way to view NP problems, is in terms of the existence of a witness or certificate that can be verified in polynomial time. Following Definition 2.1 by Arora and Barak [2009], a language L is said to be in NP if

x L u {0, 1}p(|x|)

such that M(x, u) = 1,

where M is a polynomial time Turing machine, p a polynomial and u is the witness. On the other hand, a language L is said to be in Σp 2 [Arora and Barak, 2009, Definition 5.1] if

x L u {0, 1}p(|x|) v {0, 1}p(|x|)

such that M(x, u, v) = 1,

where M is again a polynomial time Turing machine. Another way to view Σp 2 is in terms of oracle machines. The canonical Σp 2-complete problem is the special subclass of quantified boolean formula called QSAT2 [Stockmeyer,

1976], where QSAT2 corresponds to the question of satisfiability of a formula of the form

where X and Y are vectors over boolean variables and ϕ is a propositional formula defined over X and Y . Note that per Theorem 4.1 (1) from Stockmeyer [1976], QSAT2 is complete for Σp 2 regardless of the form. This fact is exploited in our membership proof as we map the PMRE to a quantified boolean formula which is not necessarily in either CNF or DNF form. In fact, in the formula used for the membership proof, while ϕ1(X) and ϕ3(X, Z) are in CNF, the subformula ϕ3(X, Y ) is a negation. Additionally, Theorem 4.1 (2) by Stockmeyer [1976] also shows that the subset QSAT2 3-DNF is also complete for Σp 2. So in our hardness proof rather than reducing arbitrary quantified boolean formulas into a PMRE , we focus on reducing an instance from the set QSAT2 3-DNF. The polynomial hierarchy (PH) is formed by taking the union over the various classes of the form ΣP i , where each class ΣP i is defined in the above form with i alternating existential and universal quantifiers (starting with an existential quantifier as in the case of ΣP 2 ). Finally, the PSPACE complexity class, covers all the problems that can be solved by a Turing machine with polynomial space [Arora and Barak, 2009]. A PSPACE-complete problem is the satisfiability of a TQBF or True Quantified Boolean Formula, where no restriction is placed on the quantification over the variables. While it is known that PH PSPACE holds, the problem of establishing PH = PSPACE remains an important open problem (or question, as it s not known yet).

3 Complexity Results for Model Reconciliation Explanation Problems

We are interested in the computational complexity of solving model reconciliation explanation problems. It is however rather obvious that checking whether any solution exists is a trivial problem:

Proposition 1. Let PMRE = MR, MR h , π R be a model reconciliation explanation problem. The question whether there exists a valid explanation can be decided in constant time. More precisely, the answer is always yes.

The reason why the answer is always yes is because we could always simply compute the difference between the sets Γ(MR h ) and Γ(MR) and present these differences as explanation. (And we know that this is always possible, so we don t need to do so just to decide whether this explanation exists it always does.) Thus, computing such an explanation is harder than deciding whether one exists; computing it is a linear problem. This corresponds to the class of explanation called model patch explanation previously studied in the literature [Chakraborti et al., 2017]. While model patch explanations are technically correct, they might in practice not be the best explanations as it would involve resolving differences that are irrelevant, in that they didn t cause confusion. Recall that the reason for the necessity of explaining something is that the robot s plan either

Proceedings of the Thirty-First International Joint Conference on Artiﬁcial Intelligence (IJCAI-22)

isn t even a plan at all in the human s model, or just not optimal. So any explanation should restrict to finding reasons pointing to any of these facts. Thus, what we are interested in is finding a minimal explanation, i.e., we want to present an explanation to the human user that involves the fewest possible number of model changes so that the observed plan is an optimal solution in his/her model even if there are still some differences to the robot s model (of which the human would then still be unaware of). Such explanations have been referred to as minimally complete explanations [Chakraborti et al., 2017]. To turn this optimization problem into a decision problem, we introduce (as it is usually done) an additional parameter representing the criterion that s being optimized in our case the number of performed changes. Formally:

Definition 6. For a given model reconciliation explanation problem PMRE = MR, MR h , π R , we define the optimal model reconciliation explanation decision problem as:

Given PMRE and a natural number k N {0}, does there exist a valid explanation E = ϵ+, ϵ for PMRE, such that |ϵ+| + |ϵ | = k? (We call this MRE-k.)

We are going to show that the problem is Σp 2-complete, which we show in the next two sections, one showing membership, the other showing hardness. To prove the computational complexity, we will focus on the canonical Σp 2 complete problem called QSAT2 [Stockmeyer, 1976], where QSAT2 corresponds to the question of satisfiability of a formula of the form X Y ϕ, where X and Y are disjoint sets of boolean variables and ϕ is a propositional formula defined over X and Y . When we focus on specific forms propositional formula, say 3-DNF, we will denote it as QSAT2 3-DNF.

3.1 Membership Proof Our first task would be to establish the fact that MRE-k is in a fact a member of the complexity class Σp 2. We will do so by reducing the problem into a QSAT2 problem. In particular, by mapping a model reconciliation explanation problem PMRE = MR, MR h , π R into QSAT2 of the form

X, Zϕ1(X) ( Y ϕ2(X, Y )) ϕ3(X, Z),

such that |X| = k |E+ E |, where E+ = Γ(MR)\Γ(MR h ) and E = Γ(MR h )\Γ(MR) are the set of propositional variables that will capture the possible individual model updates, Y corresponds to the propositional variables required to encode a planning problem where the maximum plan length is limited to |π R| 1 that will be used to capture the possible shorter plans and Z includes the propositional variables required to encode a planning problem where the maximum plan length is limited to |π R| which will be used to encode the validity of π R. Following the variables, ϕ1(X) is a CNF formula that enforces the fact that only explanations of size k are possible, ϕ2(X, Y ) is a CNF formula that encodes whether given the explanation a plan of length |π R| 1 can achieve the goal in the updated model and finally, ϕ3(X, Z) is a CNF formula that encodes whether given the explanation π R is valid in the updated model. Applying the negation and moving the

quantification upfront, we get the pre-nex QSAT2 form

X, Z Y ϕ1(X) ϕ2(X, Y ) ϕ3(X, Z)

Now the important parts of this compilation are encoding the enforcement of explanation length (through ϕ1(X)) and encoding planning models in such a way that they can reflect the effects of model updates captured by a particular instantiation of X variables (used in ϕ2(X, Y ) and ϕ3(X, Z).

Encoding Explanation Length The variable set X consists of k propositional variables for each individual model update, i.e,

τi E+ E {τ 1 i , ..., τ k i },

where each τ m i can be thought of as capturing the fact that the model update τi is applied at step m. Now our requirement is to enforce that only a single model update is applied at a given step. This is exactly done by ϕ1(X), where ϕ1(X) is a conjunction of clauses of the form

τj E+ E τj =τ1 τ m j .

ϕ1(X) will contain a clause for every pair of model updates τi, τj E+ E and every step m {1, ..., k}). Now ϕ1(X) cannot be true if for any step more than one model update variable is true.

Encoding Planning Models Conditioned on Model Updates Now the second part of the encoding requires that we have a way to capture the horizon-limited planning problem, that reflects the model updates captured by a given instantiation of X. This will be used in both ϕ2(X, Y ) and ϕ3(X, Z). The encoding will be based on the planning-as-SAT encoding discussed Section 2.2. Let ϕM T be the unmodified original SAT encoding (in CNF form) corresponding to a model M = F, A, δ, I, G for a planning horizon T. To allow for the model update, we will start with setting the

encoding to be equal to the human model (ϕPMRE T = ϕMR h T ). We first augment the model component clauses in this model. Specifically, let ψ be a clause corresponding to a model component that is part of the human model but not part of the robot model, and let the corresponding model parameter be τj E . Then we replace ψ in ϕPMRE T with a clause

( τ 1 j ... τ k j ) ψ,

This clause captures the fact that if the model component is not removed in the k explanation steps, then the model component should be considered when coming up with the plan. Note that this is still a clause as conjunction is on the left side of the implication. Let ψ be a clause corresponding to a model component that is part of the robot model but missing from the human model, with a corresponding model parameter be τj E+. We add a conjunction of the form given below to ϕPMRE T

(τ 1 j ψ ) ... (τ k j ψ )

Proceedings of the Thirty-First International Joint Conference on Artiﬁcial Intelligence (IJCAI-22)

That is, the model component needs to hold if the corresponding explanation is provided at any explanation step. Now we will remove all the original explanatory frame axioms and add one that covers action definitions from both models, i.e., for ever fluent f F MR and each time step m up to T 1 we add a clause of the form f m f m+1 Af add , where Af add = {a | a AMR f add MR add MR h }. We can similarly add an explanatory fluent for the deletes. Now to account for the explanation, we will add new clauses that will ensure that to use any previously missing adds or deletes at a time step, the respective model update should be performed at some explanation step or not performed at all if it was an effect that was not part of the robot model. Finally we leave the action exclusion clauses unmodified in the new model ϕPMRE T . This is sufficient as the human, robot and updated model all share the same action names. We can now see that this encoding is equivalent to the updated model. Proposition 2. Let x be a specific instantiation of the variable X corresponding to a model update E = ϵ+, ϵ , such that ϵ+ = {τ1, ..., τr}, ϵ = { τ1, ..., τp} and |ϵ+|+|ϵ | = k. Now let ϕ x(X) be a logical conjunction of the form

x1 τ1 ... xr τr xr+1 τ1 ... xk τp Now for the combined logical formula

ϕ x(X) ϕ1(X) ϕPMRE T ,

every instantiation of propositional variables that satisfies the formula corresponds to a plan for MR h + E. This fact should be obvious from the validity of the original encoding. Any differences in the encoding are only those related to the explanations. For example, in the new encoding the enforcement of a positive precondition f for an action al at time step m that could be removed by a model update is going to be, τ 1 ... τ k (am l f m 1), where τ = al-has-pos-prec-f. So if τ i is set true at any of the k sets then the precondition needs no longer to be satisfied. We get ϕ2(X, Y ) by using the ϕPMRE T encoding but for time horizon |π R| 1 (the encoding also includes NOOP actions to allow for shorter plans) and we define ϕ3(X, Z) to be equal to ϕPMRE |π R| (X, Z) ϕπ R,

where ϕπ R = a1 1 ...a|π R| |π R|, ai i is the variable in Z correspond-

ing to the ith action in plan π R for time step i. Lemma 1. A given problem PMRE has a k-sized explanation if and only if

X, Z Y ϕ1(X) ϕ2(X, Y ) ϕ3(X, Z)

is satisfiable. This follows directly from the construction and Proposition 2. The formula is only satisfied if there exists an instantiation of X corresponding to an explanation of length k (enforced by ϕ1(X)) that allows for the validity of the current plan (enforced by ϕ3(X, Z)) and doesn t allow for any shorter plans (enforced by ϕ2(X, Y )). This leads us to: Theorem 1. MRE-k is in Σp 2

3.2 Hardness Proof To prove that the problem MRE-k is Σp 2-hard, we will provide a polynomial reduction of a QSAT2 3-DNF instance (which has been shown to be Σp 2-complete [Stockmeyer, 1976]) into a k-bounded Model Reconciliation Explanation problem PMRE thus solving MRE-k. To present the reduction, consider an arbitrary QSAT2 3-DNF instance X Y ϕ, where ϕ is a disjunction consisting of N disjuncts (i.e., conjunctions) denoted as C1, .., CN (each of size 3 as ϕ is in 3-DNF) defined over the propositions in X and Y . As mentioned earlier, we will map the problem of checking the satisfiability of a propositional formula over a universal quantification to that of an optimality check. In particular, we will construct a planning model where the plan space covers the space of all possible instantiations of the universally quantified variables. We then establish the satisfiability of the universally quantified formula by showing that no plan (i.e., a specific instantiation of the variables) can satisfy the negation of the formula. This follows from the fact that

Though in our case, there is not only a universally quantified variable set Y but an existentially quantified variable set X. We will map this existentially quantified variable set into the initial state of the problem and will allow the model reconciliation problem to select any possible instantiation of X as part of the explanation. Thus mapping the problem to

X Y ϕ X ( Y ϕ)

That is, a valid explanation will show that there exists an initial state for which there exists no shorter action sequence that can satisfy the goal ϕ. We will also add some additional constraints in the two models that will form our model reconciliation explanation problem PMRE QSAT to ensure that the plan being explained will be optimal after all the differences between the models have been resolved. The exact construction of the PMRE QSAT problem is given below. Let us first start by defining the fluent set and the action names. Let the fluent set F be defined as

F = FX FY FN FG FD1 FD2 FS,

where FX and FY are the sets of fluents corresponding to X and Y , respectively (i.e., we could just set FX = X and FY = Y ), FN consists of a fluent per disjunct in ϕ (i.e., we could just set FN = {C1, . . . , CN}), FG = {g} contains a single goal fluent to be used by the models, FD1 is a set of dummy fluents such that |FD1| = |X|+1, FD2 is a second set of dummy fluents such that |FD2| = |Y | + N + 1 and FS = {ps} is a staging variable used to enforce action ordering. Now the action names A to be shared between the two models would be such that |A| = |Y | + 3 |FN| + |FD2| + |FD1| + 1, where we would have an action for each of the fluents in the corresponding fluent subsets Y and FD2, and an action for each conjunction of the propositional formula ϕ. Finally, there are |FD1|+1 goal actions , where there are |FD1| goal actions by which the goal can be established if ϕ can be achieved and there is one goal action to be used as part of π. Specifically, we will represent the action names as follows

A = AY A ϕ A(G, ϕ) AD2 A(G,D2)

Proceedings of the Thirty-First International Joint Conference on Artiﬁcial Intelligence (IJCAI-22)

Now we will define a model reconciliation explanation problem PMRE QSAT = M1, M2, π . The models are defined as M1 = F, A, δ, IM1, G and M2 = F, A, δ, IM2, G , where IM1 = X FS and IM2 = FD1 FS. Note that the models only differ in their initial states. We will now go on defining each of the actions. Starting with AY , an action ai Y AY (for a variable yi Y ) is defined by pre+(ai Y ) = FS, pre (ai Y ) = , add (ai Y ) = {f i Y }, and del (ai Y ) = . That is, the action definition for ai Y is empty but for a single add effect that sets the fluent corresponding to the variable yi true (f i Y FY ) and a positive precondition that requires the staging variable to be true. Next come the actions in A ϕ, which will help us test whether for a given instantiation of X and Y , the negation of the propositional formula ϕ(x, y) is satisfiable. Note that when we negate the 3-DNF ϕ, we obtain a 3-CNF ϕ, where each (ith) conjunction Ci gets turned into a disjunction (clause) C i given by {pi 1, pi 2, pi 3} (where the literals got inverted, i.e., switched from negated to positive and vice versa). Now for each literal in C i we will define an action ai,j ϕ, 1 j 3, as follows.

if pi j is positive we have:

pre+(ai,j ϕ) = {f j X Y }, pre (ai,j ϕ) = , add (ai,j ϕ) = {f i N}, and del (ai,j ϕ) = FS

and if pi j is negative then we define it as

pre+(ai,j ϕ) = , pre (ai,j ϕ) = {f j X Y }, add (ai,j ϕ) = {f i N}, and del (ai,j ϕ) = FS,

where f i N FN is an indicator variable identifying whether the clause C i is satisfied and f j X Y FX FY is the fluent corresponding to the proposition. That is, the fluent becomes a positive precondition if it was a positive literal in the clause (resulting from negating the conjunction), otherwise it becomes a negative precondition. If at least one of the literals in the clause is satisfied the clause is satisfied (captured by the add effect). Additionally, the action deletes the staging variable ps. This allows us to ensure that no action from AY can be performed after executing an action from the set A ϕ. Now one way for the goal g to be satisfied would be to satisfy all the negated clauses in ϕ, which is captured by the set of actions A(G, ϕ) = {a1 (G, ϕ), ..., a|X|+1 (G, ϕ)}. Here we have a possible goal action for each fluent in FD1. The actions here are defined such that pre+(ai (G, ϕ)) = FN {f i D1}, pre (ai (G, ϕ)) = , add (ai (G, ϕ)) = {g}, and del (ai (G, ϕ)) = , where f i D1 FD1. As we will see, once we complete the mapping of the satisfaction problem into the explanation problem, all the shorter action sequences that the explanation would need to invalidate would use these goal generating actions. The optimal plan π that needs to be explained is given by π = a1 D2, ..., a |FD2| D2 , a(G,D2) . This plan contains all

the actions that are part of AD2 = {a1 D2, ..., a |FD2| D2 } and A(G,D2) = {a(G,D2)}, such that

pre+(ai D2) = pre (ai D2) = , and for all f i D2 FD2: add (ai D2) = {f i D2}, del (ai D2) = , and

pre+(a(G,D2)) = FD2, pre (a(G,D2)) = , add (a(G,D2)) = {g}, and del (a(G,D2)) = . This brings us to the important properties (captured by the following propositions and lemmata) that will let us establish the soundness of the reduction. Proposition 3. π is optimal in M1. In M1 none of the variables in FD1 are true, neither can any action turn it true. Thus none of the goal actions in A(G, ϕ) can be used, leaving the model to use all actions in π to achieve the goal. Proposition 4. One can reach a state that captures (in terms of the truth values of FY ) any possible instantiation of the variables Y by a plan of length less than |π| N 1. The proposition follows directly given the size of |AY | and the fact that the actions in this set do not have preconditions. Proposition 5. Any possible instantiation of the variables X can be captured by the initial state of the updated model formed from a model update of size |X|. Note that the model update takes the form of ϵ+, ϵ , such that ϵ+ X and ϵ FD1. Thus one can create an explanation that sets some subset of X X true, by making ϵ+ equal to that subset (in terms of FX) and selecting a subset of FD1 as ϵ , such that |ϵ | = |X| |ϵ+|. Since |FD1| = |X|+1 and |ϵ | is a non-negative number upper-bounded by |X|, we can always find a subset of FD1 of size |X| |ϵ+|. Proposition 6. For a model update E = ϵ+, ϵ , where Xϵ+ contains the values from X corresponding to the update, there exists an action sequence π that is a valid plan in M2 + E such that |π | < |π|, if and only if there exists some instantiation of variables Y (say Y π ), such that for Xϵ+ and Y π it satisfies ϕ (denoted as (Xϵ+, Y π ) |= ϕ). This follows directly from the fact that an action sequence of length less than |π| can only satisfy the goal by using an action in A ϕ G , which requires satisfying all the clauses in ϕ. Similarly all instantiations of Y and testing validity of ϕ can be done in less than |π| steps, which brings us to the lemma: Lemma 2. For the model reconciliation explanation problem PMRE QSAT = M1, M2, π , there exists a valid explanation of size |X| if and only if the corresponding QSAT2 X Y ϕ is satisfiable.

Proof. This lemma can be directly built from the previous three propositions. If there exists a valid explanation of size |X| that means no plan of size less than |π| is valid, that means there exists an instantiation of variables X (say XE), such that for all instantiations Y of variables Y , we have

(XE, Y ) |= ϕ

which means, we have for all Y of Y

(XE, Y ) |= ϕ

Similarly if the QSAT2 formula was not satisfiable, then for every XE we should have at least one instantiation Y for

Proceedings of the Thirty-First International Joint Conference on Artiﬁcial Intelligence (IJCAI-22)

which (XE, Y ) |= ϕ. In the updated model we can now construct a plan that corresponds to Y and the evaluation of ϕ for Y which should satisfy an action in A ϕ G .

Which bring us to the theorem. Theorem 2. MRE-k is Σp 2-hard This theorem follows directly from Lemma 2 and the fact that QSAT2 3-DNF is Σp 2-complete. Finally, Theorem 1 and Theorem 2 brings us to our central result. Theorem 3. MRE-k is Σp 2-complete

4 Related Work While the complexity of the original model-reconciliation explanation has gone unexplored, there are complexity results from related problems that give us some clues about the actual complexity. For one, Sreedharan et al. [2020], showed PSPACE-completeness for providing a plan and a set of model updates such that the plan is valid in both the robot and the updated human model. Of course, here there is the additional complexity of identifying the plan and the problem overlooks the complexity of establishing the optimality, a central concern in the original model reconciliation formulation [Chakraborti et al., 2017]. On the other hand, Lin and Bercher [2021] established that the complexity of updating the model (with any or a minimal number of changes) ensuring the validity of a given plan is an NP-complete problem (for most cases, only a few are in P). However, they do not constrain the model updates to those that align with the target robot model directly, as this is only implicitly provided via the plan that s supposed to be valid. Finally, Vasileiou et al. [2021], looked at a variant of model reconciliation that is framed as the problem of finding the shortest logical support of a given propositional formula in the context where the human and robot model are represented as propositional knowledge bases. They discuss a possible membership of this problem in the Σp 2 class, but unfortunately, again the problem they define is different from the one studied by Chakraborti et al. [2017]. Vasileiou et al. [2021] looked at a case where there exists a knowledge base associated with the system KBa and one associated with the human KBh and there is a logical formula ϕ that needs to be explained such that KBa |= ϕ and KBh |= ϕ. The explanation here takes the form of a support ϵ KBa KBh such that KBh ϵ |= ϕ (as discussed by Vasileiou et al. [2021] in Definition 7). Given the generality of this formulation, one could map explanations for a classical planning problem partially into this framework, however it is not the exact problem studied by Chakraborti et al. [2017]. The first point to note is the fact that the explanation here doesn t support removal of rules from the human s knowledge base, a key form of model update discussed by Chakraborti et al. [2017]. While the definition does not allow for such a change, their algorithm (Algorithm 2) does include an ad-hoc test for satisfiability of KBa KBh and the algorithm allows for the removal of formulas from KBh if the conjunction is unsatisfiable. But this doesn t cover all the changes that are supported by Chakraborti et al. [2017]. For example, consider a case when an action a has an additional add effect e

in the human knowledge base, which manifests in the form of two rules, a rule of the form

and a rule in the explanatory frame axiom that says a is a possible action that can satisfy the transition from e to e . In this case, the problem encoding of length n (n being the length of the plan being explained), the formula KBa KBh needs not be unsatisfiable, especially if the plan being explained is not using a or e. However this rule could prevent some ϕ, say there doesn t exist a plan of length shorter than n, from being entailed without its removal. For example, let there be an action a2 that directly sets the goal true if e is satisfied and there are no actions in KBa that could have satisfied e. Now without removing this additional add effect there will always be a shorter plan. Unfortunately, after the first satisfiability test Vasileiou et al. [2021] don t provide any other way of removing rules from the human s knowledge base. Next the paper breaks down the problem of explaining optimality of the plan into two separate problems. First it explains the validity and then it explains optimality. For explaining validity they mention adding the plan and the goal as constraints into the planning model as additional clauses and then testing for satisfiability. If the encoding is unsatisfiable, the authors mention that they add the missing actions as part of the explanation [Vasileiou et al., 2021, page 5]. If this means they add all missing information in KBh for actions in the plan, this will already result in more information that the one considered in the original model reconciliation work [Chakraborti et al., 2017]. However, if they have some procedure to find the minimal information needed to be added to ensure optimality, this could still result in longer explanations. This is because choices made to ensure validity has an impact on the information needed to be provided to ensure optimality. As such the problem of finding model updates to ensure validity and optimality cannot be separated. For example, consider a case where the plan is invalid because a precondition for an action is unsatisfied in the human model. Now assume there are two possible minimal updates to ensure validity. One could say that the unsatisfied precondition is not part of that action in the knowledge base KBh or there exists a previously missing effect of an earlier action that can satisfy this precondition (though it s not needed in KBa). However one could build the rest of the model in such a way that adding the add effect information would result in other shorter plans being feasible. Say there are actions which can satisfy the goal directly whose only precondition in KBh is satisfied by this effect, while those actions have extra preconditions in KBa. This means the choice to introduce the add effect could make the explanation longer. Similarly we can create domains where the choice to remove the precondition would result in longer explanations.

5 Conclusion One of the immediate points of interest is the comparison of the complexity of model-reconciliation with the complexity of classical planning. When no information about the problem to solve is given, worst case complexity is PSPACEcomplete [Bylander, 1994]. Unless the polynomial hierarchy

Proceedings of the Thirty-First International Joint Conference on Artiﬁcial Intelligence (IJCAI-22)

collapses the problem of model reconciliation is thus easier than simple plan existence. This comparison is however not perfectly fair since in model reconciliation we have a plan given as an input thus bounding possible changes. While bounded plan existence is still PSPACE-complete since plan length can be bounded logarithmically, it turns NP-complete when encoded unarily (thus simulating the situation of model reconciliation where the bound is not given as number but explicitly via an input plan). Model reconciliation is thus harder than the respective bounded plan existence problem unless the polynomial hierarchy collapses. Another consequence of the proof is the existence of an alternate problem formulation for generating a minimally complete explanation, namely by mapping it to QSAT2 of increasing explanation length. This means one could use fast quantified boolean formula solvers to generate such explanations. One of the future directions for the work may be to investigate whether the use of this compilation provides an advantage over the A model space search proposed by Chakraborti et al. [2017]. Going forward it may also be worth investigating special cases of the model reconciliation explanation (restrictions on the planning model) that might be more tractable and consider the hardness of the various extensions of the modelreconciliation framework like those discussed by Sreedharan et al. [2018; 2019]. Another interesting direction of future work is generating lies as formalized by Chakraborti and Kambhampati [2019], which is also closely related to model reconciliation. In this case, the objective of the model updates remains the same, i.e., the robot is trying to ensure the plan is optimal in the updated model, but the model-updates is no longer required to be part of the robot s true model.

Acknowledgments

This research is supported in part by ONR grants N0001416-1-2892, N00014-18-12442, N00014-18-12840, N00014-9-1-2119, AFOSR grant FA9550-18-1-0067, DARPA SAIL-ON grant W911NF19-2-0006 and a JP Morgan AI Faculty Research grant.

[Arora and Barak, 2009] Sanjeev Arora and Boaz Barak. Computational Complexity - A Modern Approach. Cambridge University Press, 2009.

[Bylander, 1994] Tom Bylander. The computational complexity of propositional STRIPS planning. Artif. Intell., 69(1-2):165 204, 1994.

[Chakraborti and Kambhampati, 2019] Tathagata Chakraborti and Subbarao Kambhampati. (when) can ai bots lie? In Proceedings of the 2019 AAAI/ACM Conference on AI, Ethics, and Society, pages 53 59, 2019.

[Chakraborti et al., 2017] Tathagata Chakraborti, Sarath Sreedharan, Yu Zhang, and Subbarao Kambhampati. Plan explanations as model reconciliation: Moving beyond explanation as soliloquy. In IJCAI 2017, pages 156 163. IJCAI Organization, 2017.

[Chakraborti et al., 2020] Tathagata Chakraborti, Sarath Sreedharan, and Subbarao Kambhampati. The emerging landscape of explainable automated planning & decision making. In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI 2020, pages 4803 4811. IJCAI Organization, 2020. [Fox et al., 2017] Maria Fox, Derek Long, and Daniele Magazzeni. Explainable Planning. In IJCAI XAI Workshop, pages 24 30. XAI, 2017. [Geffner and Bonet, 2013] Hector Geffner and Blai Bonet. A concise introduction to models and methods for automated planning, volume 7 of Synthesis Lectures on Artificial Intelligence and Machine Learning. Morgan & Claypool Publishers, 2013. [Hoffmann and Magazzeni, 2019] J org Hoffmann and Daniele Magazzeni. Explainable AI planning (XAIP): overview and the case of contrastive explanation (extended abstract). In Reasoning Web. Explainable Artificial Intelligence, volume 11810 of Lecture Notes in Computer Science, pages 277 282. Springer, 2019. [Kautz et al., 1996] Henry A. Kautz, David A. Mc Allester, and Bart Selman. Encoding plans in propositional logic. In KR 96, pages 374 384. Morgan Kaufmann, 1996. [Lin and Bercher, 2021] Songtuan Lin and Pascal Bercher. Change the world how hard can that be? on the computational complexity of fixing planning models. In IJCAI 2021, pages 4152 4159. IJCAI Organization, 2021. [Sreedharan et al., 2018] Sarath Sreedharan, Tathagata Chakraborti, and Subbarao Kambhampati. Handling model uncertainty and multiplicity in explanations via model reconciliation. In ICAPS 2018, pages 518 526. AAAI Press, 2018. [Sreedharan et al., 2019] Sarath Sreedharan, Alberto Olmo Hernandez, Aditya Prasad Mishra, and Subbarao Kambhampati. Model-free model reconciliation. In IJCAI 2019, pages 587 594. IJCAI Organization, 2019. [Sreedharan et al., 2020] Sarath Sreedharan, Tathagata Chakraborti, Christian Muise, and Subbarao Kambhampati. Expectation-aware planning: A unifying framework for synthesizing and executing self-explaining plans for human-aware planning. In AAAI 2020, pages 2518 2526. AAAI Press, 2020. [Sreedharan et al., 2021] Sarath Sreedharan, Tathagata Chakraborti, and Subbarao Kambhampati. Foundations of explanations as model reconciliation. Artificial Intelligence, 301:103558, 2021. [Stockmeyer, 1976] Larry J Stockmeyer. The polynomialtime hierarchy. Theoretical Computer Science, 3(1):1 22, 1976. [Vasileiou et al., 2021] Stylianos Loukas Vasileiou, Alessandro Previti, and William Yeoh. On exploiting hitting sets for model reconciliation. In AAAI 2021, pages 6514 6521. AAAI Press, 2021.

Proceedings of the Thirty-First International Joint Conference on Artiﬁcial Intelligence (IJCAI-22)