theory.tex

\section{Theory Solving}\label{sec:theory}

This section is not yet ready for publishing
and will be included in one of the forthcoming editions of this guide.

Information on theory solving with \clingo\ can be obtained at the following references.

\begin{itemize}
\item Literature: \cite{gekakaosscwa16a,kascwa17a}
\item Examples: \code{/examples/clingo/} in \gringo/\clingo\ distribution
\item API reference: \url{http://potassco.org/clingo}
\end{itemize}

\subsection{ASP and Difference Constraints}
\label{sec:difference:constraints}

The system \clingoM{DL} provides a seamless way to integrate a subset of the theory of linear constraints, namely Quantifier-Free Integer Difference Logic (QF-IDL), into ASP.
It deals with constraints of the form $x-y\leq k$, where $x$ and $y$ are integer variables and $k$ is an integer constant.
Despite its restriction, QF-IDL can be used to naturally encode timing related problems, e.g., scheduling or timetabling, and provides the additional advantage of being solvable in polynomial time.
Syntactically, a difference constraint $x-y\leq k$ is represented by a difference constraint atom of the form:
 \[
    \code{\&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$}
 \]
Here, $x$ and $y$ may be terms as described in Section~\ref{subsec:lang:gringo}, but are internally interpreted as integer variable names,
and $k$ is an integer.
Difference constraint atoms may occur in bodies as well as in heads of rules.
For a more formal introduction of \clingoM{DL}, please see \cite{jakaosscscwa17a}.
The following explanations are conform with \clingoM{DL}~1.0.0 which is available here: \url{http://github.com/potassco/clingoDL}.


\subsubsection{Modeling and Solving with \clingoM{DL}}

The most common usage of \clingoM{DL} in its default configuration are rules of the form:
  \begin{align*}
    \code{\&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$ :- $L_1$,$\dots$,$L_n$.}
  \end{align*}
Here, $L_i$ for $1\leq i \leq n$ are literals as described in \ref{subsec:gringo:normal}.
Intuitively, it means that whenever the body of such a rule holds, 
the linear equation represented by the head has to be satisfied as well.
Conversely, if the body does not hold, no constraints are posed to the QF-IDL theory.
\begin{example}\label{ex:dl:simple}
         See the following simple example:
         \lstinputlisting{examples/dl1.lp}
The program contains one propositional variable \code{a} and two integer variables called \code{x} and \code{y}.
The truth value of \code{a} can be freely chosen (Line~1),
and whenever \code{a} holds, the linear equation $\code{x}-\code{y}\leq -3$ must also hold (Line~2).

Calling the system with the example produces following output:
\marginlabel{%
  To inspect the output, invoke:\\
  \code{\mbox{~}clingo-dl \textbackslash\\ 
        \mbox{~~~}\attach{examples/dl1.lp}{dl1.lp}   0}\\
}
\begin{lstlisting}[numbers=none]
clingo-dl version 1.0.0
Reading from dl1.lp
Solving...
Answer: 1

Answer: 2
dl(x,"0") dl(y,"3") a
SATISFIABLE

Models       : 2
Calls        : 1
...
\end{lstlisting}
There are two answer sets, one is the empty answer set and one contains \code{a} and the symbols \code{dl(x,"0")} and \code{dl(y,"3")}.
A symbol \code{dl($x$,"$v$")} denotes that variable $x$ is assigned value $v$.
This means that in the second answer set a valid assignment for \code{x} and \code{y} was found,
0 and 3, respectively, such that $\code{x}-\code{y}\leq -3$ is satisfied.

There are two things of note in the results.
First, no assignment is given for \code{x} and \code{y} in the first answer set since there are no difference constraints to satisfy,
hence values may be arbitrary.
Second, only one valid assignment for \code{x} and \code{y} is shown in the second answer set 
while in principle there are infinitely many valid assignments satisfying $\code{x}-\code{y}\leq -3$.
The assignment that is given by \clingoM{DL} is a so-called \emph{As-Soon-As-Possible (ASAP) assignment}.
Such assignments have the minimal sum of absolute values assigned to the variables,
or, in other words, values are as close to 0 as possible while still fulfilling all difference constraints.
As we will see in the following example, this is a useful trait in some scheduling problems,
where the ASAP assignment represents the earliest time point at which tasks may start while adhering to all timing constraints.

 \end{example}


\begin{example}\label{ex:dl:fs}

% --------------------------------------------------------------------------------
\begin{figure}[ht]
\centering
{\def\svgscale{.4}
\input{figures/dl}}
\caption{Flow shop: instance with three tasks and two machines\label{fig:fs:ins}}
\end{figure}
\begin{figure}[ht]
\centering
{\def\svgwidth{\linewidth}
\input{figures/dl-sol}}
\caption{Flow shop: solutions for all possible permutations\label{fig:fs:sol}}
\end{figure}
% --------------------------------------------------------------------------------
%
For a more involved example, we consider the flow shop problem.
The flow shop problem creates a schedule for a set of tasks $T$ that have to be consecutively executed on $m$ machines.
%
Each task has to be processed on each machine from $1$ to $m$. 
Different parts of one task are completed on each machine resulting in the completion of the task after execution on all machines is finished.
Before a task can be processed on machine $i$, it has to be finished on machine $i-1$.
The duration of different tasks on the same machine may vary.
A task can only be executed on one machine at a time and
a machine must not be occupied by more than one task at a time.
%
A solution to the problem is a permutation of the tasks and starting times for all tasks on all machines so that no conflicts occur.

Figure~\ref{fig:fs:ins} depicts a possible instance for the flow shop problem.
The three tasks \code{a}, \code{b}, and \code{c} have to be scheduled on two machines.
The colored boxes indicate how long a task has to run on a machine.
Lighter shades of the same color are for the first and darker ones for the second machine.
For example, task \code{a} needs to be processed for~$3$ time units on the first and~$4$ time units on the second machine.

% --------------------------------------------------------------------------------
\lstinputlisting[float=ht,mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily\small},label={prg:fs:ins}]{examples/shop.lp}
% --------------------------------------------------------------------------------
\lstinputlisting[float=ht,literate={\%\%}{}{0},mathescape=true,escapeinside={\#(}{\#)},basicstyle={\ttfamily\small},label={prg:fs:enc}]{examples/flow.lp}
% --------------------------------------------------------------------------------
%
Next we encode this problem using difference constraints.
We give in Listing~\ref{prg:fs:ins} a straightforward encoding of the instance in Figure~\ref{fig:fs:ins}.
Listing~\ref{prg:fs:enc} depicts the encoding of the flow shop problem.
Following the generate, define, and test methodology of ASP,
we first generate in lines~\ref{prg:fs:perm:begin}--\ref{prg:fs:perm:end} all possible permutations of tasks,
where atoms of form \code{perm(T,U)} encode that task~$T$ has to be executed before task~$U$.
Then, in the following lines~\ref{prg:fs:diff:begin}--\ref{prg:fs:diff:end},
we use difference constraints to calculate the duration of the generated permutation.
%
The difference constraint in Line~\ref{prg:fs:permutation:seq} guarantees that the tasks are executed in the right order.
For example, $\code{(a,1)} - \code{(a,2)} \leq -d$ ensures that task~\code{a} can only be executed on machine~\code{2} if it has finished on machine~\code{1}.
Hence, variable \code{(a,2)} has to be assigned so that it is greater or equal to $\code{(a,2)}-d$ where $d$ is the duration of task \code{a} on machine \code{1}.
Similarly, $\code{(a,1)} - \code{(b,1)} \leq -d$ makes sure that task~\code{b} can only be executed on machine~\code{1} if task~\code{a} has finished on machine~\code{1}.
While the first constraint is a fact (see Line~\ref{prg:fs:permutation:seq:machine}),
the latter is subject to the generated permutation of tasks (see Line~\ref{prg:fs:permutation:seq:task}).
%
The difference constraint in Line~\ref{prg:fs:null} ensures that all time points at which a task is started are greater than zero.
Note that this constraint is in principle redundant
but since sets of difference constraints may have infinitely many solutions
it is good practice to encode relative to a starting point.
Furthermore, note that~\code{0} is actually a variable.
This is a dedicated variable that is always assigned the value 0 and can be used to encode difference constraints with only one variable.

Running encoding and instance with \clingoM{DL} results in the following $6$ solutions
corresponding to the solutions in Figure~\ref{fig:fs:sol}.%
\footnote{Note that in each solution all tasks are executed as early as possible.
  This is due to the guaranteed ASAP assignment as mentioned above.}
One for each possible permutation of tasks:
\marginlabel{%
  To inspect the output, invoke:\\
  \code{\mbox{~}clingo-dl \attach{examples/flow.lp}{flow.lp} \textbackslash\\  
        \mbox{~~~}\attach{examples/shop.lp}{shop.lp.} 0}\\
}
 \begin{lstlisting}[numbers=none]
clingo-dl version 1.0.0
Reading from flow.lp ...
Solving...
Answer: 1
dl((a,1),"1")  dl((a,2),"7") dl((b,1),"0") dl((b,2),"1") 
  dl((c,1),"4") dl((c,2),"11") perm(b,a) perm(a,c)
Answer: 2
dl((a,1),"6") dl((a,2),"16") dl((b,1),"5") dl((b,2),"10") 
  dl((c,1),"0") dl((c,2),"5") perm(b,a) perm(c,b)
Answer: 3
dl((a,1),"0") dl((a,2),"3") dl((b,1),"8") dl((b,2),"13") 
  dl((c,1),"3") dl((c,2),"8") perm(c,b) perm(a,c)
Answer: 4
dl((a,1),"6") dl((a,2),"12") dl((b,1),"0") dl((b,2),"1") 
  dl((c,1),"1") dl((c,2),"7") perm(b,c) perm(c,a)
Answer: 5
dl((a,1),"0") dl((a,2),"3") dl((b,1),"3") dl((b,2),"7") 
  dl((c,1),"4") dl((c,2),"13") perm(b,c) perm(a,b)
Answer: 6
dl((a,1),"5") dl((a,2),"10") dl((b,1),"8") dl((b,2),"14") 
  dl((c,1),"0") dl((c,2),"5") perm(c,a) perm(a,b)
SATISFIABLE

Models       : 6
Calls        : 1
...
\end{lstlisting}
\end{example}

\subsubsection{Advanced Options of \clingoM{DL}}

In the following, we will consider the two main parameter that may change \clingoM{DL}'s behavior:
\begin{align*}
 \code{--strict}& \text{ : enables strict semantics}\\
 \code{--rdl}& \text{ : variables and constants of the difference constraints have real values} 
\end{align*}

\paragraph{Strict and Non-strict Semantics}

First, let us consider the \emph{strict semantics} option.
In the default configuration, this option is omitted and \clingoM{DL} works with a \emph{non-strict semantics}.
This option changes the logical connection of the difference constraint atom to the difference constraint it represents.
The connections are as follows:
\begin{align*}
 \text{non-strict :}\quad&\code{\&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$} \quad\Rightarrow\quad x-y\leq k\\
 \text{strict :}\quad&\code{\&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$}\quad \Leftrightarrow \quad x-y\leq k
\end{align*}

Here, the arrows represent logical implication and equivalence, respectively.
Intuitively, as mentioned above, in the non-strict case, 
if a difference constraint atom holds, the difference constraint has to hold as well,
while no constraint has to be considered by the QF-IDL theory if the respective difference constraint atom is false.
In contrast, strict semantics enforces the negation of the difference constraint to be satisfied if the difference constraint atom is false.
For instance, using the strict semantics, if the difference constraint atom $\code{\&diff\text{ }\{x-y\}\text{ }<=\text{ }-3}$ is false,
the difference constraint $\code{y}-\code{x}\leq 2$ has to hold, which is the negation of $\code{x}-\code{y} \leq -3$.

\begin{example}\label{ex:dl:strict}
We revisit Example~\ref{ex:dl:simple} with strict semantics:
\marginlabel{%
  To inspect the output, invoke:\\
  \code{\mbox{~}clingo-dl \textbackslash\\ 
        \mbox{~~~}\attach{examples/dl1.lp}{dl1.lp} 0 \textbackslash\\
        \mbox{~~~}--strict}
}
\begin{lstlisting}[numbers=none]
clingo-dl version 1.0.0
Reading from dl1.lp
Solving...
Answer: 1
dl(x,"0") dl(y,"0")
Answer: 2
dl(x,"0") dl(y,"3") a
SATISFIABLE

Models       : 2
Calls        : 1
...
\end{lstlisting}
As we can see, the answer set without \code{a} shows an assignment for \code{x} and \code{y},
0 for both of them, since the difference constraint $\code{x}-\code{y}\leq2$ has to be satisfied.

Now, we extend the example slightly by adding the fact that difference constraint $\code{x}-\code{y}\leq -4$ has to be satisfied:
\lstinputlisting{examples/dl2.lp}
Running this example with strict semantics results in the following output:
\marginlabel{%
  To inspect the output, invoke:\\
  \code{\mbox{~}clingo-dl \textbackslash\\ 
        \mbox{~~~}\attach{examples/dl2.lp}{dl2.lp} 0 \textbackslash\\
        \mbox{~~~}--strict}
}
\begin{lstlisting}[numbers=none]
clingo-dl version 1.0.0
Reading from dl2.lp
Solving...
Answer: 1
dl(x,"0") dl(y,"4") a
SATISFIABLE

Models       : 1
Calls        : 1
...
\end{lstlisting}

Only the answer set with \code{a} remains and the assignment of \code{y} changes to 4 
since both $\code{x}-\code{y}\leq -3$ and $\code{x}-\code{y}\leq -4$ have to be fulfilled.
If \code{a} is false, difference constraints $\code{x}-\code{y}\leq -4$ and $\code{y}-\code{x}\leq 2$ would have to be satisfied,
the first due to the fact in Line~2 and the second due to strict semantics and $\code{\&diff\text{ }\{x-y\}\text{ }<=\text{ }-3}$ being false.
Since there does not exist a valid assignment fulfilling those two constraints, there cannot be an answer set with \code{a} being false.

\end{example}

Let us now consider the usefulness of strict and non-strict semantics in different scenarios.
As a rule of thumb, using difference constraint atoms in the head of rules fits the non-strict semantics 
while usage in the body the strict one.

\begin{example}\label{ex:dl:se}
See following example:
\lstinputlisting{examples/dl3.lp}
Running this example with strict semantics results in the following output:
\marginlabel{%
  To inspect the output, invoke:\\
  \code{\mbox{~}clingo-dl \textbackslash\\ 
        \mbox{~~~}\attach{examples/dl3.lp}{dl3.lp} 0 \textbackslash\\
        \mbox{~~~}--strict}
}

\begin{lstlisting}[numbers=none]
clingo-dl version 1.0.0
Reading from examples/dl3.lp
Solving...
Answer: 1
dl(x,"0") dl(y,"4") a
SATISFIABLE

Models       : 1
Calls        : 1
...
\end{lstlisting}

This constitutes the expected result 
where the only possible answer set contains \code{a} since $\code{x}-\code{y}\leq-4$
has to be satisfied, which implies that $\code{x}-\code{y}\leq-3$ is also satisfied,
which in turn derives \code{a}.

However, switching to non-strict semantics produces a different result:
\marginlabel{%
  To inspect the output, invoke:\\
  \code{\mbox{~}clingo-dl \textbackslash\\ 
        \mbox{~~~}\attach{examples/dl3.lp}{dl3.lp} 0}
}

\begin{lstlisting}[numbers=none]
clingo-dl version 1.0.0
Reading from examples/dl3.lp
Solving...
Answer: 1
dl(x,"0") dl(y,"4")
Answer: 2
dl(x,"0") dl(y,"4") a
SATISFIABLE

Models       : 2
Calls        : 1
...
\end{lstlisting}

Now, there are two answer sets instead of one. 
While both assignments fulfill $\code{x}-\code{y}\leq-4$ since it is a fact,
\code{a} is only derived in the second answer set.
Whenever a difference constraint atom exclusively appears in bodies of rules it is called \emph{external}.
This is the case for the difference constraint atom $\code{\&diff\text{ }\{x-y\}\text{ }<=\text{ }-3}$.
The truth value of an external difference constraint atom is determined by the QF-IDL theory and does not have to be derived by any rule.
In other words, every external difference constraint atom creates an implicit choice rule.
If $\code{\&diff\text{ }\{x-y\}\text{ }<=\text{ }-3}$ is chosen to be false, 
its negation $\code{y}-\code{x}\leq 2$ does not have to be satisfied in the non-strict case.
Therefore, it does not contradict $\code{x}-\code{y}\leq -4$ which always has to be satisfied in this example.

\end{example}

\begin{example}
\marginlabel{%
  To inspect the output, invoke:\\
  \code{\mbox{~}clingo-dl \attach{examples/flow.lp}{flow.lp} \textbackslash\\  
        \mbox{~~~}\attach{examples/shop.lp}{shop.lp.} 0\\
        \mbox{~~~}--strict}
}
Similarly, executing Example~\ref{ex:dl:fs} with strict semantics leads to undesired results.
In this case, the program is unsatisfiable.
Consider tasks \code{a} and \code{b} and the ground rules that sequentialize them:
\begin{lstlisting}[numbers=none]
&diff {(a,1)-(b,1)} <= -3 :- seq((a,1),(b,1),3).
&diff {(b,1)-(a,1)} <= -1 :- seq((b,1),(a,1),1).
&diff {(a,2)-(b,2)} <= -4 :- seq((a,2),(b,2),4).
&diff {(b,2)-(a,2)} <= -6 :- seq((b,2),(a,2),6).
\end{lstlisting}
Note that among the first two and last two rule bodies exactly one of them has to be true, respectively,
one signifying \code{a} is executed before \code{b} and the other vice versa.
This means that for both pairs of rules, one head difference constraint atom is true and the other is false.
If \code{a} is before \code{b} and strict semantics is enabled, 
the first two rules lead to a conflict because difference constraints $\code{(a,1)}-\code{(b,1)}\leq -3$ and $\code{(b,1)}-\code{(a,1)}\leq 0$ constitute a contradiction.
Similarly, \code{b} before \code{a} is impossible due to the last two rules
requiring $\code{(b,2)}-\code{(a,2)}\leq -6$ and $\code{(a,2)}-\code{(b,2)}\leq 3$ to be satisfied simultaneously.
Therefore, the whole program is unsatisfiable.
\end{example}

The previous examples, illustrate that either \emph{non-strict semantics with difference constraint atoms in the head} or
\emph{non-strict semantics with difference constraint atoms in the body} is best practice when working with \clingoM{DL}.
Note that this only applies to non-fact difference constraint atoms since facts behave the same way under either semantics.
In practice, non-strict semantics has a performance advantage.
Using it, one only has to monitor difference constraints represented by difference constraint atoms occurring in the logic program.
Strict semantics, on the other hand, has to consider twice the constraints internally, the original constraint and its negation.

Note that it is possible to translate one semantics into the other.
For example, using non-strict semantics with rules of the form 
  \begin{align*}
    \code{\&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$ :- $L_1$,$\dots$,$L_n$.}
  \end{align*}
can be translated to integrity constraints with strict semantics
  \begin{align*}
    \code{:- not \&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$, $L_1$,$\dots$,$L_n$.}
  \end{align*}
achieving the same behavior.
Similarly, rules in strict semantics that derive information using difference constraint atoms in the body
  \begin{align*}
    \code{$H$ :- \&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$, $L_1$,$\dots$,$L_n$.}
  \end{align*}
can be modeled using non-strict semantics by introducing auxiliary variables:
  \begin{align*}
    \code{\{aux\}.}\\
    \code{\&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$ :- aux.}\\
    \code{$H$ :- aux, $L_1$,$\dots$,$L_n$.}
  \end{align*}
Those are not general translations but rather guiding examples on how either semantics of choice might be used to achieve the same results.
The latter translation shows the advantage of strict semantics for modeling with difference constraints in rule bodies to derive information.
Only one intuitive rule is needed, whereas a choice and an auxiliary atom has to be introduced in the non-strict setting.
In our experience, the performance advantage using non-strict semantics outweighs the modeling inconvenience.

\paragraph{Quantifier-free Real Difference Logic (QF-RDL)}

Whenever option \code{--rdl} is enabled, the domain of variables and constants are real numbers.
In detail, for a difference constraint atom
 \[
    \code{\&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$}
 \]
 $x$ and $y$ are now real variables and $k$ is a string representation of the real constant.
For example, $\code{x}-\code{y}\leq -3.25$ would be modeled by the difference constraint atom
 \[
    \code{\&diff\text{ }\{x-y\}\text{ }<=\text{ }"-3.25"}
 \]
Note that \clingoM{DL} currently does not support \code{--rdl} and \code{--strict} simultaneously,
because the exact negation of a real difference constraint cannot be automatically calculated.

\subsubsection{Modeling with Difference Constraints}

\clingoM{DL} requires the user to be familiar with the capabilities and limitations of modeling using difference constraints.
While it is, for example, not possible to express inequalities with more then three variables or variables with coefficients unequal one,
a lot of common linear constraints can be easily expressed.
The following table shows general rules with commonly used linear constraints and their \clingoM{DL} counterpart.
Here, we consider linear constraints over integers.

\begin{center}
\begin{tabular}{l|l}
\textbf{Rule with linear constraint} & \clingoM{DL}\\\hline
\code{$x\leq k$ $\leftarrow$ $L_1$,$\dots$,$L_n$} & \code{\&diff\text{ }\{$x$-0\}\text{ }<=\text{ }$k$ :- $L_1$,$\dots$,$L_n$.}\\
\code{$x<k$ $\leftarrow$ $L_1$,$\dots$,$L_n$}     & \code{\&diff\text{ }\{$x$-0\}\text{ }<=\text{ }V :- V=$k$-1,$L_1$,$\dots$,$L_n$.}\\
\code{$x\geq k$ $\leftarrow$ $L_1$,$\dots$,$L_n$} & \code{\&diff\text{ }\{0-$x$\}\text{ }<=\text{ }$-k$ :- $L_1$,$\dots$,$L_n$.}\\
\code{$x>k$ $\leftarrow$ $L_1$,$\dots$,$L_n$}     & \code{\&diff\text{ }\{$x$-0\}\text{ }<=\text{ }V :- V=$k$-1,$L_1$,$\dots$,$L_n$.}\\
\code{$x\leq y+k$ $\leftarrow$ $L_1$,$\dots$,$L_n$}   & \code{\&diff\text{ }\{$x$-$y$\}\text{ }<=\text{ }$k$ :- $L_1$,$\dots$,$L_n$.}\\
\code{$x\geq y+k$ $\leftarrow$ $L_1$,$\dots$,$L_n$}   & \code{\&diff\text{ }\{$y$-$x$\}\text{ }<=\text{ }$-k$ :- $L_1$,$\dots$,$L_n$.}
\end{tabular}
\end{center}


\subsection{ASP and Linear Constraints}
\label{sec:linear:constraints}

\begin{itemize}
\item Literature: \cite{jakaosscscwa17a}
\item URL: \url{http://github.com/potassco/clingoLP}
\item Description: \clingoM{LP} 
  \begin{itemize}
  \item deals with integer and real variables
  \item relies on \cplex{} and \lpsolve{}, respectively
  \end{itemize}
\end{itemize}


\subsection{ASP and Constraint Programming}\label{sec:constraint}

\subsubsection{ASP and Constraint Programming with \clingcon}
\label{sec:clingcon}

\begin{itemize}
\item URL: \url{http://potassco.org/clingcon}
\item Literature: \cite{bakaossc16a}
\item Description: \clingoM{LP} 
  \begin{itemize}
  \item deals with integer variables
  \item uses propagators for lazy constraint propagation (based on the order-encoding) 
  \end{itemize}
\end{itemize}

\subsubsection{ASP and Constraint Programming with \gringo}

Grounder \gringo\ features some \textcolor{red}{experimental} means for expressing finite linear constraint satisfaction problems within ASP's modeling language.
The linear constraints are compiled into normal rules following the order encoding \cite{tatakiba09a,bageinscsotawe13a}.
Hence, off-the-shelf ASP solvers like \clasp\ can be used to solve such problems.

CSP constraints in gringo are build over \emph{constraint terms}, which have form
\[\code{$c_1$~\$*~\$$v_1$~\$+~$\cdots$~\$+~$c_n$~\$*~\$$v_n$}\]
where $n>0$, and each $c_i$ (integer factor) and $v_i$ (name of a constraint variable) are terms.
If a factor is one, then the `\code{$c_i$ \$*}' part can be omitted.
Similarly, it is possible to just add a factor in which case the `\code{\$* $v_i$}' part can be omitted.

\emph{Linear constraints} in \gringo\ are syntactically similar to built-in comparison predicates (cf.\ Section~\ref{subsec:gringo:comp})
but relation symbols have to be preceded with a \code{\$} symbol
\[\code{$t_0$~\$$\prec_1$~$\cdots$~\$$\prec_{n}$~$t_n$}\]
where $n>0$, each $\prec_i$ is a comparison predicate, and each $t_i$ is a constraint term.

In addition, there is the global \emph{disjoint constraint}
\[\code{\#disjoint~\{~$\boldsymbol{t}_1$:$c_1$:$\boldsymbol{L}_1$;$\dots$;$\boldsymbol{t}_n$:$c_n$:$\boldsymbol{L}_n$~\}}\]
where $n\geq 0$, $\boldsymbol{t}_i$ and $\boldsymbol{L}_i$ are given as in Section~\ref{subsec:gringo:aggregate},
and each $c_i$ is a constraint term.
%
The idea is that sets of values labeled with the same term(s) must be disjoint.

\begin{example}\label{ex:csp:queens1}
\marginlabel{To compute both answer sets, invoke:\\
  \code{\mbox{~}clingo \attach{examples/queensC.lp}{queensC.lp} \textbackslash\\
         \mbox{~} -c n=30}\\
  or alternatively:\\
  \code{\mbox{~}gringo~\attach{examples/queensC.lp}{queensC.lp} \textbackslash\\
        \mbox{~} -c n=30 | clasp 0}
}
For illustration,
consider the following encoding of the $n$-queens puzzle:
\lstinputlisting{examples/queensC.lp}

The first line fixes the domain of the integer variables
\code{\$queen(1)} to \code{\$queen(n)}.
Line~3 forbids queens on the same columns and the last two lines address queens on the same diagonals.
\end{example}

\begin{example}
The next encoding uses the global \code{\#disjoint} constraint:
%
\marginlabel{To compute both answer sets, invoke:\\
  \code{\mbox{~}clingo \attach{examples/queensCa.lp}{queensCa.lp} \textbackslash\\
         \mbox{~} -c n=300}\\
  or alternatively:\\
  \code{\mbox{~}gringo~\attach{examples/queensCa.lp}{queensCa.lp} \textbackslash\\
        \mbox{~} -c n=300 | clasp 0}
}
%
\lstinputlisting{examples/queensCa.lp}
\end{example}

\begin{note}
The \textcolor{red}{current} implementation of constraints in \gringo\ requires 
that all constraint variables appearing in a program must have finite domains inferable from the grounded program.
Hence, rules like in Line~1 of Example~\ref{ex:csp:queens1} fixing the domain of a constraint variable have to be added for each constraint variable.
\end{note}

\subsubsection{Solving CSPs with \aspartame}
\label{sec:aspartame}

This section is not yet ready for publishing
and will be included in one of the forthcoming editions of this guide.

Information on constraint programming with \aspartame\ can be obtained at the following references.

\begin{itemize}
\item URL
\begin{itemize}
\item \url{http://potassco.org/labs}
\item \url{http://www.cs.uni-potsdam.de/aspartame}
\end{itemize}
\item Literature: \cite{bageinscsotawe13a}
\item Description: \aspartame\ solves finite linear CSPs (in XCSP and \sugar{} format) in ASP
\end{itemize}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: "guide"
%%% End: