2 An example

Our running example in this section is the Blocks World problem, represented in the STRIPS subset of the planning domain definition language (PDDL) planning language (McDermott Reference Mcdermott1998). We follow the approach of the plasp system (Dimopoulos et al. Reference Dimopoulos, Gebser, Lühne, Romero, Schaub, Balduccini and Janhunen2017), which translates a PDDL description into a set of facts, combines these facts with a meta-encoding implementing the PDDL semantics, and solves the resulting program using the ASP solver clingo.

Our instance consists of three blocks, a, b, and c. Initially, a is on top of b, that is on top of c, that is on the table. The goal is to rearrange the blocks in reverse order. This is represented by the following set of facts:

There are four actions in the domain: pick_up(X) picks up a block X that is on the table, put_down(X) puts down a block X on the table, stack(X,Y) stacks the block X on top of block Y, and unstack(X,Y) undoes that operation. The following lines specify the action stack(X,Y) in terms of its preconditions, delete (or negative) effects and additive (or positive) effects – where ‘B’ is a shorthand for the body ‘block(X), block(Y)’:

The specification of the rest of the actions is available in the supplementary material.

The following meta-encoding gives meaning to the previous rules:

Line 1 specifies which fluents F hold at time step 0, Line 2 generates one action A per time step T between 1 and some constant n, Line 3 forbids the occurrence of an action A if some of its preconditions do not hold, Line 4 defines the positive effects of an action A, Lines 5-6 define inertia for all fluents F, and Line 7 enforces that every goal fluent F holds at the last time point n.

The shortest plan for this problem requires six actions, one to pick-up or unstack every block, and another to put it down or stack it. Accordingly, when the constant n has the value 6, our program has a unique stable model that includes the atoms occ(unstack(a,b),1), occ(put_down(a),2), occ(unstack(b,c),3), occ(stack(b,a),4), occ(pick_ up(c),5), and occ(stack(c,b),6).

Such a stable model can be computed by the ASP solver clingo, that is based in the ground-and-solve approach to ASP solving. In the first step, clingo grounds the logic program by replacing the rules with variables with their ground (variable-free) instantiations. The goal of this step is to generate a ground program that is as compact as possible, while preserving the stable models of the original program. As an example, consider the precondition rule in Line 3 of the meta-encoding for action stack(b,a). At time point 2, clingo generates two ground instances, one for each precondition of the action:

:- occ(stack(b,a),2), not holds( clear(a),1).

:- occ(stack(b,a),2), not holds(holding(b),1).

At time point 1, however, the corresponding first instance is not generated, as clingo infers that holds(clear(a),0) must be true due to the fact init(clear(a)) and the rule in Line 1. In turn, the corresponding second instance is simplified to

:- occ(stack(b,a),1).

since clingo deduces that holds(holding(b),0) cannot be true, as no rule in the program can derive it.

In the second step, clingo uses a Conflict-Driven Nogood Learning (CDNL) algorithm to search for stable models of the ground program generated before. Whenever the algorithm backtracks, it learns a new constraint, also called a nogood, that is satisfied by all stable models. These learned constraints are crucial for the performance of the solver, as they prevent it from making the same mistakes more than once. We explain this in more detail in Section 3. As an example, while solving our program, clingo could learn the constraint

(1) \begin{align} {\texttt {:- holds(on(a,b),2), holds(on(b,c),2), not holds(on(b,c),4).}} \end{align}

representing that if at time point 2 block a is on top of block b, and b is on top of block c, then at time point 4 block b must remain on top of c. Note that although the constraint is specific to time points 2 and 4, the solver learned it using rules that are replicated at every time point. Then, the main question of this paper is:

• Can we generalize such learned constraints to other time points?

And if so:

• What impact does this have on the performance of ASP solvers?

We can generalize (1) to all time steps in the interval 0..n with the following constraint:

(2) \begin{align} {\texttt {:- }}& {\texttt {holds(on(a,b),T-2), holds(on(b,c),T-2),}}\\ & {\texttt {not holds(on(b,c),T), T=2..n.}}\nonumber \end{align}

This constraint can be safely added to our program, since it does not eliminate any of its stable models. Ideally, the solver could detect this automatically and learn this generalized constraint directly instead of (1). This could help it to prune the search space and find solutions faster. However, such generalization is not always easy, for two main reasons.

The first reason is that, as we have seen, clingo does not replicate exactly the same ground rules at every time point. Since the constraints learned by the solver depend on these ground rules, a constraint learned at one time step may not apply to others. For example, the solver can learn

(3) \begin{align} {\texttt {:- not holds(on(b,c),2).}} \end{align}

which corresponds to constraint (1) for step 2, without the atoms holds(on(a,b),0) and holds(on(b,c),0). During grounding, clingo infers that these atoms are true and simplifies the ground rules where they appear accordingly. As a result, the constraints learned from these simplified rules are also simpler – compare (3) with (1). Since these simplifications are not correct for all time points, the generalization of (3) to all time points

:- not holds(on(b,c),T), T = 0..n.

is also not correct. In fact, it would eliminate all stable models.

We address this issue manually, modifying the meta-encoding in such a way that the ground rules are truly the same for all time steps. We achieve this by replacing the rule in Line 1 by the choice rules

{ holds(F,0) } :- init(F).

{ holds(F,0) } :- add(A,F).

that generate all possible initial states, and by eliminating the integrity constraint of Line 8. Once this is done, the ground instantiations at all time steps become the same. For example, the ground instantiation of the rule in Line 3 for action stack(b,a) at time point 1 becomes

:- occ(stack(b,a),1), not holds( clear(a),0).

:- occ(stack(b,a),1), not holds(holding(b),0).

and instead of learning (3), clingo would learn the constraint

(4) \begin{align} {\texttt {:- holds(on(a,b),0), holds(on(b,c),0), not holds(on(b,c),2).}} \end{align}

that can be safely generalized to (2). Observe that the modified program no longer determines the values of the fluents at the initial and final situations. Instead, these values are specified by passing to clingo an additional set of so-called assumptions. Notably, these assumptions preserve the stable models of the original program but do not interfere with the grounding process. Hence, the ground rules remain the same across all time steps.

We formalize this approach in Section 4 using temporal logic problems, which consist of temporal logic programs defining the ground rules that are replicated at each time step, and partial assignments representing the initial and final states. Additionally, we study the temporal nogoods associated with temporal logic programs. Solving with assumptions is introduced in Section 3, while its application to temporal logic problems is described in Section 5.

To illustrate the second issue, let us extend our example by introducing a counter that is incremented with each action. We modify Line 4 of the meta-encoding to represent conditional effects of actions as follows:

\begin{align*} {\texttt {holds(F,T) :- occ(A,T), add(A,F), holds(G,T-1) : cond(A,F,G).}} \end{align*}

The atom cond(A,F,G) expresses that for action A to produce effect F, the fluent G must have been true in the previous state. The counter can be represented as a conditional effect of all actions:

add(A,counter(1)) :- action(A).

cond(A,counter(T),counter(T-1)) :- action(A), T = 2..m.

Actions make counter(1) true, and for T between 2 and m, they also make counter(T) true if counter(T-1) was true in the previous state. Given this extension, clingo can learn the constraint

(5) \begin{align} {\texttt {:- not holds(counter(2),2).}} \end{align}

as counter(2) always holds at time point 2 in all stable models. However, the generalization to all time points

(6) \begin{align} {\texttt {:- not holds(counter(2),T), T=0..n.}} \end{align}

would be incorrect, as counter(2) does not have to hold at time points 0 or 1. This example shows that, even when all rules are replicated across all time steps, we cannot always generalize learned constraints to all time steps. This raises the question: when can we generalize learned constraints to other – or all – time steps?

We provide a first answer in Section 5, after formalizing the problem of generalizing learned constraints. Assume that the time steps of the rules used to learn a constraint are known. This information allows us to to determine the time steps to which a learned constraint can we generalized. For instance, if constraint (5) — about fluent counter(2) at step 2 — was learned using rules from time steps 1 and 2, we could generalize it to the interval T = 2..n, because the rules used at 1 and 2 have corresponding copies at T-1 and T:

(7) \begin{align} {\texttt {:- not holds(counter(2),T), T=2..n.}} \end{align}

However, we could not generalize the constraint to T = 1, as no copies of the rules exist for time step 0. As another example, if (5) was learned using rules of steps 2 and 3, then the generalized constraint would apply to the interval T = 1..n-1, as the rules at 2 and 3 would have their corresponding copies at T and T + 1, and there are no copies at n + 1. Clearly, a drawback of this approach is that it requires tracking the time steps of the rules used to learn each constraint. Consequently, its implementation would require the modification of the inner machinery of clingo.

