DunkP1: hρ e = ¬clog, Φ = {ϕ 0 = clog, ϕ 1 = inP1 =⇒ ¬arm}, Θ = {}i, DunkP2: hρ e = ¬clog, Φ = {ϕ 0 = clog, ϕ 1 = inP2 =⇒ ¬arm}, Θ = {}i, Flush: hρ e = ⊤, Φ = {ϕ 0 = ¬clog}, Θ = {}i, and DetectMetal: hρ e = ⊤, Φ = ∅, Θ = {o 0 = inP1, o 1 = ¬inP1}i.

## 2.1 Regression

We perform regression in the CAltAlt planner to find conformant plans by starting with the goal belief state and regressing it non-deterministically over all relevant actions. An action (without observations) is relevant for regressing a belief state if (i) its unconditional effect is consistent with every state in the belief state and (ii) at least one effect consequent contains a literal that is present in a constituent of the belief state. The first part of relevance requires that every state in the successor belief state is actually reachable from the predecessor belief state and the second ensures that the action helps support the successor.

Following Pednault (1988), regressing a belief state BS over an action a, with conditional effects, involves finding the execution, causation, and preservation formulas. We define regression in terms of clausal representation, but it can be generalized for arbitrary formulas. The regression of a belief state is a conjunction of the regression of clauses in κ(BS). Formally, the result BS′ of regressing the belief state BS over the action a is defined as:3

$$B S^{\prime}=\operatorname{\mathsf{Regress}}(B S,a)=\Pi(a)\land\left(\bigwedge_{C\in\kappa(B S)}\bigvee_{l\in C}(\Sigma(a,l)\wedge I P(a,l))\right)$$

Execution formula (Π(a)) is the execution precondition ρ e(a). This is what must hold in BS′for a to have been applicable.

Causation formula (Σ(**a, l**)) for a literal l w.r.t all effects ϕ i(a) of an action a is defined as the weakest formula that must hold in the state before a such that l holds in BS. The intuitive meaning is that l already held in BS′, or the antecedent ρ i(a) must have held in BS′to make l hold in BS.

Formally Σ(**a, l**) is defined as:

$$\Sigma(a,l)=l\vee\bigvee_{i:l\in\varepsilon^{i}(a)}\rho^{i}(a)$$

Preservation formula (IP(**a, l**)) of a literal l w.r.t. all effects ϕ i(a) of action a is defined as the formula that must be true before a such that l is not violated by any effect ε i(a). The intuitive meaning is that the antecedent of every effect that is inconsistent with l could not have held in BS′.

Formally IP(**a, l**) is defined as:

$$I P(a,l)=\bigwedge_{i:\neg l\in\varepsilon^{i}(a)}\neg\rho^{i}(a)$$

Regression has also been formalized in the MBP planner (Cimatti & Roveri, 2000) as a symbolic pre-image computation of BDDs (Bryant, 1986). While our formulation is syntactically different, both approaches compute the same result.