Fixed-Parameter Tractable Reductions to SAT for Planning

1 Introduction

Like many other formalisms in AI, planning in general is highly intractable (many variants are complete for Σ P2 or even PSPACE). There are, however, several restricted settings where planning is in NP, and can thus be solved by encoding the problem into SAT and subsequently calling a SAT solver. Due to the great performance of modern SAT solvers in many practical settings [Sakallah and Marques-Silva, 2011; Gomes et al., 2008; Malik and Zhang, 2009], this is often a feasible approach. In the planning literature, the general approach of employing SAT solvers has been used also in planning settings that are beyond NP; e.g., see the approach presented by Palacios and Geffner [2009] to compile away uncertainty.

We extend this SAT-encoding approach by means of the framework of parameterized complexity theory. A classical complexity analysis can only provide a coarse complexity classification, that is based on the input size measured in bits only. However, in virtually all cases one knows more about the structure of the instance than is indicated in the raw bit size. Using parameterized complexity, one can capture information about structure in the input by means of a parameter. This parameter can then be used to provide a multivariate complexity analysis, that is sensitive to the structure of the input.

∗Supported by the Austrian Science Fund (FWF): P25518 and P26200, and the German Research Foundation (DFG): ER 738/2-1.

Recently, the idea of applying parameterized complexity to extend the range of cases where SAT solvers can be used to solve the problem has been applied to reasoning problems that are beyond NP [Fichte and Szeider, 2013; Pfandler et al., 2013]. In addition, theoretical tools have been developed that allow us to indicate the boundaries of this approach [De Haan and Szeider, 2014a; 2014b], i.e., to give evidence that the SAT-encoding approach cannot be used in certain cases.

In this paper, we provide parameterized complexity results for natural planning problems that are beyond NP. We point out several variants of planning where structure in the input admits the use of encodings into SAT as an efficient way to solve the problem. In addition, we identify several planning settings where the structure in the input does not suffice to allow this approach of direct SAT-encodings. We hope that our results may help initiate a structured investigation of the use of parameterized complexity methods aimed at obtaining SATencodings in the domain of planning. In addition, we expect that our results can be used, as a stepping stone, to obtain further parameterized complexity results for other reasoning problems that are beyond NP, since the formalism of planning is widely-known and intuitive to use. In particular, this holds for showing membership results, as planning is an expressive formalism in which other problems can often be encoded very conveniently. The fact that all complexity classes discussed in this work are characterized by different flavors of planning problems can facilitate this considerably. Moreover, as a side result, we develop a machine characterization of one of the parameterized intractability classes for this setting. We believe that this result will be useful in the future.

Main Contributions:

• We present completeness results for a variety of planning problems and parameterized complexity classes - classically all these problems are harder than NP, e.g., complete for Σ P2 or PSPACE. We show that two variants of planning under uncertainty and planning with soft goal optimization are complete for the classes para-NP, para-DP, and FPT NP[f(k)] , respectively. For these classes, the SAT approach offers potential for practical algorithms. We contrast these results by showing completeness for harder classes. Together, this gives a more fine-grained picture of the (sources of) complexity.

• This is the first work to characterize the parameterized complexity classes para-NP, para-DP, FPT NP[f(k)] , ∃k ∀∗ , and ∃∗∀k -W[P] by means of variants of a single formalism, i.e., planning. We hope that our homogeneous characterization of these classes will facilitate future complexity analysis. Additionally, the methodology used in this work may be applied to any KR formalism of high complexity.
• In addition, we present a novel machine characterization of the complexity class ∃∗∀k -W[P]. We expect that this result is especially useful for showing membership in this class.

Organization. After recalling the required basics in the next section, we discuss the idea of parameterized reductions to SAT in Section 3. In each of the Sections 4 to 8, we present a natural variant of planning that captures a particular parameterized complexity class. Finally, we conclude in Section 9.

2 Preliminaries

We assume the reader to be familiar with the basics of complexity theory and logic, such as classes from the Polynomial Hierarchy (PH), e.g., Σ P2 . For details we refer to textbooks on the topic [Papadimitriou, 1994; Arora and Barak, 2009].