To avoid this, in Section 6 we investigate under which conditions can we generalize learned constraints to all time steps. In our previous examples, we could not generalize (5) to (6) because there were no copies of the rules at step 0 or step n + 1. But what would happen if the program behaved as if those copies existed? It turns out that in such a case we could generalize the learned nogoods to all time steps. How can we capture these cases? We define for each temporal program a transition graph whose edges correspond to the transitions between states. If every initial state has a predecessor in that graph, it is as if the rule copies applied also to those initial states. Likewise, if every state reachable from an initial state has a successor, it is as if the rule copies applied to those final states as well. In Section 6 we define temporal programs as internal if their transition graph satisfies these properties, and we show that for internal programs all learned nogoods can be generalized to all time steps.

In practice, most planning representations that we have encountered are either internal or can be easily adapted to become internal. For instance, to adapt our meta-encoding, it is sufficient to modify Line 2 by replacing the comparison operator = by <=, allowing the non-execution of actions at any time step. The inertia rule in Lines 5-6 ensures that fluents persist whenever no action occurs. Thus, initial states, where no action occurs, have themselves as predecessors. Similarly, reachable states have a successor state where no action occurs and all fluents persist. This small adjustment makes the representation internal. Once it is applied, constraint (5) can no longer be learned, as it does not hold in all stable models, that is there are stable models where no action occurs at time steps 1 or 2, and counter(2) does not hold at 2. Instead, the solver can learn the following constraint:

:- not holds(counter(2),2), occ(unstack(a,b),1),

occ(putdown(a),2).

which can be safely generalized to

:- not holds(counter(2),T), occ(unstack(a,b),T-1),

occ(putdown(a),T), T = 1..n.

We consider this constraint, with T = 1..n, a generalization across all time steps because its ground instances include atoms over all steps. In this case, extending the generalization to additional steps would be pointless. For other constraints, it could even be incorrect due to the semantics of negation.

To handle cases where a temporal representation is not internal, in Section 7 we introduce a translation that transforms any temporal program into an internal one. In our example, the translation adds the following rules:

Additionally, the translation inserts the atom lambda(T) into the body of each rule in the meta-encoding, and assumes that lambda is false at time step 0. This translation ensures that initial states – where lambda is false – have themselves as predecessors, and reachable states have themselves – after erasing lambda – as successors. Once this translation is applied, clingo, instead of learning constraint (5), could learn

\begin{align*} {\texttt {:- not holds(counter(2),2), lambda(2), lambda(1).}} \end{align*}

that could be generalized to

(8) \begin{align} {\texttt {:- not holds(counter(2),T), lambda(T), lambda(T-1), T=1..n.}} \end{align}

Furthermore, the constraints learned using the translation can be applied to the original program, after simplifying away the atoms over lambda and adapting the interval of T to T = 2..n. In our example, (8) can be simplified to (7), that can be safely added to our original program.

3 Background

We review the material from (Gebser et al. Reference Gebser, Kaufmann, Neumann, Schaub and Veloso2007) about solving normal logic programs and adapt it for our purposes to cover normal logic programs with choice rules and integrity constraints over some set $\mathcal {A}$ of atoms.

A rule $r$ has the form $H \leftarrow B$ where $B$ is a set of literals over $\mathcal {A}$ , and $H$ is either an atom $a \in \mathcal {A}$ , and we call $r$ a normal rule, or $\{a\}$ for some atom $a \in \mathcal {A}$ , making $r$ a choice rule, or $\bot$ , so that $r$ is an integrity constraint. We usually drop braces from rule bodies $B$ and drop the arrow $\leftarrow$ when $B$ is empty. We use the extended choice rule $\{a_1; \ldots ; a_n\}\leftarrow B$ as a shorthand for the choice rules $\{a_1\}\leftarrow B$ , …, $\{a_n\}\leftarrow B$ , and for some set of atoms $X \subseteq \mathcal {A}$ we denote by $\mathit {Choice}(X)$ the set of choice rules $\{ \{ a \} \leftarrow \mid a \in X \}$ . A program $\Pi$ is a set of rules. By $\Pi ^{n}$ , $\Pi ^{c}$ , and $\Pi ^{i}$ we denote its normal rules, choice rules and integrity constraints, respectively. Semantically, a logic program induces a collection of stable models, which are distinguished models of the program determined by the stable models semantics (see Gebser et al. Reference Gebser, Kaminski, Kaufmann and Schaub2012 and Gelfond and Lifschitz 1988 for details).

For a rule $r$ of the form $H \leftarrow B$ , let ${\mathit {h}(r)}=a$ be the head of $r$ if $H$ has the form $a$ or $\{a\}$ for some atom $a \in \mathcal {A}$ , and let ${\mathit {h}(r)}=\bot$ otherwise. Let $ {\mathit {Bd}(r)}=B$ be the body of $r$ , $ {{{\mathit {Bd}(r)}}^+}=\{a \mid a \in \mathcal {A}, a \in B\}$ be the positive body of $r$ , and $ {{{\mathit {Bd}(r)}}^-}=\{a \mid a \in \mathcal {A}, \neg a \in B\}$ be the negative body of $r$ . The set of atoms occurring in a rule $r$ and in a logic program $\Pi$ are denoted by $\mathit {At}{r}$ and $\mathit {At}{\Pi }$ , respectively. The set of bodies in $\Pi$ is ${\mathit {Bd}(\Pi )} = \{{\mathit {Bd}(r)}\mid r\in \Pi \}$ . For regrouping rule bodies sharing the same head $a$ , we define $ {\mathit {Bd}(a)}=\{{\mathit {Bd}(r)}\mid r\in \Pi, {\mathit {h}(r)}=a\}$ , and by ${\mathit {Bd}^{n}}(a)$ we denote the restriction of that set to bodies of normal rules, that is $ \{{\mathit {Bd}(r)}\mid r\in {\Pi ^{n}},{\mathit {h}(r)}=a\}$ .

A Boolean assignment $S$ over a set $\mathcal {D}$ , called the domain of $S$ , is a set $\{\sigma _1,\ldots, \sigma _n\}$ of signed literals $\sigma _i$ of the form ${\mathbf {T}} a$ or ${\mathbf {F}} a$ for some $a\in \mathcal {D}$ and $1 \leq i \leq n$ ; ${\mathbf {T}} a$ expresses that $a$ is true and ${\mathbf {F}} a$ that it is false. We omit the attribute signed for literals whenever clear from the context. We denote the complement of a literal $\sigma$ by $\overline {\sigma }$ , that is, $\overline {{{\mathbf {T}} a}} = {{\mathbf {F}} a}$ and $\overline {{{\mathbf {F}} a}} = {{\mathbf {T}} a}$ . Given this, we access true and false propositions in $S$ via $ {S^{{\mathbf {T}}}} = \{a \in \mathcal {D} \mid {{\mathbf {T}} a} \in S\}$ and $ {S^{{\mathbf {F}}}} = \{a \in \mathcal {D} \mid {{\mathbf {F}} a} \in S\}$ . We say that a set of atoms $X$ is consistent with an assignment $S$ if ${S^{{\mathbf {T}}}}\subseteq X$ and ${S^{{\mathbf {F}}}}\cap X = \emptyset$ . In our setting, a nogood is a set $\{\sigma _1,\ldots, \sigma _n\}$ of signed literals, expressing a constraint violated by any assignment containing $\sigma _1,\ldots, \sigma _n$ . Accordingly, the nogood for a body $B$ , denoted by $\mathit {ng}(B)$ , is $\{{ {\mathbf {T}} a} \mid a \in B^{+}\}\cup \{{{\mathbf {F}} a} \mid a \in B^{-}\}$ . We say that an assignment $S$ over $\mathcal {D}$ is total if ${S^{{\mathbf {T}}}} \cup {S^{{\mathbf {F}}}} = \mathcal {D}$ and ${S^{{\mathbf {T}}}} \cap {S^{{\mathbf {F}}}} = \emptyset$ . A total assignment $S$ over $\mathcal {D}$ is a solution for a set $\Delta$ of nogoods, if $\delta \not \subseteq S$ for all $\delta \in \Delta$ . A set $\Delta$ of nogoods entails a nogood $\delta$ if $\delta \not \subseteq S$ for all solutions $S$ over $\mathcal {D}$ for $\Delta$ , and it entails a set of nogoods $\nabla$ if it entails every nogood $\delta \in \nabla$ in the set.

