1% BEGIN LICENSE BLOCK
2% Version: CMPL 1.1
3%
4% The contents of this file are subject to the Cisco-style Mozilla Public
5% License Version 1.1 (the "License"); you may not use this file except
6% in compliance with the License.  You may obtain a copy of the License
7% at www.eclipse-clp.org/license.
8% 
9% Software distributed under the License is distributed on an "AS IS"
10% basis, WITHOUT WARRANTY OF ANY KIND, either express or implied.  See
11% the License for the specific language governing rights and limitations
12% under the License. 
13% 
14% The Original Code is  The ECLiPSe Constraint Logic Programming System. 
15% The Initial Developer of the Original Code is  Cisco Systems, Inc. 
16% Portions created by the Initial Developer are
17% Copyright (C) 2006 Cisco Systems, Inc.  All Rights Reserved.
18% 
19% Contributor(s): Kish Shen, IC-Parc
20% 
21% END LICENSE BLOCK
22
23% $Id: solverinter.tex,v 1.2 2013/03/14 21:25:22 jschimpf Exp $
24% Author:		Kish Shen
25
26
27\chapter{Common Solver Interface}
28%HEVEA\cutdef[1]{section}
29\index{common solver interface|(}
30
31\section{Introduction}
32\eclipse\ now provides a common syntax for the main arithmetic constraints
33provided by different constraint solvers.
34The basic idea is that the name and syntax of the constraint determines the
35declarative meaning, while the operational semantics (the algorithmic
36constraint behaviour) is determined by the module which implements the
37constraint.
38This principle simplifies the development of applications that use
39hybrid solution methods. Constraints can be passed easily to different,
40even multiple, solvers.
41
42
43\section{Common constraints}
44
45The constraints can be divided into the following groups:
46\begin{itemize}
47\item the numeric type constraints reals/1 and integers/1.
48    Note that in this context, integers are considered a subset of the reals.
49
50\item the range cnstraints ::/2, \verb'#::' and \$::/2, which give upper
51    and lower bounds to their variables.
52    In addition, \verb'#::' also implies integrality.
53
54\item arithmetic equality, inequality and disequality over the mathematical
55    real numbers, e.g.
56    \verb'$=', \verb'$>=', \verb'>', \verb'$\='.
57    Note that in this context,
58    integers are considered a subset of the reals and can therefore
59    occur in these constraints.
60
61\item arithmetic equality, inequality and disequality which in addition to
62    the above constrain all variables within their arguments to integers.
63    Syntactically, these generally have a leading \verb'#',
64    e.g.\ \verb'#=', \verb'#\=', \verb'#<'.
65\end{itemize}
66
67
68\begin{table}
69%\begin{minipage}{\textwidth}
70\begin{center}
71\begin{toimage}
72\begin{tabular}{|l||c|c|c|c|c|c|c|c|}
73\hline
74       &              &              &             & \verb'#::/2' &                   & \\
75       &              &              &             & \verb'#=/2'  &                   & \\
76       &              &              &             & \verb'#>=/2' &                   & \\
77       & \verb'$::2'  &              &             & \verb'#=</2' &                   & \\
78       & \verb'$=/2'  & \verb'$>/2'  &             & \verb'#>/2'  &                   & \\
79       & \verb'$>=/2' & \verb'$</2'  &             & \verb'#</2'  &                   & \\
80       & \verb'$=</2' & \verb'$\=/2' & \verb'::/2' & \verb'#\=/2' & \verb'integers/1' & \verb'reals/1' \\
81\hline
82\hline
83suspend	& yes & yes & yes & yes & yes & yes \\
84\hline                          
85ic	& yes & yes & yes & yes & yes & yes \\
86\hline                          
87fd	& --- & yes & yes & yes & yes & --- \\
88\hline                          
89gfd	& --- & yes & yes & yes & yes & --- \\
90\hline                          
91eplex	& yes & --- & yes & --- & yes & yes \\
92\hline                          
93colgen	& yes & --- & yes & --- & --- & yes \\
94\hline                          
95\hline
96\end{tabular}
97\end{toimage}\imageflush
98\end{center}
99{\small
100    \begin{itemize}
101    \item If integer bounds are given to the eplex version of \verb'::/2' 
102    the external solver does not consider this as an integrality constraint
103    and only solves the continuous relaxation which can then be rounded
104    to the next integer.  To make the external solver solve a mixed
105    integer problem, use the eplex version of integers/1.
106    \end{itemize}
107}
108%\end{minipage}
109\caption{Supported constraints for various arithmetic solvers}
110\label{commoncons}
111\end{table}
112Not all constraints are supported by all the solvers. For example, the
113eplex solver does not support any strict inequality constraints.
114Table~\ref{commoncons} shows the constraints that are available
115from the various constraint solvers.
116In the table, a `yes' entry indicates that the
117particular constraint is supported by the particular solver. Note
118that some further restrictions may apply for a particular solver. For
119example, the eplex solver can only handle linear expressions. Refer
120to the documentation for each individual solver to see what restrictions
121might apply.
122
123Note that the `standard arithmetic' operators
124\verb'=:=/2', \verb'=\=/2', \verb'>=/2', \verb'=</2', \verb'>/2' and \verb'</2'
125which are automatically imported from the {\tt eclipse_language} module
126are declaratively the same as the corresponding '\$' constraints.
127On the other hand, they are not interchangeable because they
128can only be used as tests (when all variables are instantiated),
129not as active constraints. 
130
131
132\section{Using the constraints}
133
134To use the constraints, \eclipse\ needs to know which solver to pass a
135particular constraint to. The easiest method for doing this is to module
136qualify the constraint. For example,
137
138\begin{verbatim}
139    ..., ic: (A #>= B), ...
140\end{verbatim}
141
142\noindent
143passes the constraint \verb'A #>= B' to the ic solver. The solver must be
144loaded first (e.g. via lib/1) before any constraint can be passed to it.
145
146A constraint can also be passed to more than one solver by specifying a
147list in the module qualification. For example,
148
149\begin{verbatim}
150    ..., [ic, suspend]: (A #>= B), ...
151\end{verbatim}
152
153\noindent
154will pass the constraint to both the ic and suspend solvers. 
155
156Module qualification is {\em not} needed if the constraint is defined by an
157imported module, and there is no other imported module
158which defines the same constraint. For example, if ic is the only imported
159module which defines \verb'#>=/2', then \verb'#>=/2' can be used without 
160qualification:
161
162\begin{verbatim}
163    ..., A #>= B, ...
164\end{verbatim}
165
166Note that for constraints that are defined for \verb'eclipse_language',
167such as \verb'>=' (the standard arithmetic test), the default behaviour
168when an unqualified call to such a
169constraint is made is to pass it to \verb'eclipse_language',
170even if another solver which defines the constraint is imported.
171Thus, for example
172\begin{verbatim}
173    ..., A >= B, ...
174\end{verbatim}
175
176\noindent
177will by default have standard (i.e.\ non-suspending) test semantics, even
178if, e.g.\ the \verb'ic' library (which also defines \verb'>=/2') is
179imported. To access the \verb'ic' version, module qualification should
180be added:
181\begin{verbatim}
182    ..., ic:(A >= B), ...
183\end{verbatim}
184Alternatively, the synonymous \verb'$>=/2' constraint could be used:
185\begin{verbatim}
186    ..., A $>= B, ...
187\end{verbatim}
188
189In general, module qualifications are recommended if the programmer
190wants to ensure a particular constraint behaviour regardless of which
191other modules might be loaded.  On the other hand, if the intention is
192to switch easily between different solvers by simply loading a
193different library, module qualification is best omitted.
194
195Finally, it is also possible to let the running program determine which
196solver to use. In this case, the program has a variable in the module
197position, which will only be bound at runtime:
198\begin{verbatim}
199    ..., Solver:(A #>= B), ...
200\end{verbatim}
201This will however prevent the solver from performing any compile-time
202preprocessing on the constraint.
203
204
205
206\section{The Solvers}
207
208\begin{description}
209\item[\biptxtref{suspend}{lib(suspend)}{../bips/lib/suspend/index.html}]
210    This is the simplest possible 'solver'. Its behaviour is to wait until
211    all variables in a constraint have been instantiated to numbers.
212    Then it performs a test to check whether the constraint is satisfied,
213    and fails if this is not the case.
214
215\item[\biptxtref{ic}{lib(ic)}{../bips/lib/ic/index.html}]
216    A hybrid solver, combining integer and real interval constraint
217    solving.  This solver replaces the older FD solver.
218    For more information, please see chapter \ref{chapic}.
219
220\item[\biptxtref{gfd}{lib(gfd)}{../bips/lib/gfd/index.html}]
221    An integer finite domain solver, implemented via interfacing
222    to the third party Gecode software.
223    For more information, please see chapter \ref{chapgfd}.
224
225\item[\biptxtref{fd}{lib(fd)}{../bips/lib/fd/index.html}]
226    Obsolescent integer finite domain solver.
227
228\item[\biptxtref{eplex}{lib(eplex)}{../bips/lib/eplex/index.html}]
229    An interface to an LP or MIP solver, i.e.\ it implements linear
230    constraints over reals or integers.
231
232%\item[\biptxtref{fdplex}{lib(fdplex)}{../bips/lib/fdplex/index.html}]
233%    An example of a hybrid solver that combines the fd and eplex solvers.
234
235\item[standard arithmetic]
236    This is not really a solver, but just the implementation of simple
237    arithmetic tests in module {\tt eclipse_language}. These require
238    that all variables are instantiated when the test is invoked.
239    The reason to list it here is that the arithmetic constraints
240    can be considered generalisations of these traditional tests.
241\end{description}
242\index{common solver interface|)}
243
244%HEVEA\cutend