Planning. In this work we build upon the SAS+ formalism (see, e.g., [B¨ackstr¨om and Nebel, 1995]). Let V = {v1, . . . , vn} be a finite set of variables over a finite domain D. Furthermore, let D+ = D ∪ {u}, where u is a special "undefined" value not present in D. Then Dn is the set of total states and (D+)n is the set of partial states over V and D. Clearly, Dn ⊆ (D+)n . The value of a variable v in a state s ∈ (D+)n is denoted by s[v]. A SAS+ instance is a tuple P = 〈V, D, A, I, G〉 where V is a set of variables, D is a domain, A is a set of actions, I ∈ Dn is the initial state and G ∈ (D+)n is the (partial) goal state. Each action a ∈ A has a precondition pre(a) ∈ (D+)n and an effect eff(a) ∈ (D+)n .

We will frequently use the convention that a variable has value u in a precondition/effect unless a value is explicitly specified. Furthermore, by slight abuse of notation, we denote actions and partial states such as preconditions, effects, and goals as follows: Let a ∈ A, pi ∈ V , di ∈ D, and 1 ≤ i ≤ m ≤ n such that pre(a)[p1] = d1, . . . , pre(a)[pm] = dm. Then we denote the precondition pre(a) by pre(a) = {p1 = d1, . . . , pm = dm} (analogously for effects). For m′ ≤ n and ej ∈ V with 1 ≤ j ≤ m′ , we use a : {p1 = d1, . . . , pm = dm} → {e1 = d′1 , . . . , em′ = d′m′ } as a shorthand to describe that a has pre(a) = {p1 = d1, . . . , pm = dm} and eff(a) = {e1 = d′1 , . . . , em′ = d′m′}.

Let a ∈ A and s ∈ Dn . Then a is valid in s if for all v ∈ V , either pre(a)[v] = s[v] or pre(a)[v] = u. The result of a in s is a state t ∈ Dn defined such that for all v ∈ V , t[v] = eff(a)[v] if eff(a)[v] ̸= u and t[v] = s[v] otherwise. Let s0, sℓ ∈ Dn and let ω = 〈a1, . . . , aℓ〉 be a sequence of actions (of length ℓ). Then ω is a plan from s0 to sℓ if either (i) ω = 〈〉 and ℓ = 0, or (ii) there are states s1, . . . , sℓ-1 ∈ Dn such that for all 1 ≤ i ≤ ℓ, ai is valid in si-1 and si is the result of ai in si-1. A state s ∈ Dn is a goal state if for all v ∈ V , either G[v] = s[v] or G[v] = u. An action sequence ω is a plan for P if ω is a plan from I to a goal state.

In planning instances often so-called conditional effects are permitted as effects. For a planning instance with n variables and domain D, let 1 ≤ m1,m2 ≤ n. A conditional effect is an effect of the form {p1 = d11 , . . . , pm1 = d1m1 } ▷ {e1 = d21 , . . . , em2 = d2m2 } with d1i , d2j ∈ D, 1 ≤ i ≤ m1 and 1 ≤ j ≤ m2. Without defining the semantics formally, a conditional effect (of an executed action) ensures that the effect {e1 = d21 , . . . , em2 = d2m2 } only materializes if its condition {p1 = d11 , . . . , pm1 = d1m1 } is also satisfied.

Parameterized Complexity. Before we turn to parameterized algorithms for SAT-encodings, we introduce some core notions from parameterized complexity theory. For an indepth treatment we refer to other sources [Downey and Fellows, 1999; 2013; Flum and Grohe, 2006; Niedermeier, 2006]. A parameterized problem L is a subset of Σ∗ × N for some finite alphabet Σ. For an instance (I, k) ∈ Σ∗ × N, we call I the main part and k the parameter. The following generalization of polynomial time computability is commonly regarded as the tractability notion of parameterized complexity theory. A parameterized problem L is fixed-parameter tractable if there exists a computable function f and a constant c such that there exists an algorithm that decides whether (I, k) ∈ L in time O(f(k) |I|c ), where |I| denotes the size of I. Such an algorithm is called an fpt-algorithm, and this amount of time is called fpt-time. FPT is the class of all fixed-parameter tractable decision problems. If the parameter is constant, then fpt-algorithms run in polynomial time where the order of the polynomial is independent of the parameter.

Parameterized complexity also generalizes the notion of polynomial-time reductions. Let L ⊆ Σ∗ × N and L′ ⊆ (Σ′ )∗ × N be two parameterized problems. An fpt-reduction from L to L′ is a mapping R : Σ∗ × N → (Σ′ )∗ × N from instances of L to instances of L′ such that there exist some computable function g : N → N such that for all (I, k) ∈ Σ∗ ×N: (i) (I, k) is a yes-instance of L if and only if (I ′ , k′ ) = R(I, k) is a yes-instance of L′ , (ii) k′ ≤ g(k), and (iii) R is computable in fpt-time.

