# On the Semantics of Hybrid ASP Systems Based on Clingo
## 5 Answer Set Solving Modulo Linear Equations
### clingo[DL]  
Let us now return to the clingo[DL] system that uses the theory \(\mathfrak{D}\) in which theory atoms have the form &diff\(\{x-y\}\) <= \(k\), as introduced in (6). As with \(\mathfrak{L}\), the abstract theory \(\mathfrak{D}\) also has a complete complement operation. However, while in linear constraints, the complementary atom would be obtained by just switching the ordering relation from '<=' to '>', in the case of \(\mathfrak{D}\), the resulting construct &diff\(\{x-y\}\)>\(k\) is not exactly in the format of a difference constraint, where we must always use the '<=' relation. Fortunately, as we deal with integer numbers, we can reformulate the complement simply as &diff\(\{y-x\}\) <= \(-k-1\). For example, the complement of &diff\(\{x-y\}\) <= 5 would be &diff\(\{y-x\}\) <= \(-6\).  
In clingo[DL], the set of external atoms \(\mathcal{E}\) consists of all body atoms: atoms that do not occur in rule bodies are founded. One difference with respect to clingcon is that, in this case, we do have a one-to-one correspondence between the \(\mathfrak{D}\)-solutions and the \(\langle\mathfrak{D},\mathcal{E}\rangle\)-stable models of a clingo[DL]-logic program \(P\). Another important difference is that, for a given stable model, clingo[DL] does not enumerate all possible \(\langle\mathfrak{D},\mathcal{E}\rangle\)-answer sets but only provides one of them. This answer set corresponds to the case where all integer variables are assigned a non-negative integer with the minimal possible value. That is, clingo[DL]-answer sets are a selection among the \(\langle\mathfrak{D},\mathcal{E}\rangle\)-answer sets of the program. Formally, to characterize this minimal answer set, we start defining a partial order \(\leq_{\text{d1}}\) between two \(\langle\mathfrak{D},\mathcal{E}\rangle\)-answer sets \((Y,v)\) and \((Y^{\prime},v^{\prime})\) as follows:  
\[(Y,v)\leq_{\text{d1}}(Y^{\prime},v^{\prime})\text{ iff }\] \[Y=Y^{\prime}\text{ and }\textit{domain}(v)=\textit{domain}(v^{ \prime})\text{ and }v(x)\leq v^{\prime}(x)\text{ for all }x\in\textit{domain}(v)\]  
As usual, we write \((Y,v)<_{\text{d1}}(Y^{\prime},v^{\prime})\) when \((Y,v)\leq_{\text{d1}}(Y^{\prime},v^{\prime})\) and \(v\
eq v^{\prime}\).  
**Definition 6** (clingo[DL]-answer set).: _A \(\langle\mathfrak{D},\mathcal{E}\rangle\)-answer set \((Y,v)\) is called a clingo[DL]-answer set of \(P\) if \((Y,v)\) is \(<_{\text{d1}}\)-minimal among the \(\langle\mathfrak{D},\mathcal{E}\rangle\)-answer sets of \(P\) that do not assign a negative value to any variable._  
Note that if a set of difference constraints has a solution, then it also has a solution that assigns non-negative integer values to all variables. As a simple example consider a clingo[DL]-program that just consists of the fact  
\[\&\texttt{diff}\{x-y\}\mathrel{\hbox to 0.0 pt{\lower 4.0 pt\hbox{ $\sim$}}\raise 1.0 pt \hbox{$-$}}-2 \tag{18}\]  
This program is imposing the condition \(x+2\leq y\) and has infinitely many answer sets: we can choose any integer value for \(x\) and then fix \(y\) as any value greater than or equal to \(x+2\). However, since clingo[DL]-answer sets do not admit negative numbers, we must further pick \(x\geq 0\), leaving the possible answer sets shown in Figure 1, where each pair of numbers \((c,d)\) represents the valuation \(x=c\), \(y=d\). The arrows show the \(<_{\text{d1}}\) relationsamong them. In this case, there exists a unique clingo[DL]-answer set corresponding to the valuation \(x=0,y=2\).