## 4 Solving the Warehouse Delivery Problem
### Task Assignment and Sequencing
#### 4.3.2 Conflict Detection and Resolution
* If \(\texttt{assign}(r,t)\!\in X\), then \(t\in f_{T}^{X}(r)\);
* If \(\{\texttt{assign}(r,t),\texttt{assign}(r,t^{\prime}),\texttt{task\_sequence}(t,t ^{\prime})\}\subseteq X\), then \(\langle t,t^{\prime}\rangle\sqsubseteq f_{T}^{X}(r)\);
* If \(\{\texttt{walk}(r,s,v),\texttt{dl}(\texttt{arrive}(r,s),a),\texttt{dl}( \texttt{exit}(r,s),e)\}\subseteq X\) and \(\texttt{walk}(r,s+1,v^{\prime})\ \in X\), then route point \((v,a,e)\) is at position \(s+1\) of \(f_{W}^{X}(r)\);
* If \(\{\texttt{walk}(r,s,v),\texttt{dl}(\texttt{arrive}(r,s),a),\texttt{dl}( \texttt{exit}(r,s),e)\}\subseteq X\) and \(\texttt{walk}(r,s+1,v^{\prime})\
ot\in X\), then route point \((v,a,\infty)\) is at position \(s+1\) of \(f_{W}^{X}(r)\);
* If there are no \(\texttt{walk}/3\) atoms for \(r\) in \(X\), then \(f_{W}^{X}(r)=\langle(f_{H}(r),0,\infty)\rangle\). Given a stable model \(X\) of logic program \(F\cup P\), we now establish step by step why the induced robot assignment \((f_{T}^{X},f_{W}^{X})\) meets all required conditions of a solution to the warehouse delivery problem. We begin with the basic properties of robot assignments. **Condition 4: \(f_{T}^{X}(r)\) is a task sequence over \(T\) for every robot \(r\in R\)**. As described in Section 4.2, atoms over predicates \(\texttt{assign}/2\) and \(\texttt{task\_sequence}/2\) are established in a way that all tasks are assigned to exactly one robot (Lines 1 and 2 in Listing 2), tasks are indeed arranged in sequences with a single beginning (Line 15 in Listing 2), no branching (Line 14 in Listing 2), or cycles (either Listing 4 or timing constraints induced by Listing 9), and, finally, tasks connected via a task sequence are assigned to the same robot (Line 12 in Listing 2), Then, by construction, this carries over to \(f_{T}^{X}(r)\) and makes each a task sequence for any \(r\in R\). Note, there are two implicit consequences of the above construct of \(f_{T}^{X}\) from \(X\). Firstly, if there are no \(\texttt{assign}/2\) atoms for \(r\) in \(X\) then \(f_{T}^{X}(r)=\langle\rangle\). Secondly, if there does exist some \(\texttt{assign}(r,t)\!\in X\) but \(t\) does not exist either as the first or second parameter of some \(\texttt{task\_sequence}/2\) atom, then \(\texttt{assign}(r,t)\) is guaranteed to be the only \(\texttt{assign}/2\) atom for \(r\) and \(f_{T}^{X}(r)=\langle t\rangle\). **Condition 5: \(f_{W}^{X}(r)\) is a timed walk feasible in (\(V\),\(E\),\(f_{E}\),\(C\),\(R\),\(f_{H}\),\(f_{S}\)) for every robot \(r\in R\). ** This is achieved by the rules in Lines 5, 7, and 8 in Listing 6 and Lines 1 and 3 in Listing 9. The construction of \(f_{W}^{X}\) along with the consecutive numbering of steps enforced in Line 7 of Listing 6, ensures that any atom \(\mathtt{walk}(r,s,v)\in X\) indicates a route point \((v,a,e)\in f_{W}^{X}(r)\) at position \(s+1\) in the timed walk of robot \(r\) for \(v\in V\) and \(a,e\in\mathbb{N}\). We rely upon their consecutive step numbering in the following. For Condition 1, we observe that for two successive route points \((v,a,e)\) and \((v^{\prime},a^{\prime},e^{\prime})\) in \(f_{T}^{X}(r)\), the integrity constraint in Line 8 of Listing 6 makes sure that there exists an edge \((v,v^{\prime})\in E\). Condition 2 is captured in Line 1 of Listing 9: For any route point \((v,a,e)\) in a timed walk \(f_{T}^{X}(r)\), the robot's exit time is at least as large as its arrival time, viz. we have \(a\leq e\). Line 3 of Listing 9 enforces Condition 3; it requires \(e+f_{E}((v,v^{\prime}))\leq a^{\prime}\) for any successive route points \((v,a,e)\) and \((v^{\prime},a^{\prime},e^{\prime})\) in \(f_{T}^{X}(r)\). Note that Line 5 of Listing 6 does not guarantee that instances of predicate \(\mathtt{walk}/3\) are generated for every robot. This leaves us with the corner case that there may be no such atoms in \(X\) for a given robot \(r\). This corresponds to the timed walk \(f_{W}^{X}(r)=\langle(f_{H}(r),0,\infty)\rangle\). In this case, Condition 1 and 2 are trivially satisfied in the presence of a single route point and \(0\leq\infty\) satisfies Condition 3.