We say that a nogood $\delta$ is a resolvent of a set of nogoods $\Delta$ if there is a sequence of nogoods $\delta _1, \ldots, \delta _n$ with $n \geq 1$ such that $\delta _n=\delta$ , and for all $i$ such that $1 \leq i \leq n$ , either $\delta _i \in \Delta$ , or there are some $\delta _j$ , $\delta _k$ with $1\leq j \lt k \lt i$ such that $\delta _i=(\delta _j\setminus \{\sigma \})\cup (\delta _k\setminus \{\overline {\sigma }\})$ for some signed literal $\sigma$ . In this case, we say that the sequence $\delta _1, \ldots, \delta _n$ is a proof of $\delta _n$ . We say that a signed literal $\sigma$ is unit resulting for a nogood $\delta$ and an assignment $S$ if $\delta \setminus S = \{\sigma \}$ and $\overline {\sigma }\notin S$ . For a set of nogoods $\Delta$ and an assignment $S$ , unit propagation is the process of extending $S$ with unit-resulting literals until no further literal is unit resulting for any nogood in $\Delta$ .

Inferences in ASP can be expressed in terms of atoms and rule bodies. We begin with nogoods capturing inferences from the Clark completion. For a body $B=\{a_1,\ldots, a_m,\neg a_{m+1},\ldots, \neg a_n\}$ , we have that $ {\delta (B)} \! = \! \{{{\mathbf {F}} B},{{\mathbf {T}} a_1},\ldots, {{\mathbf {T}} a_m},{{\mathbf {F}} a_{m+1}},\ldots, $ ${{\mathbf {F}} a_n}\}$ and $ {\Delta (B)} = \{ \, \{{{\mathbf {T}} B},{{\mathbf {F}} a_1}\}, \ldots, $ $ \{{{\mathbf {T}} B},{{\mathbf {F}} a_m}\}, \{{{\mathbf {T}} B},{{\mathbf {T}} a_{m+1}}\}, \ldots, \{{{\mathbf {T}} B},$ ${{\mathbf {T}} a_n}\} \, \}.$ For an atom $a$ such that ${{\mathit {Bd}^{n}}(a)}=\{B_1,\ldots, $ $B_k\}$ , we have that $ {\Delta (a)} = \{\,\{{{\mathbf {F}} a},{{\mathbf {T}} B_1}\},\ldots, $ $ \{{{\mathbf {F}} a},{{\mathbf {T}} B_k}\}\,\},$ and if ${\mathit {Bd}(a)}=\{B_1,\ldots, B_k\}$ then $ {\delta (a)} = \{{{\mathbf {T}} a},{{\mathbf {F}} B_1},\ldots, {{\mathbf {F}} B_k}\}.$ Given this, the completion nogoods of a logic program $\Pi$ are defined as follows:

\begin{equation*} \begin{array}{l@{}c@{}l} \Delta _\Pi & \,=\, & \{{\delta (B)} \mid B\in {\mathit {Bd}({\Pi }\setminus {\Pi ^{i}})}\} \cup \{\delta \in {\Delta (B)}\mid B\in {\mathit {Bd}({\Pi }\setminus {{\Pi ^{i}}})}\} \\[2pt] & \cup & \{{\delta (a)} \mid a\in {\mathit {At}{\Pi }}\} \cup \{\delta \in {\Delta (a)} \mid a\in {\mathit {At}{\Pi }}\} \\[2pt] & \cup & \{{\mathit {ng}(B)} \mid B\in {\mathit {Bd}({\Pi ^{i}})}\} \end{array} \end{equation*}

Choice rules of the form $\{a\} \leftarrow B$ are considered by not adding the corresponding nogood $\{{{\mathbf {F}} a}, {{\mathbf {T}} B}\}$ to $\Delta (a)$ , and integrity constraints from $\Pi ^{i}$ of the form $\bot \leftarrow B$ are considered by adding directly their corresponding nogood $\mathit {ng}(B)$ . The definition of the loop nogoods $\Lambda _\Pi$ , capturing the inferences from loop formulas, is the same as in (Gebser et al. Reference Gebser, Kaufmann, Neumann, Schaub and Veloso2007). We do not specify them here since they do not pose any special challenge to our approach, and they are not needed in our (tight) examples.

To simplify the presentation, we slightly deviate from (Gebser et al. Reference Gebser, Kaufmann, Neumann, Schaub and Veloso2007) and consider a version of the nogoods of a logic program where the occurrences of the empty body are simplified. Note that ${\delta (\emptyset )}=\{{{\mathbf {F}} \emptyset }\}$ and ${\Delta (\emptyset )}=\emptyset$ . Hence, if $\emptyset \in {\mathit {Bd}(\Pi )}$ then any solution to the completion and loop nogoods of $\Pi$ must contain ${\mathbf {T}} \emptyset$ . Based on this, we can delete from $\Delta _\Pi \cup \Lambda _\Pi$ the nogoods that contain ${\mathbf {F}} \emptyset$ and eliminate the occurrences of ${\mathbf {T}} \emptyset$ from the others. Formally, we define the set of (simplified) nogoods for $\Pi$ as:

\begin{equation*} \Sigma _\Pi = \{\delta \setminus \{{{\mathbf {T}} \emptyset }\} \mid \delta \in \Delta _\Pi \cup \Lambda _\Pi, {{\mathbf {F}} \emptyset } \notin \delta \}. \end{equation*}

To accommodate this change, for a program $\Pi$ , we fix the domain $\mathcal {D}$ of the assignments to the set ${\mathit {At}{\Pi }}\cup ({\mathit {Bd}(\Pi )}\setminus \emptyset )$ . Given this, the stable models of a logic program $\Pi$ can be characterized by the nogoods $\Sigma _{\Pi }$ for that program. This is made precise by the following theorem, which is an adaptation of Theorem 3.4 from (Gebser et al. Reference Gebser, Kaufmann, Neumann, Schaub and Veloso2007) to our setting.

To compute the stable models of a logic program $\Pi$ , we apply the algorithm ${\mathit {CDNL}\text {-}\mathit {ASP}}(\Pi )$ from (Gebser et al. Reference Gebser, Kaufmann, Neumann, Schaub and Veloso2007) implemented in the ASP solver clingo. The algorithm searches for a solution $S$ to the set of nogoods $\Sigma _\Pi$ , and when it finds one it returns the corresponding set of atoms ${S^{{\mathbf {T}}}}\cap {\mathit {At}{\Pi }}$ . $\mathit {CDNL}\text {-}\mathit {ASP}$ maintains a current assignment $S$ and a current set of learned nogoods $\nabla$ , both initially empty. The main loop of the algorithm starts by applying unit propagation to $\Sigma _{\Pi }\cup \nabla$ , possibly extending $S$ . Every derived literal is “implied” by some nogood $\delta \in \Sigma _{\Pi }\cup \nabla$ , which is stored in association with the derived literal. This derivation may lead to the violation of another nogood. This situation is called conflict. If propagation finishes without conflict, then a (heuristically chosen) literal can be added to $S$ , provided that $S$ is partial, while otherwise $S$ represents a solution and can be directly returned. On the other hand, if there is a conflict, there are two possibilities. Either it is a top-level conflict, independent of heuristically chosen literals, in which case the algorithm returns unsatisfiable. Or, if that is not the case, the conflict is analyzed to calculate a conflict nogood $\delta$ , that is added to $\nabla$ . More in detail, $\delta$ is a resolvent of the set of nogoods associated with the literals derived after the last heuristic choice. Hence, every learned nogood $\delta$ added to $\nabla$ is a resolvent of $\Sigma _{\Pi }\cup \nabla$ and, by induction, it is also a resolvent of $\Sigma _{\Pi }$ . After recording $\delta$ , the algorithm backjumps to the earliest stage where the complement of some formerly assigned literal is implied by $\delta$ , thus triggering propagation and starting the loop again.

This algorithm has been extended for solving under assumptions (Eén and Sörensson Reference Eén and Sörensson2003). In this setting, the procedure ${\mathit {CDNL}\text {-}\mathit {ASP}}(\Pi, S)$ receives additionally as input a partial assignment $S$ over $\mathit {At}{\Pi }$ , the so-called assumptions, and returns some stable model of $\Pi$ that is consistent with $S$ . To accommodate this extension, the algorithm simply decides first on the literals from $S$ , and returns unsatisfiable as soon as any of these literals is undone by backjumping. No more changes are needed. Notably, the learned nogoods are still resolvents of $\Delta _{\Pi }$ , that are independent of the set of assumptions $S$ .