3 Parameterized Encodings into SAT

Problems that can be solved by means of a fixed-parameter tractable (many-one) encoding into SAT are captured by the class para-NP, that is defined as follows. Let C be a classical complexity class, e.g., NP. The parameterized complexity class para-C is defined as the class of all parameterized problems L ⊆ Σ∗ × N, for some finite alphabet Σ, for which there exist an alphabet Π, a computable function f : N→Π∗ , and a problem P ⊆ Σ∗ × Π∗ such that P ∈ C and for all instances (x, k) ∈ Σ∗ ×N of L we have that (x, k) ∈ L if and only if (x, f(k)) ∈ P [Flum and Grohe, 2003].

In addition to many-one fpt-reductions to SAT, we are also interested in Turing fpt-reductions. A Turing fpt-reduction from a problem P to SAT is an fpt-algorithm that has access to a SAT oracle and that decides P . We are mainly interested in fpt-algorithms that only use a small number of queries to the SAT oracle (SAT calls). We let FPT NP[f(k)] denote the class of all parameterized problems P for which there exists an fpt-algorithm that decides if (x, k) ∈ P by using at most f(k) many SAT calls, for some computable function f.

In order to provide evidence against the existence of (many-one) fpt-reductions to SAT, one can show hardness for para-Σ P2 . Recent work in parameterized complexity theory has resulted in additional complexity classes that can be used to provide evidence for the non-existence of fpt-reductions to SAT [De Haan and Szeider, 2014b]. The parameterized complexity class ∃k ∀∗ consists of all parameterized problems that can be fpt-reduced to the problem ∃k ∀∗ -WSAT, which is a variant of quantified Boolean satisfiability that is based on truth assignments of restricted (Hamming) weight. The input for this problem is a quantified Boolean formula (QBF) ϕ = ∃X∀Y ψ, and an integer k. The parameter is k, and the question is whether there is a truth assignment α to X of weight k such that for all truth assignments β to Y it holds that α ∪ β satisfies ψ. There is evidence that problems that are hard for ∃k ∀∗ do not allow an fpt-reduction to SAT or UNSAT [De Haan and Szeider, 2014b]. Similarly, the intractability class ∃∗∀k -W[P] has been defined based on an analogous restriction on the weight of assignments for quantified Boolean circuits, a generalization of QBFs. Formally, the class ∃∗∀k -W[P] consists of all parameterized problems that can be fpt-reduced to the problem ∃∗∀k -WSAT(CIRC). The input for this problem is a quantified Boolean circuit ϕ = ∃X∀Y C, and an integer k. The parameter is k, and the question is whether there is a truth assignment α to X such that for all truth assignments β to Y of weight k it holds that α ∪ β satisfies the circuit C.

For an overview of parameterized complexity classes that are relevant to the results in this paper, we refer to Figure 1. For a more detailed discussion, we refer to previous work on this topic [De Haan and Szeider, 2014b].

4 A para-NP-complete Variant

We start our analysis with a parameterized version of planning with uncertainty in the initial state where the plan length is polynomially bounded in the input size. Classically this problem is known to be Σ P2 -complete [Baral et al., 2000]. More formally, we analyze the following problem:

PLANNING[UNCERTAINTY] Instance: A planning instance P = 〈V, Vu, D, A, I, G〉 similar to a classical planning instance, but containing additional variables Vu that are unknown in the initial state, i.e., for all v ∈ Vu it holds that I(v) = u. Parameter: |Vu| + |D|. for all complete initial states, i.e., each possible way of com-

Question: Is there a plan of polynomial length for P that works pleting I with a combination of values for variables in Vu?

PLANNING[UNCERTAINTY] turns out to be para-NP-complete and thus admits an fpt-reduction to SAT. In other words, even though the problem is Σ P2 -complete from the classical perspective, an encoding into SAT is feasible if the number of unknown variables is moderately large, as long as we are only interested in short, i.e., polynomially bounded, plans. In addition, this means that we can characterize the class para-NP by planning with uncertainty in the initial state if the degree of uncertainty, i.e., the number of variables that are unknown, and the size of the domain are considered as parameter.

Theorem 1. The problem PLANNING[UNCERTAINTY] is para-NP-complete if the plan length is bounded by a polynomial in the input size.

