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