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 , regressing a belief state over an action , 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 . Formally, the result of regressing the belief state over the action is defined as:3
Execution formula ( ) is the execution precondition . This is what must hold in for to have been applicable.
Causation formula ( ) for a literal w.r.t all effects of an action is defined as the weakest formula that must hold in the state before such that holds in . The intuitive meaning is that already held in , or the antecedent must have held in to make hold in . Formally is defined as:
Preservation formula ( ) of a literal w.r.t. all effects of action is defined as the formula that must be true before such that is not violated by any effect . The intuitive meaning is that the antecedent of every effect that is inconsistent with could not have held in . Formally is defined as:
Regression has also been formalized in the MBP planner  as a symbolic pre-image computation of BDDs . While our formulation is syntactically different, both approaches compute the same result.