Proof. The basic idea of the membership proof is that we can materialize all initial states in the transformation of the planning instance into SAT by an fpt-reduction. Let n be the input size and m = p(n) be a bound on the plan length where p is an arbitrary polynomial that bounds the plan length. To show membership, recall that classical planning is NP-complete if the plan length is at most m. Thus, for a classical planning instance P we can construct a propositional formula ϕ[P, VA] in polynomial time that is satisfiable if and only if there is a plan of length at most m for P, where VA contains all variables representing actions. Due to the uncertainty in the initial state in PLANNING[UNCERTAINTY], there is not a single initial state, but rather a set of initial states I of cardinality |D||Vu| . Now let P′ be an instance of PLANNING[UNCERTAINTY] and I ∈ I. Then, let P′ (I) denote the classical planning instance obtained by instantiating the unknown variables in P′ with the values of the corresponding variables in I. To show membership, we construct the formula ψ = ∧I∈I ϕ[P′ (I), VA] of conjuncts that are variable-disjoint (except VA). Clearly, ψ is satisfiable if and only if P′ is a yes-instance.

For para-NP-hardness, notice that the construction used in a proof by Kronegger et al. [2013, Theorem 11] for SAS+ planning even holds if Vu = ∅.

5 A para-DP-complete Variant

The complexity class DP consists of all problems that can be reduced to the problem SAT-UNSAT = { (ϕ, ψ) | ϕ ∈ SAT, ψ ∈ UNSAT}. The class para-DP is interesting as at most two calls to a SAT solver are required to solve any instance. Therefore, showing membership in para-DP can be a positive result for hard problems. In what follows we will describe a natural planning problem complete for this class.

We consider a variant of planning with uncertainty in the initial state as described in Section 4. The crucial difference is that we ask whether an action a0 is essential. More formally, we consider the following problem.

PLANNING[ESSENTIAL ACTION]

Instance: A planning instance with uncertainty in the initial

state P = 〈V, Vu, D, A, I, G〉 and an action a0 ∈ A.

Parameter: |Vu| + |D|.

Question: Is a0 essential, i.e., is there a plan of polynomial length for P that uses a0 and works for all complete initial states, but there is no such plan for P without using a0?

We now show that this problem is para-DP-complete and thus can be solved by two SAT-calls for polynomial plan length.

Theorem 2. The problem PLANNING[ESSENTIAL ACTION] is para-DP-complete if the plan length is bounded by a polynomial in the input size.

Proof. To establish hardness, we will show that we can encode an instance of the SAT-UNSAT problem into an instance of PLANNING[ESSENTIAL ACTION]. For this, let (ϕ, ψ) be a SAT-UNSAT instance. Recall that classical planning is NP-complete if the plan length is bounded by a polynomial in the input size. Therefore, there are two planning instances Pϕ = 〈Vϕ, Vu,Dϕ,Aϕ, Iϕ,Gϕ〉 and Pψ = 〈Vψ, Vu, Dψ, Aψ, Iψ, Gψ〉 with Vu = ∅ and with disjoint variables, actions, and domain such that Pϕ (resp., Pψ) has a plan of polynomial length if and only if ϕ (resp., ψ) is satisfiable. We use now the action a0 of verify that Pψ has indeed no plan.

From Pψ we construct an instance P′ψ as follows: Let the set of actions A′ψ = Aψ ∪ {a0 : {} → Gψ} be defined by adding to Aψ an additional action with empty precondition that immediately fulfills the goal Gψ. Further, let P′ψ = 〈Vψ, Vu,Dψ,A′ψ , Iψ,Gψ〉. We now combine Pϕ and P′ψ to a single planning instance P∗ (with uncertainty in the initial state). Notice that this can always be done as the instances are disjoint. The instance of PLANNING[ESSENTIAL ACTION] is then given by (P∗ , a0). It is now easy to verify that (i) there is a plan for P∗ and (ii) a0 is essential if and only if ϕ is satisfiable and ψ is unsatisfiable.

Membership in para-DP can be shown as follows. Let (P = 〈V, Vu,D,A, I,G〉, a0) be an instance of PLANNING[ESSENTIAL ACTION] and k be a bound on the plan length that is polynomial in the input size. W.l.o.g., we assume that 0, 1 ∈ D. We have to check whether there is a plan that uses a0 and that there is no plan without using a0. Recall from the proof of Theorem 1 that we can construct in fpt-time for an arbitrary instance P of PLANNING[UNCERTAINTY] (parameterized by |Vu| + |D|) a propositional formula ϕ[P] that is satisfiable if and only if P is a yes-instance.