4 Temporal programs, problems and nogoods

We introduce a simple language of temporal logic programs to represent temporal problems. These programs represent the dynamics of a temporal domain by referring to two time steps: the current step and the previous step. We refer to the former by atoms from a given set $\mathcal {A}$ , and to the latter by atoms from the set ${\mathcal {A}'}=\{ {a'} \mid a \in \mathcal {A}\}$ , that we assume to be disjoint from $\mathcal {A}$ . We define a state as a subset of $\mathcal {A}$ . Following the common-sense flow of time, normal or choice rules define the atoms of the current step in terms of the atoms of both the current and the previous step. Integrity constraints forbid some states, possibly depending on their previous state. Syntactically, a temporal logic program $\Pi$ over $\mathcal {A}$ has the form of a (non-temporal) logic program over $\mathcal {A}\cup {\mathcal {A}'}$ such that for every rule $r \in \Pi$ , if $r \in {\Pi ^{n}}\cup {\Pi ^{c}}$ then ${\mathit {h}(r)}\in \mathcal {A}$ , and otherwise $({{{\mathit {Bd}(r)}}^+}\cup {{{\mathit {Bd}(r)}}^-})\cap \mathcal {A}\neq \emptyset$ . Given that temporal logic programs over $\mathcal {A}$ can also be seen as (non-temporal) logic programs over $\mathcal {A}\cup {\mathcal {A}'}$ , in what follows we may apply the notation of the latter to the former.

This language is designed to capture the core of the translations to ASP of action and temporal languages. For instance, in our introductory PDDL example (McDermott Reference Mcdermott1998), a temporal logic program can represent the transition between T-1 and T defined by the rules in Lines 2-6 of the meta-encoding. In essence, this temporal program corresponds to the ground instantiation of those rules at a single time point. Temporal programs are also closely related to the present-centered programs used in the implementation of the temporal ASP solver telingo (Cabalar et al. Reference Cabalar, Kaminski, Morkisch, Schaub, Balduccini, Lierler and Woltran2019), or to the programs that define the transitions in action languages (Lee et al. Reference Lee, Lifschitz, Yang and Rossi2013).

Example 1. Our running example is the temporal logic program $\Pi _1$ over $\mathcal {A}_1=\{a,b,c,$ $d\}$ that consists only of choice rules and integrity constraints:

