On the Computational Complexity of Model Reconciliations

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 Σp2 -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 reduction 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 = ⟨preM+ , preM- , 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

Note that when we refer to an "action" we usually mean its name a ∈ AM, not its precondition and effect tuple (preM+ (a), preM- (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) = preM+ (a) ⊆ s and s ∩ preM- (a) = ∅. The effect of executing an action is represented by the function γ(a, s,M) defined as:

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

̸

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

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 ati ⇒ pt+1 , for all time steps t. Similarly, an example of an explanatory clause for p would be

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 ∧

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 MRh (i.e., the robot model assumed by the human) and is trying to make sense of the robot's plan. If the model MRh is different fromMR, 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 MRh . 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 fromM(F,A) to a subset of propositions F (F,A) (henceforth referred to as model parameters), where

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

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 P MRE = ⟨MR,MRh , π∗R⟩, where MR = ⟨F MR ,AMR , δMR , IMR ,GMR ⟩ is a model that the robot is using in its decision-making; MRh = ⟨F MRh , AMRh , IMRh , GMRh ⟩ 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 MRh , AMR = AMRh , and that π∗R is optimal in the model MR.

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 MRh 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 P MRE = ⟨MR,MRh , π∗R⟩, a model update is given by a tuple E = ⟨ϵ+, ϵ-⟩, such that ϵ+ ⊆ Γ(MR) \ Γ(MRh ) and ϵ- ⊆ Γ(MRh ) \ Γ(MR). We will refer to the model MRh + E = Γ-1 ((Γ(MRh ) \ ϵ-) ∪ ϵ+) 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 P MRE = ⟨MR,MRh , π∗R⟩, a model update E = ⟨ϵ+, ϵ-⟩ is considered to be a valid explanation if the plan π∗R is an optimal plan inMRh + 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

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 Σp2 [Arora and Barak, 2009, Definition 5.1] if

where M is again a polynomial time Turing machine. Another way to view Σp2 is in terms of oracle machines.

The canonical Σp2 -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 Σp2 regardless of the form. This fact is exploited in our membership proof as we map the P MRE 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 Σp2 . So in our hardness proof rather than reducing arbitrary quantified boolean formulas into a P MRE , 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 ΣPi , where each class ΣPi is defined in the above form with i alternating existential and universal quantifiers (starting with an existential quantifier as in the case of ΣP2 ). 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 P MRE = ⟨MR,MRh , π∗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 Γ(MRh ) 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 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 P MRE = ⟨MR,MRh , π∗R⟩, we define the optimal model reconciliation explanation decision problem as:

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

We are going to show that the problem is Σp2 -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 Σp2 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 Σp2 . We will do so by reducing the problem into a QSAT2 problem. In particular, by mapping a model reconciliation explanation problem P MRE = ⟨MR,MRh , π∗R⟩ into QSAT2 of the form

such that |X| = k·|E+∪E-|, where E+ = Γ(MR)\Γ(MRh ) and E- = Γ(MRh )\Γ(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

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,

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

ϕ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 ϕMT 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 (ϕP MRE T = ϕMRh 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 ϕP MRE T with a clause

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 ϕP MRE T

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 ⇒ Afadd , where Afadd = {a | a ∈ AMR ∧ f ∈ add MR ∪ add MRh }. 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 ϕP MRE 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

Now for the combined logical formula

every instantiation of propositional variables that satisfies the formula corresponds to a plan for MRh + 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 ⇒ (aml ⇒ 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 ϕP MRE 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

where ϕπ∗R = a11 ∧...a|π∗R| |π∗R| , aii is the variable in Z corresponding to the ith action in plan π∗R for time step i.

Lemma 1. A given problem P MRE has a k-sized explanation if and only if

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 Σp2

3.2 Hardness Proof

To prove that the problem MRE-k is Σp2 -hard, we will provide a polynomial reduction of a QSAT2 ∩ 3-DNF instance (which has been shown to be Σp2 -complete [Stockmeyer, 1976]) into a k-bounded Model Reconciliation Explanation problem P MRE 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

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 P MRE 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 P MRE 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

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

Now we will define a model reconciliation explanation problem P MRE 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 aiY ∈ AY (for a variable yi ∈ Y ) is defined by pre +(aiY ) = FS, pre -(aiY ) = ∅, add(aiY ) = {f iY }, and del (aiY ) = ∅. That is, the action definition for aiY is empty but for a single add effect that sets the fluent corresponding to the variable yi true (f iY ∈ 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 {pi1 , pi2 , pi3 } (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 pij is positive we have: pre +(ai,j ¬ϕ ) = {f jX∪Y }, pre -(ai,j ¬ϕ ) = ∅, add (ai,j ¬ϕ ) = {f iN }, and del (ai,j ¬ϕ ) = FS
• and if pij is negative then we define it as pre +(ai,j ¬ϕ ) = ∅, pre -(ai,j ¬ϕ ) = {f jX∪Y }, add (ai,j ¬ϕ ) = {f iN }, and del (ai,j ¬ϕ ) = FS ,

where f iN ∈ FN is an indicator variable identifying whether the clause C ′ i is satisfied and f jX∪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 iD1 }, pre -(ai(G,¬ϕ) ) = ∅, add(ai(G,¬ϕ) ) = {g}, and del (ai(G,¬ϕ) ) = ∅, where f iD1 ∈ 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 π = ⟨a1D2 , ..., a|FD2 | D2 , a(G,D2)⟩. This plan contains all the actions that are part of AD2 = {a1D2 , ..., a|FD2 | D2 } and A(G,D2) = {a(G,D2)}, such that

• pre +(aiD2 ) = pre -(aiD2 ) = ∅, and for all f iD2 ∈ FD2 : add (aiD2 ) = {f iD2 }, del (aiD2 ) = ∅, 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 inM1.

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 P MRE 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

which means, we have for all Y ′ of Y

Similarly if the QSAT2 formula was not satisfiable, then for every XE we should have at least one instantiation Y ′ for 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 Σp2 -hard

This theorem follows directly from Lemma 2 and the fact that QSAT2 ∩3-DNF is Σp2 -complete. Finally, Theorem 1 and Theorem 2 brings us to our central result.

Theorem 3. MRE-k is Σp2 -complete

4 RelatedWork

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 Σp2 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 formai ⇒ ei 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 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 N00014- 16-1-2892, N00014-18-1- 2442, 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.