To ensure that action a0 is indeed used, we create the instance P′ = 〈V ∪ {va0 }, Vu,D,A′ , I ′ ,G′ 〉 where we introduce the new variable va0 . Let I ′ (va0 ) = 0, G′ (va0 ) = 1, I ′ (v) = I(v) and G′ (v) = G(v) for each v ∈ V . We obtain A′ from A by adding va0 = 1 to the effect of action a0. Furthermore, we create for the case where a0 must not be used the instance P′′ = 〈V, Vu,D,A \ {a0}, I,G〉. The instance of SAT-UNSAT is then given by (ϕ[P′ ], ϕ[P′′ ]). In the construction we ensure that there is a plan of (of length at most k) that uses action a0, and that there is no plan (of length at most k) without using action a0.

6 An FPT NP[f(k)] -complete Variant

In this section, we investigate the following planning problem with two different types of goals: (i) a hard goal Gh that needs to be satisfied, and (ii) a soft goal Gs for which the number of variables satisfied according to Gs is to be maximized. We call a plan optimal with respect to some given bound k on the plan length if there does not exist another plan with length at most k that satisfies more variables according to the soft goal Gs. We analyze the problem of finding an optimal plan given a planning instance P = 〈V, D, A, I, Gh, Gs〉 and a bound k on the plan length, parameterized by |Gs|.

In general, finding an optimal plan for P given a bound k on the plan length in polynomial time requires O(log |P|) many SAT calls. We can find such a plan by performing binary search on the number of fulfilled variables in the soft goal, asking whether ≤ ℓ variables in the soft goal can be fulfilled. We show that we can restrict the number of SAT calls to a function of the number of variables in the soft goal, i.e., |Gs|. We believe that this result indicates that the SAT approach is still feasible for this (parameterized) problem. First, we show that planning with soft goals can be solved in fpt-time using ⌈log |Gs|⌉ SAT calls. Second, we prove that the number of required SAT calls cannot be bounded by a constant.

Proposition 3. Let P = 〈V,D,A, I,Gh,Gs〉 be a planning instance with a hard goal Gh and a soft goal Gs, and let k be an integer that is polynomial in the input size. Then finding a plan of length at most k that is optimal for P with respect to k (if it exists) can be done in fpt-time using ⌈log |Gs|⌉ SAT calls.

Proof (sketch). The problem of deciding whether there is a plan of length at most k that reaches some state s′ satisfying the hard goal Gh and that agrees with the soft goal Gs on at least u variables is in NP. Namely, one can guess such a plan, and verify whether it satisfies the requirements. Therefore, any instance of this problem can be encoded into an instance of SAT in polynomial time. Moreover, from a satisfying assignment (if one exists) for such a SAT instance, we can extract in polynomial time a plan that satisfies the requirements. Then we can find the maximum number u of variables contained in the soft goal that can be fulfilled using ⌈log |Gs|⌉ SAT calls, by using binary search. Moreover, using the satisfying assignments that are given by the SAT solver, we can find a plan that is optimal for P with respect to length k.

In order to show that we cannot find such an optimal plan in fpt-time using a constant number of SAT calls, we consider the following parameterized decision problem.

PLANNING[SOFT GOAL]-PARITY

Instance: A planning instance P = 〈V, D, A, I, Gh, Gs〉 with a hard goal Gh and a soft goal Gs, and an integer k.

Parameter: |Gs|.

Question: Does there exist a plan of length at most k that is optimal for P (w.r.t. k), and that satisfies an odd number of variables of the soft goal?

We show that this problem is complete for the class FPT NP[f(k)] . It follows that if we could find an optimal plan in fpt-time using a constant number of SAT calls (where the parameter is |Gs|), then the Polynomial Hierarchy would collapse [Endriss et al., 2014, Proposition 18].

Theorem 4. The problem PLANNING[SOFT GOAL]-PARITY is FPT NP[f(k)] -complete.

Proof (sketch). Membership in FPT NP[f(k)] follows directly from Proposition 3. To show hardness, we reduce from the problem SMALL-MAX-MODEL-PARITY. For this problem, the input is a CNF formula ϕ, and a subset X ⊆ Var(ϕ), where Var(ϕ) denotes the set of propositional variables of ϕ. The parameter is k = |X|. The question is whether the satisfying assignment that sets the maximum number of variables x ∈ X to true, satisfies an odd number of variables in X. This problem can straightforwardly be shown to be FPT NP[f(k)] - complete, using results by Endriss et al. [2014, Theorem 15]. (Due to space limitations, we omit the proof.)