Temporal logic programs $\Pi$ can be instantiated to specific time intervals. We introduce some notation for that. Let $m$ and $n$ be integers such that $1 \leq m \leq n$ , and $[m,n]$ denote the set of integers $\{ i \mid m \leq i \leq n\}$ . For $a \in \mathcal {A}$ , the symbol $a[m]$ denotes the atom $a_m$ , and for ${a'} \in \mathcal {A}'$ , the symbol a’[m] denotes the atom $a_{m-1}$ . For a set of atoms $X\subseteq \mathcal {A}\cup {\mathcal {A}'}$ , $X[m]$ denotes the set of atoms $\{ {a[m]} \mid a \in X\}$ , and $X{[m,n]}$ denotes the set of atoms $\{{a[i]}\mid p \in X, i \in [m,n]\}$ . For a rule $r$ over $\mathcal {A}\cup \mathcal {A}'$ , the symbol $r[m]$ denotes the rule that results from replacing in $r$ every atom $a \in \mathcal {A}\cup \mathcal {A}'$ by $a[m]$ , and $r{[m,n]}$ denotes the set of rules $\{{r[i]} \mid i \in [m,n]\}$ . Finally, for a temporal program $\Pi$ , $\Pi [m]$ is $\{ {r[m]} \mid r \in \Pi \}$ , and $\Pi {[m,n]}$ is $\{ {\Pi [i]} \mid i \in [m,n] \}$ .

Example 2. The instantiation of $\Pi _1$ at $1$ , denoted by $\Pi _1[1]$ , is

The programs $\Pi _1[i]$ for $i \in \{2,3,4\}$ are the same, except that the subindex $1$ is replaced by $i$ , and the subindex $0$ is replaced by $i-1$ . The instantiation of $\Pi _1$ at $[1,4]$ , denoted by $\Pi _1{[1,4]}$ , is ${\Pi _1[1]}\cup {\Pi _1[2]}\cup {\Pi _1[3]}\cup {\Pi _1[4]}$ .

To represent temporal reasoning problems, temporal programs are complemented by assignments $I$ and $F$ that partially or completely describe the initial and the final state of a problem. Formally, a temporal logic problem over some set of atoms $\mathcal {A}$ is a tuple $({\Pi, I,F})$ where $\Pi$ is a temporal logic program over $\mathcal {A}$ , and $I$ and $F$ are assignments over $\mathcal {A}$ . A solution to such a problem is a sequence of states that is consistent with the dynamics described by $\Pi$ and with the information provided by $I$ and $F$ . The possible sequences of states of length $n$ , for some integer $n\geq 1$ , are represented by the generator program for $\Pi$ and $n$ , denoted by $\mathit {gen}(\Pi, n)$ , that consists of the rules:

\begin{equation*}{{\mathit {Choice}(\mathcal {A})}[0]} \cup {\Pi {[1,n]}}.\end{equation*}

A solution to a temporal problem $({\Pi, I,F})$ is defined as a pair $(X,n)$ , where $n$ is an integer such that $n\geq 1$ and $X$ is a stable model of $\mathit {gen}(\Pi, n)$ consistent with ${I[0]}\cup {F[n]}$ .

Temporal problems can be used to formalize planning problems, using a temporal logic program $\Pi$ of the form described above, a total assignment $I$ that assigns a value to every possible atom (action occurrences are made false initially), and a partial assignment $F$ to fix the goal. The solutions of the temporal problem correspond to the plans of the planning problem.

To pave the way to the nogood characterization of temporal logic problems, we define the transition program $\mathit {trans}(\Pi )$ of a temporal logic program $\Pi$ as the (non-temporal) logic program ${\mathit {Choice}({A'})}\cup \Pi$ over $\mathcal {A}\cup {\mathcal {A}'}$ . Each stable model of this program represents a possible transition between a previous and a current step, where the former is selected by the additional choice rules over atoms from $\mathcal {A}'$ , and the latter is determined by the rules of $\Pi$ , interpreted as non-temporal rules.

Next, we introduce temporal nogoods and their instantiation. Given a temporal logic program $\Pi$ over $\mathcal {A}$ , a temporal nogood over $\mathcal {A} \cup {\mathit {Bd}(\Pi )}$ has the form of a (non-temporal) nogood over $\mathcal {A} \cup {\mathcal {A}'} \cup {\mathit {Bd}(\Pi )}$ . For a temporal nogood $\delta$ over $\mathcal {A} \cup {\mathit {Bd}(\Pi )}$ and an integer $n\geq 1$ , the instantiation of $\delta$ at $n$ , denoted by $\delta [n]$ , is the nogood that results from replacing in $\delta$ any signed literal ${\mathbf {T}} \alpha$ ( ${\mathbf {F}} \alpha$ ) by ${\mathbf {T}} {\alpha [n]}$ (by ${\mathbf {F}} {\alpha [n]}$ , respectively). We extend this notation to sets of nogoods and to intervals like we did above. For example, $\delta _1=\{{{\mathbf {F}} b'},{{\mathbf {T}} b}\}$ is a temporal nogood over $\mathcal {A}_1\cup {\mathit {Bd}(\Pi _1)}$ , and $\delta _1{[1,2]}$ is $\big \{ \{{{\mathbf {F}} {b_0}},{{\mathbf {T}} {b_1}}\}, \{{{\mathbf {F}} {b_1}},{{\mathbf {T}} {b_2}}\} \big \}$ . By $\mathit {step}(\delta )$ we denote the steps of the literals occurring in $\delta$ , that is ${\mathit {step}(\delta )} = \{i \mid {{\mathbf {T}} {p_i}}\in \delta \text { or }{{\mathbf {F}} {p_i}}\in \delta \}$ . For example, ${\mathit {step}(\{{{\mathbf {F}} {b_0}},{{\mathbf {F}} {b_1}},{{\mathbf {T}} {b_2}}\})}=\{0,1,2\}$ .

We are now ready to define the temporal nogoods for a temporal logic program $\Pi$ over $\mathcal {A}$ . Recall that $\mathit {trans}(\Pi )$ is a (non-temporal) logic program over $\mathcal {A}\cup {\mathcal {A}'}$ , whose corresponding nogoods are denoted by $\Sigma _{{\mathit {trans}(\Pi )}}$ . Then, the set of temporal nogoods for $\Pi$ , denoted by $\Psi _{\Pi }$ , has the form $\Sigma _{{\mathit {trans}(\Pi )}}$ , interpreted as a set of temporal nogoods over $\mathcal {A}\cup {\mathit {Bd}(\Pi )}$ , and not as a set of (non-temporal) nogoods over $\mathcal {A}\cup {\mathcal {A}'}\cup {\mathit {Bd}(\Pi )}$ .

Temporal nogoods provide an alternative characterization of the nogoods of $\mathit {gen}(\Pi, n)$ .

In words, the nogoods for $\mathit {gen}(\Pi, n)$ are the same as the instantiation of the temporal nogoods for $\Pi$ , that are nothing else than the nogoods of the logic program $\mathit {trans}(\Pi )$ interpreted as temporal nogoods.

By Theorem1, the temporal nogoods can be used to characterize the solutions of temporal logic problems.

5 Generalization of learned constraints

A common software architecture to solve a temporal problem $({\Pi, I,F})$ combines a scheduler that assigns resources to different values of $n$ , with one or many solvers that look for solutions of the assigned lengths $n$ (see (Rintanen et al. Reference Rintanen, Heljanko and Niemelä2006). The standard approach for the solvers is to extend the program $\mathit {gen}(\Pi, n)$ with facts and integrity constraints to adequately represent $I$ and $F$ and call the procedure $\mathit {CDNL}\text {-}\mathit {ASP}$ with this extended program without assumptions. However, as we have seen in our introductory example, this method does not work well for our purposes, because it leads to a nogood representation of the initial and the final steps that is different from the nogood representation of the other steps. Hence, the constraints learned using nogoods specific to the initial and final steps may not be generalizable to the other steps. To overcome this issue, in our approach the solvers apply the procedure ${\mathit {CDNL}\text {-}\mathit {ASP}}({\mathit {gen}(\Pi, n)},$ ${I[0]}\cup {F[n]})$ to the generator program for $\Pi$ and $n$ , using assumptions to fix the assignments about the initial and final situations. Observe that in this case, by Proposition1, the solver initially contains exactly the nogoods $\Psi _{\Pi }{[1,n]}$ , and all the nogoods that it learns afterward are resolvents of $\Psi _{\Pi }{[1,n]}$ .

Once this is settled, we ask ourselves:

• What generalizations of the nogoods learned by $\mathit {CDNL}\text {-}\mathit {ASP}$ can be applied to the same or other problems?

We make the question more precise step by step. First, instead of talking about “the nogoods learned by the algorithm”, we refer to the resolvents of $\Psi _{\Pi }{[1,n]}$ for some temporal problem $({\Pi, I,F})$ . Or more precisely, we refer to the resolvents of $\Psi _{\Pi }{[i,j]}$ for some $i$ and $j$ such that $1 \leq i \leq j \leq n$ , since the learned nogoods are always the result of resolving nogoods belonging to some interval $[i,j]$ that may be smaller than $[1,n]$ .

To formalize the notion of the “generalizations of nogoods”, we introduce some notation for shifting a non-temporal nogood an amount of $t$ time steps. For integers $n\geq 1$ and $t$ , and a non-temporal nogood $\delta$ over $(\mathcal {A} \cup \mathcal {A}' \cup {\mathit {Bd}(\Pi )}){[1,n]}$ , the symbol ${\delta }\langle {t}\rangle$ denotes the nogood that results from replacing in $\delta$ any signed literal ${{\mathbf {T}} \alpha }_m$ $({{{\mathbf {F}} \alpha }_m})$ by ${{\mathbf {T}} \alpha }_{m+t}$ (by ${{\mathbf {F}} \alpha }_{m+t}$ , respectively). For example, ${{\delta }\langle {0}\rangle }=\delta$ , and if $\delta =\{{{\mathbf {T}} {a_2}},{{\mathbf {F}} {b_3}}\}$ , then ${\delta }\langle {1}\rangle$ is $\{{{\mathbf {T}} {a_3}},{{\mathbf {F}} {b_4}}\}$ , and ${\delta }\langle {-1}\rangle$ is $\{{{\mathbf {T}} {a_1}},{{\mathbf {F}} {b_2}}\}$ . We say that ${\delta }\langle {t}\rangle$ is a shifted version of the nogood $\delta$ , and that a generalization of a nogood is a set of some of its shifted versions. For example, $\{\{{{\mathbf {T}} {a_2}},{{\mathbf {F}} {b_3}}\}\}$ and $\{ \{{{\mathbf {T}} {a_1}},{{\mathbf {F}} {b_2}}\}, \{{{\mathbf {T}} {a_2}},{{\mathbf {F}} {b_3}}\}, \{{{\mathbf {T}} {a_3}},{{\mathbf {F}} {b_4}}\}\}$ are generalizations of $\{{{\mathbf {T}} {a_2}},{{\mathbf {F}} {b_3}}\}$ and of $\{{{\mathbf {T}} {a_3}},{{\mathbf {F}} {b_4}}\}$ .

Next, by the “other problems” mentioned in the question, we refer to variations $m$ of the length of the solution and to variations $({\Pi, I',F'})$ of the original problem where the initial and final situation may change, but the temporal program remains the same. Then, a generalization of a nogood “can be applied” to such problems if it can be added to the set of nogoods used by the algorithm $\mathit {CDNL}\text {-}\mathit {ASP}$ without changing the solutions to the problem. For any variation $({\Pi, I',F'})$ , those nogoods are $\Psi _{{\Pi }}{[1,m]}$ , and a generalization can be added to them if the generalization is entailed by them. Hence, a generalization of a nogood “can be applied” to “some problem” $({\Pi, I',F'})$ , searching for a solution of length $m$ , if the generalization is entailed by $\Psi _{{\Pi }}{[1,m]}$ . Putting all together, we can rephrase our question as follows:

• Given some temporal logic problem $({\Pi, I,F})$ , what generalizations of a resolvent $\delta$ of $\Psi _{{\Pi }}{[i,j]}$ are entailed by $\Psi _{{\Pi }}{[1,m]}$ ?

Fig. 1. Representation of different shifted versions of the nogood $\delta = \{{{\mathbf {T}} {a_3}}\}$ . The surrounding rectangles cover the interval of the nogoods needed to prove them. For example, the rectangle of $\{{{\mathbf {T}} {a_2}}\}$ covers the interval $[1,3]$ because $\{{{\mathbf {T}} {a_2}}\}$ is a resolvent of $\Psi _{\Pi _1}{[1,3]}$ .

Theorem 3. Let $\Pi$ be a temporal logic program, and $\delta$ be a resolvent of $\Psi _{{\Pi }}{[i,j]}$ for some $i$ and $j$ such that $1 \leq i \leq j$ . Then, for any $n\geq 1$ , the set of nogoods $\Psi _{{\Pi }}{[1,n]}$ entails the generalization

\begin{equation*}\{ {{\delta }\langle {t}\rangle } \mid [i+t,j+t] \subseteq [1,n]\}.\end{equation*}

This theorem is based on the fact that the resolution proof that derived $\delta$ from $\Psi _{{\Pi }}{[i,j]}$ can be used to derive every ${\delta }\langle {t}\rangle$ from $\Psi _{{\Pi }}{[i+t,j+t]}$ , simply by shifting the nogoods $t$ time steps. This means that ${\delta }\langle {t}\rangle$ is a resolvent of $\Psi _{{\Pi }}{[i+t,j+t]}$ . Given that $[i+t,j+t] \subseteq [1,n]$ , the nogood ${\delta }\langle {t}\rangle$ is also a resolvent of $\Psi _{{\Pi }}{[1,n]}$ . Then, the theorem follows from the correctness of resolution.

This result allows us to generalize the learned nogoods to different lengths and different initial and final situations. Following our example, if we were now searching for a solution of length 9 to the temporal problem $({\Pi _1,\{{{\mathbf {T}} c}\},\{{{\mathbf {T}} b}\}})$ , we could add the generalization $\{ \{{{\mathbf {T}} {a_i}}\} \mid i \in [2,8]\}$ to ${\mathit {CDNL}\text {-}\mathit {ASP}}({\mathit {gen}(\Pi _1,9)},$ $\{{{\mathbf {T}} {c_0}},{{\mathbf {T}} {b_9}}\})$ . Observe that this method requires knowing the specific interval $[i,j]$ of the nogoods used to derive a learned constraint. To obtain this information in clingo, we would have to modify the implementation of the solving algorithm. We leave that option for future work, and in the next section we follow another approach that does not require to modify the solver.

6 When can we generalize all learned nogoods to all time steps?

Given any temporal problem, Theorem3 gives us a sufficient condition for the generalization of the nogoods learned while solving that problem. In this section, we investigate for what kind of temporal problems can we generalize all learned nogoods to all time steps. In other words, we would like to know when can we add the generalization:

\begin{equation*}\{ {{\delta }\langle {t}\rangle } \mid {\mathit {step}({{\delta }\langle {t}\rangle })} \subseteq [0,n]\}\end{equation*}

of a learned nogood $\delta$ to the set of nogoods used by algorithm $\mathit {CDNL}\text {-}\mathit {ASP}$ .

This analysis suggests that we can always add a learned nogood, shifted backward in time, if the initial states occur in some path with sufficient states before them. A similar analysis in the other direction – for instance, for nogood ${\delta }\langle {1}\rangle$ in the previous example – suggests that we can add a learned nogood, shifted forward in time, if the final states occur in some path with sufficient states after them. These observations lead us to this informal answer: we can generalize all learned nogoods to all time steps if the initial states have enough preceding states and the final states have enough following states. We make this claim precise in the following.

In Section 4 we introduced transition programs and used them to characterize the solutions of a given temporal problem. Transition programs $\mathit {trans}(\Pi )$ define transitions between the states of some temporal program $\Pi$ . In turn, these transitions implicitly define a transition graph $\mathit {G}(\Pi )$ . Formally, given a temporal logic program $\Pi$ over $\mathcal {A}$ , the transition graph $\mathit {G}(\Pi )$ is the graph $( N,E )$ where $E$ is the set of edges

\begin{equation*} \big \{ ( \{ a \mid {a'} \in X \cap {\mathcal {A}'}\}, X \cap \mathcal {A}) \mid X \text { is a stable model of } {\mathit {trans}(\Pi )} \big \} \end{equation*}

and $N$ is the set of nodes occurring in some edge of $E$ , that is, $N = \bigcup _{(X,Y)\in E}\{X,Y\}$ . Every node in $N$ is also a state of $\Pi$ , so we may use both names interchangeably. A path of a transition graph $( N, E )$ is a sequence of states $(X_0, \ldots, X_n)$ such that for every $i \in [1,n]$ the pair $(X_{i-1},X_{i})$ is an edge from $E$ . We say that the length of such a path is $n$ . We usually denote the states occurring in a path by symbols of the form $X_i$ , where the subindex $i$ represents the position of the state in the path, and does not represent the instantiation of some set $X$ to time step $i$ , which would be represented by $X[i]$ .

We can characterize the solutions to a temporal problem $({\Pi, I,F})$ as the finite paths of $\mathit {G}(\Pi )$ whose first and final nodes are consistent with $I$ and $F$ , respectively. We state this formally in the next theorem, that extends Theorem2.

Fig. 2. Transition $\mathit {G}(\Pi _1)$ of temporal program $\Pi _1$ . The nodes that belong to some solution of length $4$ have a gray background. The transitions of those solutions are represented by normal arrows, while the other arrows are dashed.

Figure 2 represents the transition $\mathit {G}(\Pi _1)$ of temporal program $\Pi _1$ . There are only three paths in $\mathit {G}(\Pi )$ of length $4$ :

• • $( \{a,b,c\}, \{a,b\}, \{b,d\}, \{c,d\}, \{a,c,d\})$ ,

• • $( \{a,b,c\}, \{a,b\}, \{b\}, \{c,d\}, \{a,c,d\})$ , and

• • $( \{a,b,c\}, \{a,b\}, \{b\}, \{b,c,d\}, \{a,c,d\})$ .

By Theorem4, each of them corresponds to one of the solutions to $({\Pi _1,\emptyset, \emptyset })$ of length $4$ .

Theorem4 establishes a relation between the solutions to the set of nogoods $\Psi _\Pi {[1,n]}$ and the paths of $\mathit {G}(\Pi )$ . This leads naturally to a relation between the nogoods entailed by $\Psi _\Pi {[1,n]}$ and the paths of $\mathit {G}(\Pi )$ .

We formalize the relation between nogoods and paths. For simplicity, we only discuss the case where learned nogoods consist of normal atoms, but the extension to body atoms does not pose any special challenge, since body atoms can be seen as a conjunction of literals over normal atoms. Let $\Pi$ be a temporal program over $\mathcal {A}$ , let $( X_0, \ldots, X_n )$ be some path in $\mathit {G}(\Pi )$ , and $\delta$ be some (non-temporal) nogood over $\mathcal {A}{[0,n]}$ . We say that the path $( X_0, \ldots, X_n )$ violates $\delta$ if

\begin{equation*}\delta \subseteq \bigcup _{i \in [0,n]}\big ( \{ {{\mathbf {T}} a_i} \mid a \in X_i \} \cup \{ {{\mathbf {F}} a_i} \mid a \in \mathcal {A}\setminus X_i \} \big ).\end{equation*}

The right-hand side of the equation represents the path as an assignment.

Our next theorem answers formally the question of this section. To introduce it, we define a node in a given graph as a source if it has no incoming edges, as a sink if it has no outgoing edges, and as an internal node otherwise. Then, we say that a temporal program $\Pi$ is internal if every node in $\mathit {G}(\Pi )$ is internal. The theorem states that we can generalize all learned nogoods to all time steps when the temporal program is internal.

Observe that if $\Pi$ is internal, then every path can be extended arbitrarily from both ends. This means that every state has always “enough preceding states” and “enough following states,” as we said earlier.

Theorem 5. Let $\Pi$ be a temporal logic program, and $\delta$ be a resolvent of $\Psi _{{\Pi }}{[i,j]}$ for $1 \leq i \leq j$ . If $\Pi$ is internal, for any $n\geq 1$ , the set of nogoods $\Psi _{{\Pi }}{[1,n]}$ entails the generalization

\begin{equation*}\{ {{\delta }\langle {t}\rangle } \mid {\mathit {step}({{\delta }\langle {t}\rangle })} \subseteq [0,n]\}.\end{equation*}

Theorem5 allows the generalization of learned nogoods to all time steps when the temporal program is internal. Unfortunately, internal temporal programs are not very useful for representing planning problems. To see this, consider some planning problem and any of its transitions, where an action $a$ in state $X$ results in state $Y$ . If actions occur at the same time point as their effects – as in our introductory example – the transition graph must have an edge between $X$ and $Y \cup \{a\}$ . Since actions at the previous step can be chosen freely, for any action $b$ there will also be an edge between $X \cup \{b\}$ and $Y \cup \{a\}$ . But if the temporal program is internal, then $X \cup \{b\}$ must have an incoming edge. Hence, $X$ must result from executing action $b$ in some state. Overall, this means that every state $X$ that leads to another state $Y$ must be the result of every possible action under some previous state, which clearly does not apply to many planning problems. Something similar happens if action occurrences are placed before their effects.

To address this issue, we extend our study by taking into account the initial states associated with temporal logic problems. We refine the definition of being internal by considering only the initial states and the states that are reachable from them. This modification resolves the problem observed in our previous example: if the state $X \cup \{b\}$ has no incoming edges, then it is not reachable from any initial state, and no condition is imposed on it.

Let $\Pi$ be a temporal logic program and $I$ be a partial assignment. A state $X$ of $\Pi$ is

• • initial wrt $I$ if it is consistent with $I$ and has some outgoing edge in $\mathit {G}(\Pi )$ ;

• • reachable wrt $I$ if it can be reached from some initial state of $\Pi$ wrt $I$ , that is if there is some path $( Y, \ldots, X )$ in $\mathit {G}(\Pi )$ starting at some initial state $Y$ of $\Pi$ wrt $I$ ; and

• • loop-reachable if it can be reached from some loop in $\mathit {G}(\Pi )$ , that is if there is some path of the form $(Y, \ldots, Y, \ldots, X)$ in $\mathit {G}(\Pi )$ for some state $Y$ of $\Pi$ .

The temporal program $\Pi$ is internal wrt $I$ if these conditions hold:

1. (i) Every initial state wrt $I$ is loop-reachable.

2. (ii) Every reachable state wrt $I$ is internal.

Condition (i) guarantees that initial states have “enough previous states”, and condition (ii) guarantees that reachable states have “enough successor states”. Together, they imply that any path starting at some initial or reachable state can be extended indefinitely in both directions.

Temporal programs that are internal with respect to a partial assignment generalize the notion of internal temporal programs.

If a temporal program is internal wrt an assignment $I$ , we can generalize all learned nogoods to all time steps provided that $I$ holds initially. We enforce this condition by adding the set of nogoods $ \big \{ \{ {{\mathbf {F}} {a_0}} \} \mid {{\mathbf {T}} a} \in I \big \} \cup \big \{ \{ {{\mathbf {T}} {a_0}} \} \mid {{\mathbf {F}} a} \in I \big \}$ that we denote by $\mathit {nogoods}(I)$ .

Theorem 6. Let $\Pi$ be a temporal logic program, $I$ be a partial assignment, and $\delta$ be a resolvent of $\Psi _{{\Pi }}{[i,j]}$ for $1 \leq i \leq j$ . If $\Pi$ is internal wrt $I$ , then for any $n\geq 1$ , the set of nogoods ${\Psi _{{\Pi }}{[1,n]}}\cup {\mathit {nogoods}(I)}$ entails the generalization

\begin{equation*}\{ {{\delta }\langle {t}\rangle } \mid {\mathit {step}({{\delta }\langle {t}\rangle })} \subseteq [0,n]\}.\end{equation*}

In theory, the inclusion of $\mathit {nogoods}(I)$ appears to conflict with our goal of applying the learned nogoods to variations of the original problem with different initial states. But in practice this need not pose a problem, since the assignment $I$ may reflect a form of representing problems in general – such as placing actions at the step where their effects occur – and be independent of any specific instance. As a result, the learned nogoods may remain applicable to all intended variations of the original problem.

This observation holds for most representations of planning problems that we have encountered, which can be captured by temporal logic programs internal wrt a generic assignment $I$ . Such an assignment ensures that

1. (a) initial states have no action occurrences.

To achieve this, actions must occur at the same time step as their effects. In ASP, this is usually a matter of convenience. To satisfy condition (i) of being internal wrt $I$ , it suffices if:

1. (b) whenever no action occurs in a state, that state remains unchanged.

Conditions (a) and (b) create a loop in all initial states, making them loop-reachable. To meet condition (b), the representation should allow the non-execution of actions, and the law of inertia should make all fluents persist. Most representations of planning problem conform to this, or can be adapted with minor changes. Condition (ii) of being internal wrt $I$ can be satisfied directly if after the execution of each action, another action can always be applied. An alternative and more generic condition is the following:

1. (c) from every state with an action occurrence, there is a transition to the same state without action occurrences.

In addition to the representation of inertia, this condition only requires that the representation always allows the non-execution of actions. Based on our experience, most representations of planning problems satisfy conditions (a-c) or, as we have seen in our introductory example, can be easily modified to do that. In fact, the encodings used in our conference paper (Romero et al. Reference Romero, Schaub, Strauch, Proceedings and Turhan2022) required only minor changes to fit within this approach.

In summary, our methodology represents a planning problem as a temporal logic problem $({\Pi, I,F})$ such that the assignment $I$ is divided into:

• • A generic assignment $I_1$ that ensures condition (a).

• • A specific assignment $I_2$ that describes the initial situation of the planning problem.

Moreover, the temporal program $\Pi$ is construed to satisfy conditions (b) and (c), ensuring that it is internal wrt $I_1$ . Given this, to solve $({\Pi, I,F})$ we run the procedure ${\mathit {CDNL}\text {-}\mathit {ASP}}({\mathit {gen}(\Pi, n)},{I_1[0]}\cup {I_2[0]}\cup {F[n]})$ for different lengths $n$ . For each run, any nogood $\delta$ learned by the solver is a resolvent of $\Psi _{{\Pi }}{[1,n]}$ . By Theorem6, we can generalize $\delta$ across all time steps, also in other runs with different lengths, and in other variations of the original problem. Such variations can be represented as temporal logic problems $({\Pi, I_1 \cup {I_2^{\prime}},F'})$ where $\Pi$ and $I_1$ remain unchanged. As before, we can solve them using ${\mathit {CDNL}\text {-}\mathit {ASP}}({\mathit {gen}(\Pi, n)},{I_1[0]}\cup {I_2'[0]}\cup {F'[n]})$ for different lengths $n$ . Since the solutions computed by such calls are solutions of ${\Psi _{{\Pi }}{[1,n]}} \cup {\mathit {nogoods}(I_1)}$ , by Theorem6 the generalization of $\delta$ to all time steps can also be added to them.

7 From non-internal to internal temporal programs

If we want to solve the temporal problem $({\Pi _1,\emptyset, \emptyset })$ and generalize the nogoods learned during this process, the results from the previous section are not applicable because $\Pi _1$ is not internal, and the initial assignment is empty. To address this limitation, we introduce a method to translate any temporal program into an internal one that preserves the same solutions modulo the original atoms. We can solve the original problem using the new program, and given that this program is internal, we can generalize all learned nogoods to all time steps. Moreover, we can apply these nogoods to the original program, after eliminating the auxiliary atoms introduced by the translation.

Let $\Pi$ be a temporal logic program over $\mathcal {A}$ , and let $\lambda$ be a fresh atom not included in $\mathcal {A}$ . We define $\lambda (\Pi )$ as the temporal logic program

(9) \begin{align} \{ \{ {\lambda } \} \leftarrow \} \ \cup \\[-36pt]\nonumber \end{align}

(10) \begin{align} \{ {\mathit {h}(r)} \leftarrow {\mathit {Bd}(r)} \cup \{ {\lambda }\} \mid r \in \Pi \} \ \cup \\[-36pt]\nonumber\end{align}

(11) \begin{align} \{ \{ a \} \leftarrow \neg {\lambda } \mid a \in \mathcal {A} \}. \end{align}

This translation extends $\Pi$ by introducing a choice rule for $\lambda$ , tagging the rules of $\Pi$ with $\lambda$ , and allowing the selection of any subset of $\mathcal {A}$ when $\lambda$ does not hold.

To understand the translation, let us study the relationship between the transition graphs defined by $\Pi$ and $\lambda (\Pi )$ . These graphs are defined by the corresponding transition programs:

• • ${\mathit {trans}(\Pi )} = \Pi \cup {\mathit {Choice}(\mathcal {A}')}$ , and

• • ${\mathit {trans}({\lambda (\Pi )})} = {\lambda (\Pi )}\cup {\mathit {Choice}(\mathcal {A}'\cup \{{\lambda }'\})}$ .

The behavior of $\mathit {trans}({\lambda (\Pi )})$ depends on whether $\lambda$ is chosen at (9) or not. If $\lambda$ is chosen, then $\mathit {trans}({\lambda (\Pi )})$ has the same stable models as the program

\begin{equation*}\{{\lambda }\leftarrow \}\cup {\mathit {trans}(\Pi )}\cup \{\{{\lambda }'\}\leftarrow \}\end{equation*}

as the rules in (10) can be simplified to the original rules from $\Pi$ , and the rules in (11) become irrelevant. Then, for every stable model $X$ of $\mathit {trans}(\Pi )$ , the sets $X \cup \{{\lambda }\}$ and $X \cup \{{\lambda },{\lambda }'\}$ are stable models of $\mathit {trans}({\lambda (\Pi )})$ . In terms of transition graphs, this means that for every edge $(X,Y)$ in $\mathit {G}(\Pi )$ there are two corresponding edges $(X,Y\cup \{{\lambda }\})$ and $(X\cup \{{\lambda }\},Y\cup \{{\lambda }\})$ in $\mathit {G}({\lambda (\Pi )})$ .

If $\lambda$ is not chosen, then $\mathit {trans}({\lambda (\Pi )})$ has the same stable models as the program

\begin{equation*}\{ \{ a \} \leftarrow \mid a \in \mathcal {A}\} \cup {\mathit {Choice}(\mathcal {A}'\cup \{{\lambda }'\})}\end{equation*}

as the rules in (10) have no effect, and the body of (11) becomes true. Then, for every $X,Y \subseteq \mathcal {A}$ , if $X'$ denotes the set $\{ a' \mid a \in X\}$ , the sets $X' \cup Y$ and $X' \cup Y \cup \{{\lambda }'\}$ are stable models of $\mathit {trans}({\lambda (\Pi )})$ . Accordingly, $\mathit {G}({\lambda (\Pi )})$ contains the edges $(X,Y)$ and $(X\cup \{{\lambda }\},Y)$ .

Given these sets, particularly the second, there is a one-to-one correspondence between the paths in $\mathit {G}(\Pi )$ and the paths in $\mathit {G}({\lambda (\Pi )})$ where $\lambda$ belongs to all states. This correspondence holds even if $\lambda$ does not occur in the initial state of the path, since the first edge can also be taken from the first set of the previous proposition. By Theorem4, this correspondence between paths induces a correspondence between the solutions to $\Pi$ and the solutions to $\lambda (\Pi )$ where $\lambda$ is true always after the initial step. To formalize this, we say that a solution $(X,n)$ to a given temporal problem is $\lambda$ -normal if ${{\lambda }_0}\notin X$ and ${{\lambda }_i}\in X$ for all $i \in [1,n]$ .

The call ${\mathit {CDNL}\text {-}\mathit {ASP}}({\mathit {gen}({\lambda (\Pi )},n)},$ $ {I[0]}\cup {F[n]}\cup \{{{\mathbf {F}} {{\lambda }_0}}, {{\mathbf {T}} {{\lambda }_1}},\ldots, {{\mathbf {T}} {{\lambda }_n}}\})$ computes $\lambda$ -normal solutions to $({\lambda (\Pi )},I,F)$ , enforcing the correct value for $\lambda$ at every time point using assumptions. The solutions to the original problem $({\lambda (\Pi )},I,F)$ can be obtained from these $\lambda$ -normal solutions by removing the atoms $\{{{\lambda }_1}, \ldots, {{\lambda }_n}\}$ .

The following proposition establishes that the program $\lambda (\Pi )$ is internal wrt $\{\mathbf {F} \lambda _{0}\}$ . To see why, observe that the third and fourth sets of Proposition6 show that, in $\mathit {G}({\lambda (\Pi )})$ , every state $X$ –whether it contains $\lambda$ or not – is connected to the state $X \setminus \{{\lambda }\}$ . This implies that:

1. (a) every state without $\lambda$ is connected to itself, and

2. (b) every state has a successor state.

Condition (a) provides condition (i) for $\Pi$ being internal wrt $\{\mathbf {F} {\lambda }_{0}\}$ , since initial states do not have $\lambda$ ; and condition (b) ensures the corresponding condition (ii).

Since $\lambda (\Pi )$ is internal wrt $\{{\mathbf {F}} {\lambda }_{0}\}$ , by Theorem6 we obtain the next result, that allows us to generalize all nogoods learned using $\Psi _{\lambda (\Pi )}$ to all time steps, as long as $\lambda$ is initially false.

Theorem 7. Let $\Pi$ be a temporal logic program, and $\delta$ be a resolvent of $\Psi _{{{\lambda (\Pi )}}}{[i,j]}$ for some $i$ and $j$ such that $1 \leq i \leq j$ . For any $n\geq 1$ , the set of nogoods ${\Psi _{{{\lambda (\Pi )}}}{[1,n]}}\cup \big \{\{{{\mathbf {T}} {{\lambda }_0}}\}\big \}$ entails the generalization

\begin{equation*}\{ {{\delta }\langle {t}\rangle } \mid {\mathit {step}({{\delta }\langle {t}\rangle })} \subseteq [0,n]\}.\end{equation*}

The nogoods learned from the program $\lambda ({\Pi })$ can be applied to the original program $\Pi$ after removing all auxiliary atoms. We define the simplification of a nogood $\delta$ , denoted by $\mathit {simp}(\delta )$ , as the nogood obtained from $\delta$ after removing all literals of the form ${\mathbf {F}} {{\lambda }_i}$ or ${\mathbf {T}} {{\lambda }_i}$ . for any integer $i$ .

Theorem 8. Let $\Pi$ be a temporal logic program, and let $\delta$ be a resolvent of $\Psi _{{{\lambda (\Pi )}}}{[i,j]}$ for some $i$ and $j$ such that $1 \leq i \leq j$ . For any $n\geq 1$ , the set of nogoods $\Psi _{{\Pi }}{[1,n]}$ entails the generalization

\begin{equation*}\{ {\mathit {simp}({{\delta }\langle {t}\rangle })} \mid {\mathit {step}({{\delta }\langle {t}\rangle })} \subseteq [0,n], {{\mathbf {T}} {{\lambda }_0}}\notin {{\delta }\langle {t}\rangle } \}.\end{equation*}

8 Experiments

We experimentally evaluate the generalization of learned nogoods in ASP planning using the solver clingo. The goal of the experiments is to study the performance of clingo when the planning encodings are extended by the generalizations of some constraints learned by clingo itself. We are interested only in the solving time and not in the grounding time, but in any case we have observed no differences between grounding times among the different configurations. We did experiments in two different settings, single-shot and multi-shot, that we detail below. Following the approach of (Gebser et al. Reference Gebser, Kaminski, Kaufmann, Lühne, Romero, Schaub, Carro and King2016), in all experiments we disregarded the learned nogoods of size greater than $50$ and of degree greater than $10$ , where the degree of a nogood is defined as the difference between the maximum and minimum step of the literals of the nogood.Footnote ¹ In all the experiments, the learned nogoods are always sorted either by size or by literal block distance (lbd, (Audemard and Simon, 2009)), a measure that is usually associated with the quality of a learned nogood. We tried configurations adding the best $500$ , $1000$ , or $1500$ nogoods, according to either their nogood size or their lbd. The results ordering the nogoods by lbd were similar but slightly better than those ordering by size, and here we focus on them. We used two benchmark sets from (Dimopoulos et al. Reference Dimopoulos, Gebser, Lühne, Romero and Schaub2018). The first consists of PDDL benchmarks from planning competitions, translated to ASP using the system plasp presented in that paper. This set contains 120 instances of 6 different domains. The second set consists of ASP planning benchmarks from ASP competitions. It contains 136 instances of 9 domains. We adapted the logic programs of these benchmarks to the format of temporal logic programs as follows: we deleted the facts used to specify the initial situation, as well as the integrity constraints used to specify the goal, we added some choice rules to open the initial situation, and we fixed the initial situation and the goal using assumptions. All benchmarks were run using the version $5.5.1$ of clingo on an Intel Xeon E5-2650v4 under Debian GNU/Linux 10, with a memory limit of 8 GB, and a timeout of 15 minutes per instance.

The task in the single-shot experiment is to find a plan of a fixed length $n$ that is part of the input. For the PDDL benchmarks we consider plan lengths varying from $5$ to $75$ in steps of $5$ units, for a total of $2040$ instances. The ASP benchmarks already have a plan length, and we use it. In a preliminary learning step, clingo is run with every instance for $10$ minutes or until $16000$ nogoods are learned, whatever happens first. The actual learning time is disregarded and not taken into account in the tables. Some PDDL instances reach the memory limit in this phaseFootnote ² We leave them aside and are left with $1663$ instances of this type. We compare the performance of clingo running normally (baseline), versus the (learning) configurations where we add the best $500$ , $1000$ , or $1500$ learned nogoods according to their lbd value. In this case we apply Theorem6 and learn the nogoods using a slight variation of the original encoding, but use the original encoding for the evaluation of all configurations.

Tables 1 and 2 show the results for the PDDL and the ASP benchmarks, respectively. The first columns include the name and number of instances of every domain. The tables show the average solving times and the number of timeouts, in parenthesis, for every configuration and domain. We can observe that in general the learning configurations are faster than the baseline and in some domains they solve more instances. The improvement is not huge, but is persistent among the different settings. The only exception is the elevator domain in PDDL, where the baseline is a bit faster than the other configurations. We also analyzed the average number of conflicts per domain and configuration, and the results follow the same trend as the solving times.

Table 1. Single-shot solving of PDDL benchmarks

Table 2. Single-shot solving of ASP benchmarks

In the multi-shot solving experiment, the solver first looks for a plan of length $5$ . If the solver finds no such plan, then it looks for a plan of length $10$ , and so on until it finds a plan. At each of these solver calls, we collect the best learned nogoods. Then, before the next solver call, we add the generalization of the best $500$ , $1000$ , or $1500$ of them, depending on the configuration. As before, we rely on Theorem6, but this time we use the same original encoding, slightly modified, for both learning and solving.Footnote ³ The results for PDDL and ASP are shown in Tables 3 and 4, respectively. In both of them, the baseline and the different configurations perform similarly, and there is not a clear trend. The analysis of the number of conflicts shows similar results.

Table 3. Multi-shot solving of PDDL benchmarks

Table 4. Multi-shot solving of ASP benchmarks

We expected similar results in the single-shot and the multi-shot solving experiments, but the learning configurations outperformed the baseline in the former, while they performed similarly in the latter. We do not have a clear explanation for this, but we can suggest some hypotheses. In the single-shot experiments we can select the best nogood from a larger set than in the multi-shot experiments, which could influence the quality of the learned nogoods. In addition, having the learned constraints from the start could positively influence the solver’s heuristic. Moreover, the fixed plan length in the single-shot experiments could also improve the learning process.