Let (ϕ,X) specify an instance of SMALL-MAX-MODELPARITY, where ϕ has u clauses. We construct a planning instance P = 〈V,D,A, I,Gh,Gs〉, with a hard goal Gh and a soft goal Gs, and an integer k′ bounding the plan length as follows. We let V = Var(ϕ) ∪ {zx | x ∈ Var(ϕ) } ∪ {yδ | δ is a clause of ϕ}, and D = {0, 1}. For each variable x ∈ Var(ϕ), we introduce two actions: ax0 : {} → {x = 0, zx = 1} and ax1 : {} → {x = 1, zx = 1}. Moreover, for each clause δ in ϕ and each literal l in δ, we introduce an action: aδl whose precondition requires all variables zx to have value 1 and requires the variable of l to be set in such a way that δ is satisfied, and whose effect ensures that yδ is set to 1. We let I(v) = 0 for all v ∈ V , Gh = { yδ = 1 | δ is a clause of ϕ}, and Gs = {x = 1 | x ∈ X }. Finally, we let k′ = |Var(ϕ)| + u.

The intuition behind this reduction is that the actions axi can be used to enforce a truth assignment over the variables in Var(ϕ), and that the actions aδl can be used to check that such a truth assignment satisfies all clauses δ of ϕ. It is straightforward to verify that those plans consisting of k′ actions - an action axi (for some i ∈ {0, 1}) for each x ∈ Var(ϕ), and an action aδl (for some l ∈ δ) for each δ ∈ ϕ - correspond to truth assignments over Var(ϕ) that satisfy ϕ. Moreover, only plans of this form can satisfy the hard goal. Then, finding such a plan that maximizes the number of fulfilled variables in the soft goal corresponds to a satisfying truth assignment that maximizes the number of satisfied variables in X. From this, the correctness of the reduction follows.

7 An ∃k ∀∗ -complete Variant

In this section we reconsider planning with uncertainty in the initial state as discussed in Section 4 and 5 with a different parameter. This time we allow for an unbounded number of unknown variables and parameterize by the bound k on the plan length. It turns out that the problem does not retain its full hardness although a feasible translation to SAT still seems to be unlikely. To be more precise, we show that this problem is ∃k ∀∗ -complete.

For membership we build upon the ∃∀-encoding of Rintanen [2007] for planning instances with uncertainty in the initial state and binary domain. There, a QBF of the form ∃X∀Y ψ, where ψ is a quantifier-free formula, is satisfiable if and only if there is a plan whose length is bounded by a given integer. Observe that X only contains variables representing actions. Furthermore, for any satisfying truth assignment the weight of X is equal to the plan length. Notice that this encoding assumes binary domains. Here, we consider planning instances with an arbitrarily large domain. However, since the domain is part of the input, the reduction also works for arbitrarily large domains. Thus, the aforementioned encoding together with the observations above allows to show membership in ∃k ∀∗ . Note that other encodings could in principle also be used for this purpose.

Corollary 5. Planning with uncertainty in the initial state parameterized by the plan length is in ∃k ∀∗ .

Next we show hardness. Note that this reduction makes use of conditional effects.

Theorem 6. Planning with uncertainty in the initial state parameterized by the plan length is ∃k ∀∗ -hard.

Proof. We reduce from ∃k ∀∗ -WSAT over QBFs in 3DNF, which is known to be ∃k ∀∗ -complete [De Haan and Szeider, 2014b]. Let (ϕ, k′ ) be an instance of ∃k ∀∗ -WSAT, where k′ is an integer, ϕ = ∃X∀Y ψ, and ψ = ∨1≤i≤m ∧1≤j≤3 li,j .

The variables of the planning instance P are V = X ∪ {c1, . . . , ck′} ∪ {e, g}. For every v ∈ X and 1 ≤ i ≤ k′ we introduce an action aiv : {v = ci = e = 0} → {v = ci = 1}. Furthermore, we introduce two additional actions: ae : {c1 = 1, . . . , ck′ = 1} → {e = 1}, and ag : {e = 1} → {{l1,1 = l1,2 = l1,3 = 1} ▷ {g = 1}, . . . , {lm,1 = lm,2 = lm,3 = 1} ▷ {g = 1}}. The set of actions A is then given by A = ⋃v∈X ⋃1≤i≤k′ {aiv } ∪ {ae, ag}. To obtain the instance P, we set Vu = Y , D = {0, 1}, I = 0|V | and G = {g = 1}.

The intuition of this encoding is to first guess an assignment α of weight k′ using k′ distinct actions aiv , then to fix this assignment using action ae and finally to evaluate α according to ϕ with the action ag. It is straightforward to check that (ϕ, k′ ) is a yes-instance if and only if there is a plan of length k = k′ + 2 for P.

8 An ∃∗∀k -W[P]-complete Variant

We now turn to a variant of planning with uncertainty in the initial state, i.e., planning with bounded deviation. Let P = 〈V, Vu, D, A, I, G〉 be such a planning instance. W.l.o.g., we assume 0 ∈ D which we call the base value for variables in Vu. Here, the parameter describes the maximum number of unknown variables that deviate from the base value. In other words, in this setting, there can be many unknown variables but only few of them have unexpected values - we however, do not know which. More formally, the problem is defined as follows.

PLANNING[BOUNDED DEVIATION]

Instance: A planning instance P = 〈V, Vu,D,A, I,G〉 and

two integers k and d.

Parameter: d.

Question: Does there exist a plan of length at most k that works for all complete initial states where at most d unknown variables deviate from the base value?

Before we present the main result of this section we provide a way of showing membership in ∃∗∀k -W[P] by means of Turing machines. In particular, we show that ∃∗∀k -W[P] contains those parameterized decision problems that can be decided by a certain class of alternating Turing machines.

An alternating Turing machine (ATM) with m tapes is a 6-tuple M = (S∃, S∀,Σ,∆, s0, F), where: S∃ and S∀ are disjoint sets; S = S∃ ∪ S∀ is the finite set of states; Σ is the alphabet; s0 ∈ S is the initial state; F ⊆ S is the set of accepting states; and ∆ ⊆ S × (Σ ∪ {$, □})m × S × (Σ ∪ {$})m × {L,R, S}m is the transition relation. We use the same notation as Flum and Grohe [Flum and Grohe, 2006, Appendix A.1]; for further details, we refer to their textbook.

We consider the following restrictions on ATMs. An ∃∀- Turing machine (or simply ∃∀-machine) is a 2-alternating ATM (S∃, S∀,Σ,∆, s0, F), where s0 ∈ S∃. Let P be a parameterized problem. An ∃∗∀k -W[P]-machine for P is a ∃∀- machine M such that there exists a computable function f and a polynomial p such that: (i) M decides P in time f(k)p(|x|); and (ii) for all instances (x, k) of P and each computation path R of M with input (x, k), at most f(k) log |x| of the universal configurations of R are nondeterministic. We say that a parameterized problem P is decided by some ∃∗∀k -W[P]- machine if there exists a ∃∗∀k -W[P]-machine for P.

Theorem7. If a parameterized problemQ is decided by some ∃∗∀k -W[P]-machine, then Q ∈ ∃∗∀k -W[P].

Proof (sketch). We describe a way of constructing, for each instance (x, k) of Q, an instance (ϕ, k′ ) of ∃∗∀k -WSAT(CIRC) that is a yes-instance if and only if (x, k) ∈ Q. Our construction is based on the proof of Cook's Theorem [Cook, 1971].

We begin with some observations. Let M be an ∃∗∀k -W[P]- machine for Q. We may assume without loss of generality that for any nondeterministic transition of M, there are exactly two possible ways of proceeding. Any run of M on input (x, k) can be specified entirely by indicating what nondeterministic choices Mmakes. Given (a representation of) these nondeterministic choices, determining whether this run of M is an accepting run can be done in fpt-time in (x, k) - simply by simulating M using the given choices. In other words, to decide whether M accepts an input (x, k), we need to decide whether there exists some sequence s1 of nondeterministic choices for the existential phase of the computation, such that for all sequences s2 of nondeterministic choices for the universal phase of the computation it holds that the run of M on (x, k) that is specified by (s1, s2) is an accepting run.

By definition of ∃∗∀k -W[P]-machines, we know that there is some computable function f and some constant c such that for each input (x, k) with |x| = n, (i) M runs in time f(k)nc and (ii) M makes at most f(k) log n nondeterministic choices in the universal phase of the computation. Therefore, in particular, in the existential phase of the computation Mmakes at most f(k)nc nondeterministic choices. We can encode all possibilities for the 2f(k)nc many different possible combinations of choices that M makes in the existential phase of the computation using f(k)nc many existential variables of ϕ. Moreover, since there are at most 2f(k) logn = nf(k) many different possible combinations of choices that Mmakes in the universal phase of the computation, we can encode these possibilities using n universal variables, whose assignments are restricted to set only k′ = f(k) many variables to true.

The circuit ϕ then simulates the behavior of M on input (x, k) with the nondeterministic behavior given by (s1, s2) as specified by the assignment to the variables. Since such a simulation can be done in fpt-time, we know we can encode this simulation in a circuit ϕ that can be constructed in fpttime. Then, (ϕ, k′ ) is a yes-instance of ∃∗∀k -WSAT(CIRC) if and only if M accepts (x, k), which is the case if and only if (x, k) ∈ Q.

The result for the other direction, i.e., if a parameterized problem Q ∈ ∃∗∀k -W[P] then Q is decided by some ∃∗∀k -W[P]-machine, is omitted due to space limitations. Now we are ready to present the main result of this section.

Theorem 8. The problem PLANNING[BOUNDED DEVIATION] is ∃∗∀k -W[P]-complete if the plan length k is bounded by a polynomial in the input size.

Proof. We describe an algorithm to solve the problem that can be implemented by an ∃∗∀k -W[P]-machine. The algorithm first guesses a sequence ω of m actions from A using m log |A| (binary) nondeterministic choices in the existential phase of the computation. Then, in the universal phase, it verifies whether this plan works for all cases where k of the unknown variables deviate from the base value in the initial state. Each such initial state can be specified using k log (|Vu| · |D|) nondeterministic choices (in the universal phase), and for any such initial state I, checking whether the ω reaches a goal state from I can be done in polynomial time. This algorithm is correct and can be implemented by an ∃∗∀k -W[P]-machine. Then, by Proposition 7, the result follows.

To show hardness, we reduce from ∃∗∀k -WSAT(CIRC). Intuitively, in the reduction, we will emulate the evaluation of the circuit by a planning problem. Here, the goal is to set the output gate to true and the unknown variables are used to model the universally quantified variables of the circuit. With help of the actions we sequentially evaluate the output of the gates in a fixed order to finally compute the value of the output gate of the circuit. Recall that an instance of ∃∗∀k -WSAT(CIRC) consists of a Boolean circuit C over two sets of disjoint input variables X and Y , and an integer k′ .

Since a circuit can be seen as an acyclic directed graph, we may assume that the gates g1, . . . , gm are numbered in such a way that for each gate gi, its inputs gj1 , . . . , gjℓ are numbered in such a way that j1, . . . , jℓ < i. This numbering gives a natural ordering of the gates, which ensures that all input values for a gate are already computed if the output value is to be determined. We create the set L = {l1, . . . , lm} of variables. Then we introduce a new variable f and the action af : {f = 0} → {f = 1}. Furthermore, for each variable x ∈ X, we create the action ax : {f = 0} → {x = 1}. For each gate gi, we create an action agi where:

Here Γgi depends on the type of gate gi and is obtained as follows. For each gate gi we introduce the variable o(gi), representing the unnegated output of gate gi. Let the unnegated input gates of gate g be g′1 , . . . , g′p , and the negated ones be g′′ 1 , . . . , g′′ l . To simplify the presentation, we assume that each variable in Y is also represented by a gate g, whose output is represented as o(g). If g is an AND-gate we define:

If g is an OR-gate, Γgi is defined analogously. Notice that the effect in the set Γgi are conditional. Intuitively, executing the actions ag1 , . . . , agm in order corresponds to evaluating the circuit using the given values for the variables in X and Y . Moreover, executing these actions is the only way to set o(go) to 1, where go is the output gate of C.

To put things together, we set V = X ∪ L ∪ {f} ∪ {o(g) | g is a gate in C}, Vu = Y , A = {af} ∪ {ax | x ∈ X} ∪ {ag | g is a gate in C}, I(v) = 0 for each v ∈ V , G = {o(go) = 1}, where go is the output gate of C, k = m+ |X|, and d = k′ . The correctness of this reduction can be checked straightforwardly.

9 Conclusion

For a variety of planning problems we have investigated the limits of a reduction-based approach to SAT. In particular, classes such as para-NP, para-DP, and FPT NP[f(k)] give hope for an efficient transformation to SAT (as long as the parameters are of moderate size). We believe that our results for different variants of planning provide a versatile toolbox for showing membership in these classes. This is desirable because planning is an expressive formalism that allows for easy encodings of other problems. Thus, our results help to explore the limits of efficient reducibility to SAT also for other important AI problems different to planning.

For future work we plan to extend this complexity map to other problems from different fields. It is also interesting to investigate how the performance of problems from different classes behaves in practice. Furthermore, it is desirable to find natural problems for the more exotic classes in this complexity landscape.