/usr/lib/swi-prolog/doc/Manual/clpfd.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">

<html>
<head>
<title>SWI-Prolog 7.1.10 Reference Manual: Section A.7</title><link rel="home" href="index.html">
<link rel="contents" href="Contents.html">
<link rel="index" href="DocIndex.html">
<link rel="summary" href="summary.html">
<link rel="previous" href="check.html">
<link rel="next" href="clpqr.html">

<style type="text/css">

/* Style sheet for SWI-Prolog latex2html
*/

dd.defbody
{ margin-bottom: 1em;
}

dt.pubdef, dt.multidef
{ color: #fff;
padding: 2px 10px 0px 10px;
margin-bottom: 5px;
font-size: 18px;
vertical-align: middle;
overflow: hidden;
}

dt.pubdef { background-color: #0c3d6e; }
dt.multidef { background-color: #ef9439; }

.bib dd
{ margin-bottom: 1em;
}

.bib dt
{ float: left;
margin-right: 1.3ex;
}

pre.code
{ margin-left: 1.5em;
margin-right: 1.5em;
border: 1px dotted;
padding-top: 5px;
padding-left: 5px;
padding-bottom: 5px;
background-color: #f8f8f8;
}

div.navigate
{ text-align: center;
background-color: #f0f0f0;
border: 1px dotted;
padding: 5px;
}

div.title
{ text-align: center;
padding-bottom: 1em;
font-size: 200%;
font-weight: bold;
}

div.author
{ text-align: center;
font-style: italic;
}

div.abstract
{ margin-top: 2em;
background-color: #f0f0f0;
border: 1px dotted;
padding: 5px;
margin-left: 10%; margin-right:10%;
}

div.abstract-title
{ text-align: center;
padding: 5px;
font-size: 120%;
font-weight: bold;
}

div.toc-h1
{ font-size: 200%;
font-weight: bold;
}

div.toc-h2
{ font-size: 120%;
font-weight: bold;
margin-left: 2em;
}

div.toc-h3
{ font-size: 100%;
font-weight: bold;
margin-left: 4em;
}

div.toc-h4
{ font-size: 100%;
margin-left: 6em;
}

span.sec-nr
{
}

span.sec-title
{
}

span.pred-ext
{ font-weight: bold;
}

span.pred-tag
{ float: right;
padding-top: 0.2em;
font-size: 80%;
font-style: italic;
color: #fff;
}

div.caption
{ width: 80%;
margin: auto;
text-align:center;
}

/* Footnotes */
.fn {
color: red;
font-size: 70%;
}

.fn-text, .fnp {
position: absolute;
top: auto;
left: 10%;
border: 1px solid #000;
box-shadow: 5px 5px 5px #888;
display: none;
background: #fff;
color: #000;
margin-top: 25px;
padding: 8px 12px;
font-size: larger;
}

sup:hover span.fn-text
{ display: block;
}

/* Lists */

dl.latex
{ margin-top: 1ex;
margin-bottom: 0.5ex;
}

dl.latex dl.latex dd.defbody
{ margin-bottom: 0.5ex;
}

/* PlDoc Tags */

dl.tags
{ font-size: 90%;
margin-left: 5ex;
margin-top: 1ex;
margin-bottom: 0.5ex;
}

dl.tags dt
{ margin-left: 0pt;
font-weight: bold;
}

dl.tags dd
{ margin-left: 3ex;
}

td.param
{ font-style: italic;
font-weight: bold;
}

/* Index */

dt.index-sep
{ font-weight: bold;
font-size: +1;
margin-top: 1ex;
}

/* Tables */

table.center
{ margin: auto;
}

table.latex
{ border-collapse:collapse;
}

table.latex tr
{ vertical-align: text-top;
}

table.latex td,th
{ padding: 2px 1em;
}

table.latex tr.hline td,th
{ border-top: 1px solid black;
}

table.frame-box
{ border: 2px solid black;
}

</style>
</head>
<body style="background:white">
<div class="navigate"><a class="nav" href="index.html"><img src="home.gif" alt="Home"></a>
<a class="nav" href="Contents.html"><img src="index.gif" alt="Contents"></a>
<a class="nav" href="DocIndex.html"><img src="yellow_pages.gif" alt="Index"></a>
<a class="nav" href="summary.html"><img src="info.gif" alt="Summary"></a>
<a class="nav" href="check.html"><img src="prev.gif" alt="Previous"></a>
<a class="nav" href="clpqr.html"><img src="next.gif" alt="Next"></a>
</div>
<h2 id="sec:clpfd"><a id="sec:A.7"><span class="sec-nr">A.7</span> <span class="sec-title">library(clpfd): 
Constraint Logic Programming over Finite Domains</span></a></h2>

<p><a id="sec:clpfd"></a>

<dl class="tags">
<dt class="tag">author</dt>
<dd>
Markus Triska
</dd>
</dl>

<p>

<h4><a id="sec:A.7.1"><span class="sec-nr">A.7.1</span> <span class="sec-title">Introduction</span></a></h4>

<p>Constraint programming is a declarative formalism that lets you 
describe conditions a solution must satisfy. This library provides 
CLP(FD), Constraint Logic Programming over Finite Domains. It can be 
used to model and solve various combinatorial problems such as planning, 
scheduling and allocation tasks.

<p>Most predicates of this library are finite domain <i>constraints</i>, 
which are relations over integers. They generalise arithmetic evaluation 
of integer expressions in that propagation can proceed in all 
directions. This library also provides <i>enumeration</i> <i>predicates</i>, 
which let you systematically search for solutions on variables whose 
domains have become finite.

<p>You can cite this library in your publications as:

<pre class="code">
@inproceedings{Triska12,
  author    = {Markus Triska},
  title     = {The Finite Domain Constraint Solver of {SWI-Prolog}},
  booktitle = {FLOPS},
  series    = {LNCS},
  volume    = {7294},
  year      = {2012},
  pages     = {307-316}
}
</pre>

<p>

<h4><a id="sec:A.7.2"><span class="sec-nr">A.7.2</span> <span class="sec-title">Arithmetic 
constraints</span></a></h4>

<p>A finite domain <i>arithmetic expression</i> is one of:
<blockquote>
<table class="latex frame-box">
<tr><td><i>integer</i> </td><td>Given value </td></tr>
<tr><td><i>variable</i> </td><td>Unknown integer </td></tr>
<tr><td>?(<i>variable</i>)</td><td>Unknown integer </td></tr>
<tr><td>-Expr</td><td>Unary minus </td></tr>
<tr><td>Expr + Expr</td><td>Addition </td></tr>
<tr><td>Expr * Expr</td><td>Multiplication </td></tr>
<tr><td>Expr - Expr</td><td>Subtraction </td></tr>
<tr><td>Expr <code>^</code> Expr</td><td>Exponentiation </td></tr>
<tr><td><code>min(Expr,Expr)</code> </td><td>Minimum of two expressions </td></tr>
<tr><td><code>max(Expr,Expr)</code> </td><td>Maximum of two expressions </td></tr>
<tr><td>Expr mod Expr</td><td>Modulo induced by floored division </td></tr>
<tr><td>Expr rem Expr</td><td>Modulo induced by truncated division </td></tr>
<tr><td><code>abs(Expr)</code> </td><td>Absolute value </td></tr>
<tr><td>Expr / Expr</td><td>Truncated integer division </td></tr>
</table>
</blockquote>

<p>Arithmetic <i>constraints</i> are relations between arithmetic 
expressions.

<p>The most important arithmetic constraints are:
<blockquote>
<table class="latex frame-box">
<tr><td>Expr1 <code>#&gt;=</code> Expr2</td><td>Expr1 is greater than or 
equal to Expr2 </td></tr>
<tr><td>Expr1 <code>#=&lt;</code> Expr2</td><td>Expr1 is less than or 
equal to Expr2 </td></tr>
<tr><td>Expr1 <code>#=</code> Expr2</td><td>Expr1 equals Expr2 </td></tr>
<tr><td>Expr1 <code>#\=</code> Expr2</td><td>Expr1 is not equal to Expr2 </td></tr>
<tr><td>Expr1 <code>#&gt;</code> Expr2</td><td>Expr1 is greater than 
Expr2 </td></tr>
<tr><td>Expr1 <code>#&lt;</code> Expr2</td><td>Expr1 is less than Expr2 </td></tr>
</table>
</blockquote>

<p>

<h4><a id="sec:A.7.3"><span class="sec-nr">A.7.3</span> <span class="sec-title">Reification</span></a></h4>

<p>The constraints <a class="pred" href="clpfd.html#in/2">in/2</a>, <a class="pred" href="clpfd.html##=/2">#=/2</a>, <a class="pred" href="clpfd.html##\=/2">#\=/2</a>, <a class="pred" href="clpfd.html##</2">#&lt;/2</a>, <a class="pred" href="clpfd.html##>/2">#&gt;/2</a>, <a class="pred" href="clpfd.html##=</2">#=&lt;/2</a>, 
and <a class="pred" href="clpfd.html##>=/2">#&gt;=/2</a> can be
<i>reified</i>, which means reflecting their truth values into Boolean 
values represented by the integers 0 and 1. Let P and Q denote reifiable 
constraints or Boolean variables, then:
<blockquote>
<table class="latex frame-box">
<tr><td><code>#\</code> Q</td><td>True iff Q is false </td></tr>
<tr><td>P <code>#\/</code> Q</td><td>True iff either P or Q </td></tr>
<tr><td>P <code>#/\</code> Q</td><td>True iff both P and Q </td></tr>
<tr><td>P <code>#&lt;==&gt;</code> Q</td><td>True iff P and Q are 
equivalent </td></tr>
<tr><td>P <code>#==&gt;</code> Q</td><td>True iff P implies Q </td></tr>
<tr><td>P <code>#&lt;==</code> Q</td><td>True iff Q implies P </td></tr>
</table>
</blockquote>

<p>The constraints of this table are reifiable as well.

<p>

<h4><a id="sec:A.7.4"><span class="sec-nr">A.7.4</span> <span class="sec-title">Examples</span></a></h4>

<p>Here is an example session with a few queries and their answers:

<pre class="code">
?- use_module(library(clpfd)).
% library(clpfd) compiled into clpfd 0.06 sec, 633,732 bytes
true.

?- X #&gt; 3.
X in 4..sup.

?- X #\= 20.
X in inf..19\/21..sup.

?- 2*X #= 10.
X = 5.

?- X*X #= 144.
X in -12\/12.

?- 4*X + 2*Y #= 24, X + Y #= 9, [X,Y] ins 0..sup.
X = 3,
Y = 6.

?- Vs = [X,Y,Z], Vs ins 1..3, all_different(Vs), X = 1, Y #\= 2.
Vs = [1, 3, 2],
X = 1,
Y = 3,
Z = 2.

?- X #= Y #&lt;==&gt; B, X in 0..3, Y in 4..5.
B = 0,
X in 0..3,
Y in 4..5.
</pre>

<p>In each case, and as for all pure programs, the answer is 
declaratively equivalent to the original query, and in many cases the 
constraint solver has deduced additional domain restrictions.

<p>

<h4><a id="sec:A.7.5"><span class="sec-nr">A.7.5</span> <span class="sec-title">Search</span></a></h4>

<p>A common usage of this library is to first post the desired 
constraints among the variables of a model, and then to use enumeration 
predicates to search for solutions. As an example of a constraint 
satisfaction problem, consider the cryptoarithmetic puzzle SEND + MORE = 
MONEY, where different letters denote distinct integers between 0 and 9. 
It can be modeled in CLP(FD) as follows:

<pre class="code">
:- use_module(library(clpfd)).

puzzle([S,E,N,D] + [M,O,R,E] = [M,O,N,E,Y]) :-
        Vars = [S,E,N,D,M,O,R,Y],
        Vars ins 0..9,
        all_different(Vars),
                  S*1000 + E*100 + N*10 + D +
                  M*1000 + O*100 + R*10 + E #=
        M*10000 + O*1000 + N*100 + E*10 + Y,
        M #\= 0, S #\= 0.
</pre>

<p>Sample query and its result (actual variables replaced for 
readability):

<pre class="code">
?- puzzle(As+Bs=Cs).
As = [9, _A2, _A3, _A4],
Bs = [1, 0, _B3, _A2],
Cs = [1, 0, _A3, _A2, _C5],
_A2 in 4..7,
all_different([9, _A2, _A3, _A4, 1, 0, _B3, _C5]),
1000*9+91*_A2+ -90*_A3+_A4+ -9000*1+ -900*0+10*_B3+ -1*_C5#=0,
_A3 in 5..8,
_A4 in 2..8,
_B3 in 2..8,
_C5 in 2..8.
</pre>

<p>Here, the constraint solver has deduced more stringent bounds for all 
variables. It is good practice to keep the modeling part separate from 
the actual search. This lets you observe termination and determinism 
properties of the modeling part in isolation from the search. Labeling 
can then be used to search for solutions in a separate predicate or 
goal:

<pre class="code">
?- puzzle(As+Bs=Cs), label(As).
As = [9, 5, 6, 7],
Bs = [1, 0, 8, 5],
Cs = [1, 0, 6, 5, 2] ;
false.
</pre>

<p>In this case, it suffices to label a subset of variables to find the 
puzzle's unique solution, since the constraint solver is strong enough 
to reduce the domains of remaining variables to singleton sets. In 
general though, it is necessary to label all variables to obtain ground 
solutions.

<p>

<h4><a id="sec:A.7.6"><span class="sec-nr">A.7.6</span> <span class="sec-title">Declarative 
integer arithmetic</span></a></h4>

<p>You can also use CLP(FD) constraints as a more declarative 
alternative for ordinary integer arithmetic with <a class="pred" href="arith.html#is/2">is/2</a>, <a class="pred" href="arith.html#>/2">&gt;/2</a> 
etc. For example:

<pre class="code">
:- use_module(library(clpfd)).

n_factorial(0, 1).
n_factorial(N, F) :-
        N #&gt; 0, N1 #= N - 1, F #= N * F1,
        n_factorial(N1, F1).
</pre>

<p>This predicate can be used in all directions. For example:

<pre class="code">
?- n_factorial(47, F).
F = 258623241511168180642964355153611979969197632389120000000000 ;
false.

?- n_factorial(N, 1).
N = 0 ;
N = 1 ;
false.

?- n_factorial(N, 3).
false.
</pre>

<p>To make the predicate terminate if any argument is instantiated, add 
the (implied) constraint F <code>#\=</code> 0 before the recursive call. 
Otherwise, the query <code>n_factorial(N, 0)</code> is the only 
non-terminating case of this kind.

<p>

<h4><a id="sec:A.7.7"><span class="sec-nr">A.7.7</span> <span class="sec-title">Advanced 
topics</span></a></h4>

<p>This library uses <a class="pred" href="consulting.html#goal_expansion/2">goal_expansion/2</a> 
to rewrite constraints at compilation time. The expansion's aim is to 
transparently bring the performance of CLP(FD) constraints close to that 
of conventional arithmetic predicates (<a class="pred" href="arith.html#</2">&lt;/2</a>, <a class="pred" href="arith.html#=:=/2">=:=/2</a>, <a class="pred" href="arith.html#is/2">is/2</a> 
etc.) when the constraints are used in modes that can also be handled by 
built-in arithmetic. To disable the expansion, set the flag <code>clpfd_goal_expansion</code> 
to <code>false</code>.

<p>If you set the flag <code>clpfd_monotonic</code> to <code>true</code>, 
then CLP(FD) is monotonic: Adding new constraints cannot yield new 
solutions. When this flag is <code>true</code>, you must wrap variables 
that occur in arithmetic expressions with the functor <code>(?)/1</code>. 
For example, <code>?(X) #= ?(Y) + ?(Z)</code>. The wrapper can be 
omitted for variables that are already constrained to integers.

<p>Use <a class="pred" href="coroutining.html#call_residue_vars/2">call_residue_vars/2</a> 
and <a class="pred" href="attvar.html#copy_term/3">copy_term/3</a> to 
inspect residual goals and the constraints in which a variable is 
involved. This library also provides <i>reflection</i> predicates (like <a class="pred" href="clpfd.html#fd_dom/2">fd_dom/2</a>, <a class="pred" href="clpfd.html#fd_size/2">fd_size/2</a> 
etc.) with which you can inspect a variable's current domain. These 
predicates can be useful if you want to implement your own labeling 
strategies.

<p>You can also define custom constraints. The mechanism to do this is 
not yet finalised, and we welcome suggestions and descriptions of use 
cases that are important to you. As an example of how it can be done 
currently, let us define a new custom constraint <code>oneground(X,Y,Z)</code>, 
where Z shall be 1 if at least one of X and Y is instantiated:

<pre class="code">
:- use_module(library(clpfd)).

:- multifile clpfd:run_propagator/2.

oneground(X, Y, Z) :-
        clpfd:make_propagator(oneground(X, Y, Z), Prop),
        clpfd:init_propagator(X, Prop),
        clpfd:init_propagator(Y, Prop),
        clpfd:trigger_once(Prop).

clpfd:run_propagator(oneground(X, Y, Z), MState) :-
        (   integer(X) -&gt; clpfd:kill(MState), Z = 1
        ;   integer(Y) -&gt; clpfd:kill(MState), Z = 1
        ;   true
        ).
</pre>

<p>First, <span class="pred-ext">clpfd:make_propagator/2</span> is used 
to transform a user-defined representation of the new constraint to an 
internal form. With
<span class="pred-ext">clpfd:init_propagator/2</span>, this internal 
form is then attached to X and Y. From now on, the propagator will be 
invoked whenever the domains of X or Y are changed. Then, <span class="pred-ext">clpfd:trigger_once/1</span> 
is used to give the propagator its first chance for propagation even 
though the variables' domains have not yet changed. Finally, <span class="pred-ext">clpfd:run_propagator/2</span> 
is extended to define the actual propagator. As explained, this 
predicate is automatically called by the constraint solver. The first 
argument is the user-defined representation of the constraint as used in
<span class="pred-ext">clpfd:make_propagator/2</span>, and the second 
argument is a mutable state that can be used to prevent further 
invocations of the propagator when the constraint has become entailed, 
by using <span class="pred-ext">clpfd:kill/1</span>. An example of using 
the new constraint:

<pre class="code">
?- oneground(X, Y, Z), Y = 5.
Y = 5,
Z = 1,
X in inf..sup.
</pre>

<dl class="latex">
<dt class="pubdef"><a id="in/2"><var>?Var</var> <strong>in</strong> <var>+Domain</var></a></dt>
<dd class="defbody">
<var>Var</var> is an element of <var>Domain</var>. <var>Domain</var> is 
one of:

<dl class="latex">
<dt><strong><var>Integer</var></strong></dt>
<dd class="defbody">
Singleton set consisting only of <i><var>Integer</var></i>.
</dd>
<dt><var><var>Lower</var></var> <strong>..</strong> <var><var>Upper</var></var></dt>
<dd class="defbody">
All integers <i>I</i> such that <i><var>Lower</var></i> <code>=&lt;</code> <i>I</i> <code>=&lt;</code> <i><var>Upper</var></i>.
<i><var>Lower</var></i> must be an integer or the atom <b>inf</b>, which 
denotes negative infinity. <i><var>Upper</var></i> must be an integer or 
the atom <b>sup</b>, which denotes positive infinity.
</dd>
<dt><var><var>Domain1</var></var> <strong><code>\/</code></strong> <var><var>Domain2</var></var></dt>
<dd class="defbody">
The union of <var>Domain1</var> and <var>Domain2</var>.
</dd>
</dl>

</dd>
<dt class="pubdef"><a id="ins/2"><var>+Vars</var> <strong>ins</strong> <var>+Domain</var></a></dt>
<dd class="defbody">
The variables in the list <var>Vars</var> are elements of <var>Domain</var>.</dd>
<dt class="pubdef"><a id="indomain/1"><strong>indomain</strong>(<var>?Var</var>)</a></dt>
<dd class="defbody">
Bind <var>Var</var> to all feasible values of its domain on 
backtracking. The domain of <var>Var</var> must be finite.</dd>
<dt class="pubdef"><a id="label/1"><strong>label</strong>(<var>+Vars</var>)</a></dt>
<dd class="defbody">
Equivalent to <code>labeling([], Vars)</code>.</dd>
<dt class="pubdef"><a id="labeling/2"><strong>labeling</strong>(<var>+Options, 
+Vars</var>)</a></dt>
<dd class="defbody">
Assign a value to each variable in <var>Vars</var>. Labeling means 
systematically trying out values for the finite domain variables <var>Vars</var> 
until all of them are ground. The domain of each variable in <var>Vars</var> 
must be finite.
<var>Options</var> is a list of options that let you exhibit some 
control over the search process. Several categories of options exist:

<p>The variable selection strategy lets you specify which variable of
<var>Vars</var> is labeled next and is one of:

<dl class="latex">
<dt><strong>leftmost</strong></dt>
<dd class="defbody">
Label the variables in the order they occur in <var>Vars</var>. This is 
the default.
</dd>
<dt><strong>ff</strong></dt>
<dd class="defbody">
<i>First fail</i>. Label the leftmost variable with smallest domain 
next, in order to detect infeasibility early. This is often a good 
strategy.
</dd>
<dt><strong>ffc</strong></dt>
<dd class="defbody">
Of the variables with smallest domains, the leftmost one participating 
in most constraints is labeled next.
</dd>
<dt><strong>min</strong></dt>
<dd class="defbody">
Label the leftmost variable whose lower bound is the lowest next.
</dd>
<dt><strong>max</strong></dt>
<dd class="defbody">
Label the leftmost variable whose upper bound is the highest next.
</dd>
</dl>

<p>The value order is one of:

<dl class="latex">
<dt><strong>up</strong></dt>
<dd class="defbody">
Try the elements of the chosen variable's domain in ascending order. 
This is the default.
</dd>
<dt><strong>down</strong></dt>
<dd class="defbody">
Try the domain elements in descending order.
</dd>
</dl>

<p>The branching strategy is one of:

<dl class="latex">
<dt><strong>step</strong></dt>
<dd class="defbody">
For each variable X, a choice is made between X = V and X <code>#\=</code> 
V, where V is determined by the value ordering options. This is the 
default.
</dd>
<dt><strong>enum</strong></dt>
<dd class="defbody">
For each variable X, a choice is made between X = V_1, X = V_2 etc., for 
all values V_i of the domain of X. The order is determined by the value 
ordering options.
</dd>
<dt><strong>bisect</strong></dt>
<dd class="defbody">
For each variable X, a choice is made between X <code>#=&lt;</code> M 
and X <code>#&gt;</code> M, where M is the midpoint of the domain of X.
</dd>
</dl>

<p>At most one option of each category can be specified, and an option 
must not occur repeatedly.

<p>The order of solutions can be influenced with:

<p>
<ul class="compact">
<li><code>min(Expr)</code>
<li><code>max(Expr)</code>
</ul>

<p>This generates solutions in ascending/descending order with respect 
to the evaluation of the arithmetic expression Expr. Labeling <var>Vars</var> 
must make Expr ground. If several such options are specified, they are 
interpreted from left to right, e.g.:

<pre class="code">
?- [X,Y] ins 10..20, labeling([max(X),min(Y)],[X,Y]).
</pre>

<p>This generates solutions in descending order of X, and for each 
binding of X, solutions are generated in ascending order of Y. To obtain 
the incomplete behaviour that other systems exhibit with "<code>maximize(Expr)</code>" 
and "<code>minimize(Expr)</code>", use <a class="pred" href="metacall.html#once/1">once/1</a>, 
e.g.:

<pre class="code">
once(labeling([max(Expr)], Vars))
</pre>

<p>Labeling is always complete, always terminates, and yields no 
redundant solutions.</dd>
<dt class="pubdef"><a id="all_different/1"><strong>all_different</strong>(<var>+Vars</var>)</a></dt>
<dd class="defbody">
<var>Vars</var> are pairwise distinct.</dd>
<dt class="pubdef"><a id="all_distinct/1"><strong>all_distinct</strong>(<var>+Ls</var>)</a></dt>
<dd class="defbody">
Like <a class="pred" href="clpfd.html#all_different/1">all_different/1</a>, 
with stronger propagation. For example,
<a class="pred" href="clpfd.html#all_distinct/1">all_distinct/1</a> can 
detect that not all variables can assume distinct values given the 
following domains:

<pre class="code">
?- maplist(in, Vs,
           [1\/3..4, 1..2\/4, 1..2\/4, 1..3, 1..3, 1..6]),
   all_distinct(Vs).
false.
</pre>

</dd>
<dt class="pubdef"><a id="sum/3"><strong>sum</strong>(<var>+Vars, +Rel, 
?Expr</var>)</a></dt>
<dd class="defbody">
The sum of elements of the list <var>Vars</var> is in relation <var>Rel</var> 
to <var>Expr</var>.
<var>Rel</var> is one of #=, #<code>\</code>=, #<var>&lt;</var>, #<var>&gt;</var>, <code>#=&lt;</code> 
or #<var>&gt;</var>=. For example:

<pre class="code">
?- [A,B,C] ins 0..sup, sum([A,B,C], #=, 100).
A in 0..100,
A+B+C#=100,
B in 0..100,
C in 0..100.
</pre>

</dd>
<dt class="pubdef"><a id="scalar_product/4"><strong>scalar_product</strong>(<var>+Cs, 
+Vs, +Rel, ?Expr</var>)</a></dt>
<dd class="defbody">
<var>Cs</var> is a list of integers, <var>Vs</var> is a list of 
variables and integers. True if the scalar product of <var>Cs</var> and <var>Vs</var> 
is in relation <var>Rel</var> to <var>Expr</var>, where <var>Rel</var> 
is #=, #<code>\</code>=, #<var>&lt;</var>, #<var>&gt;</var>, <code>#=&lt;</code> 
or #<var>&gt;</var>=.</dd>
<dt class="pubdef"><a id="#>=/2"><var>?X</var> <strong>#&gt;=</strong> <var>?Y</var></a></dt>
<dd class="defbody">
<var>X</var> is greater than or equal to <var>Y</var>.</dd>
<dt class="pubdef"><a id="#=</2"><var>?X</var> <strong>#=&lt;</strong> <var>?Y</var></a></dt>
<dd class="defbody">
<var>X</var> is less than or equal to <var>Y</var>.</dd>
<dt class="pubdef"><a id="#=/2"><var>?X</var> <strong>#=</strong> <var>?Y</var></a></dt>
<dd class="defbody">
<var>X</var> equals <var>Y</var>.</dd>
<dt class="pubdef"><a id="#\=/2"><var>?X</var> <strong>#\=</strong> <var>?Y</var></a></dt>
<dd class="defbody">
<var>X</var> is not <var>Y</var>.</dd>
<dt class="pubdef"><a id="#>/2"><var>?X</var> <strong>#&gt;</strong> <var>?Y</var></a></dt>
<dd class="defbody">
<var>X</var> is greater than <var>Y</var>.</dd>
<dt class="pubdef"><a id="#</2"><var>?X</var> <strong>#&lt;</strong> <var>?Y</var></a></dt>
<dd class="defbody">
<var>X</var> is less than <var>Y</var>. In addition to its regular use 
in problems that require it, this constraint can also be useful to 
eliminate uninteresting symmetries from a problem. For example, all 
possible matches between pairs built from four players in total:

<pre class="code">
?- Vs = [A,B,C,D], Vs ins 1..4,
        all_different(Vs),
        A #&lt; B, C #&lt; D, A #&lt; C,
   findall(pair(A,B)-pair(C,D), label(Vs), Ms).
Ms = [ pair(1, 2)-pair(3, 4),
       pair(1, 3)-pair(2, 4),
       pair(1, 4)-pair(2, 3)].
</pre>

</dd>
<dt class="pubdef"><a id="#\/1"><strong>#\</strong> <var>+Q</var></a></dt>
<dd class="defbody">
The reifiable constraint <var>Q</var> does <i>not</i> hold. For example, 
to obtain the complement of a domain:

<pre class="code">
?- #\ X in -3..0\/10..80.
X in inf.. -4\/1..9\/81..sup.
</pre>

</dd>
<dt class="pubdef"><a id="#<==>/2"><var>?P</var> <strong>#&lt;==&gt;</strong> <var>?Q</var></a></dt>
<dd class="defbody">
<var>P</var> and <var>Q</var> are equivalent. For example:

<pre class="code">
?- X #= 4 #&lt;==&gt; B, X #\= 4.
B = 0,
X in inf..3\/5..sup.
</pre>

<p>The following example uses reified constraints to relate a list of 
finite domain variables to the number of occurrences of a given value:

<pre class="code">
:- use_module(library(clpfd)).

vs_n_num(Vs, N, Num) :-
        maplist(eq_b(N), Vs, Bs),
        sum(Bs, #=, Num).

eq_b(X, Y, B) :- X #= Y #&lt;==&gt; B.
</pre>

<p>Sample queries and their results:

<pre class="code">
?- Vs = [X,Y,Z], Vs ins 0..1, vs_n_num(Vs, 4, Num).
Vs = [X, Y, Z],
Num = 0,
X in 0..1,
Y in 0..1,
Z in 0..1.

?- vs_n_num([X,Y,Z], 2, 3).
X = 2,
Y = 2,
Z = 2.
</pre>

</dd>
<dt class="pubdef"><a id="#==>/2"><var>?P</var> <strong>#==&gt;</strong> <var>?Q</var></a></dt>
<dd class="defbody">
<var>P</var> implies <var>Q</var>.</dd>
<dt class="pubdef"><a id="#<==/2"><var>?P</var> <strong>#&lt;==</strong> <var>?Q</var></a></dt>
<dd class="defbody">
<var>Q</var> implies <var>P</var>.</dd>
<dt class="pubdef"><a id="#/\/2"><var>?P</var> <strong>#/\</strong> <var>?Q</var></a></dt>
<dd class="defbody">
<var>P</var> and <var>Q</var> hold.</dd>
<dt class="pubdef"><a id="#\//2"><var>?P</var> <strong>#\/</strong> <var>?Q</var></a></dt>
<dd class="defbody">
<var>P</var> or <var>Q</var> holds. For example, the sum of natural 
numbers below 1000 that are multiples of 3 or 5:

<pre class="code">
?- findall(N, (N mod 3 #= 0 #\/ N mod 5 #= 0, N in 0..999,
               indomain(N)),
           Ns),
   sum(Ns, #=, Sum).
Ns = [0, 3, 5, 6, 9, 10, 12, 15, 18|...],
Sum = 233168.
</pre>

</dd>
<dt class="pubdef"><a id="lex_chain/1"><strong>lex_chain</strong>(<var>+Lists</var>)</a></dt>
<dd class="defbody">
<var>Lists</var> are lexicographically non-decreasing.</dd>
<dt class="pubdef"><a id="tuples_in/2"><strong>tuples_in</strong>(<var>+Tuples, 
+Relation</var>)</a></dt>
<dd class="defbody">
<var>Relation</var> must be a list of lists of integers. The elements of 
the list <var>Tuples</var> are constrained to be elements of <var>Relation</var>. 
Arbitrary finite relations, such as compatibility tables, can be modeled 
in this way. For example, if 1 is compatible with 2 and 5, and 4 is 
compatible with 0 and 3:

<pre class="code">
?- tuples_in([[X,Y]], [[1,2],[1,5],[4,0],[4,3]]), X = 4.
X = 4,
Y in 0\/3.
</pre>

<p>As another example, consider a train schedule represented as a list 
of quadruples, denoting departure and arrival places and times for each 
train. In the following program, Ps is a feasible journey of length 3 
from A to D via trains that are part of the given schedule.

<pre class="code">
:- use_module(library(clpfd)).

trains([[1,2,0,1],
        [2,3,4,5],
        [2,3,0,1],
        [3,4,5,6],
        [3,4,2,3],
        [3,4,8,9]]).

threepath(A, D, Ps) :-
        Ps = [[A,B,_T0,T1],[B,C,T2,T3],[C,D,T4,_T5]],
        T2 #&gt; T1,
        T4 #&gt; T3,
        trains(Ts),
        tuples_in(Ps, Ts).
</pre>

<p>In this example, the unique solution is found without labeling:

<pre class="code">
?- threepath(1, 4, Ps).
Ps = [[1, 2, 0, 1], [2, 3, 4, 5], [3, 4, 8, 9]].
</pre>

</dd>
<dt class="pubdef"><a id="serialized/2"><strong>serialized</strong>(<var>+Starts, 
+Durations</var>)</a></dt>
<dd class="defbody">
Describes a set of non-overlapping tasks.
<var>Starts</var> = [S_1,...,S_n], is a list of variables or integers,
<var>Durations</var> = [D_1,...,D_n] is a list of non-negative integers. 
Constrains <var>Starts</var> and <var>Durations</var> to denote a set of 
non-overlapping tasks, i.e.: S_i + D_i <code>=&lt;</code> S_j or S_j + 
D_j <code>=&lt;</code> S_i for all 1 <code>=&lt;</code> i <var>&lt;</var> 
j <code>=&lt;</code> n. Example:

<pre class="code">
?- length(Vs, 3),
   Vs ins 0..3,
   serialized(Vs, [1,2,3]),
   label(Vs).
Vs = [0, 1, 3] ;
Vs = [2, 0, 3] ;
false.
</pre>

<dl class="tags">
<dt class="tag">See also</dt>
<dd>
Dorndorf et al. 2000, "Constraint Propagation Techniques for the 
Disjunctive Scheduling Problem"
</dd>
</dl>

</dd>
<dt class="pubdef"><a id="element/3"><strong>element</strong>(<var>?N, 
+Vs, ?V</var>)</a></dt>
<dd class="defbody">
The <var>N</var>-th element of the list of finite domain variables <var>Vs</var> 
is <var>V</var>. Analogous to <a class="pred" href="lists.html#nth1/3">nth1/3</a>.</dd>
<dt class="pubdef"><a id="global_cardinality/2"><strong>global_cardinality</strong>(<var>+Vs, 
+Pairs</var>)</a></dt>
<dd class="defbody">
Global Cardinality constraint. Equivalent to
<code>global_cardinality(Vs, Pairs, [])</code>. Example:

<pre class="code">
?- Vs = [_,_,_], global_cardinality(Vs, [1-2,3-_]), label(Vs).
Vs = [1, 1, 3] ;
Vs = [1, 3, 1] ;
Vs = [3, 1, 1].
</pre>

</dd>
<dt class="pubdef"><a id="global_cardinality/3"><strong>global_cardinality</strong>(<var>+Vs, 
+Pairs, +Options</var>)</a></dt>
<dd class="defbody">
Global Cardinality constraint. <var>Vs</var> is a list of finite domain 
variables, <var>Pairs</var> is a list of Key-Num pairs, where Key is an 
integer and Num is a finite domain variable. The constraint holds iff 
each V in <var>Vs</var> is equal to some key, and for each Key-Num pair 
in <var>Pairs</var>, the number of occurrences of Key in <var>Vs</var> 
is Num. <var>Options</var> is a list of options. Supported options are:

<dl class="latex">
<dt><strong>consistency</strong>(<var>value</var>)</dt>
<dd class="defbody">
A weaker form of consistency is used.
</dd>
<dt><strong>cost</strong>(<var>Cost, Matrix</var>)</dt>
<dd class="defbody">
<var>Matrix</var> is a list of rows, one for each variable, in the order 
they occur in <var>Vs</var>. Each of these rows is a list of integers, 
one for each key, in the order these keys occur in <var>Pairs</var>. 
When variable v_i is assigned the value of key k_j, then the associated 
cost is <var>Matrix</var>_{ij}. <var>Cost</var> is the sum of all costs.
</dd>
</dl>

</dd>
<dt class="pubdef"><a id="circuit/1"><strong>circuit</strong>(<var>+Vs</var>)</a></dt>
<dd class="defbody">
True if the list <var>Vs</var> of finite domain variables induces a 
Hamiltonian circuit. The k-th element of <var>Vs</var> denotes the 
successor of node k. Node indexing starts with 1. Examples:

<pre class="code">
?- length(Vs, _), circuit(Vs), label(Vs).
Vs = [] ;
Vs = [1] ;
Vs = [2, 1] ;
Vs = [2, 3, 1] ;
Vs = [3, 1, 2] ;
Vs = [2, 3, 4, 1] .
</pre>

</dd>
<dt class="pubdef"><a id="cumulative/1"><strong>cumulative</strong>(<var>+Tasks</var>)</a></dt>
<dd class="defbody">
Equivalent to <code>cumulative(Tasks, [limit(1)])</code>.</dd>
<dt class="pubdef"><a id="cumulative/2"><strong>cumulative</strong>(<var>+Tasks, 
+Options</var>)</a></dt>
<dd class="defbody">
<var>Tasks</var> is a list of tasks, each of the form <code>task(S_i, D_i, E_i, C_i, T_i)</code>. 
S_i denotes the start time, D_i the positive duration, E_i the end time, 
C_i the non-negative resource consumption, and T_i the task identifier. 
Each of these arguments must be a finite domain variable with bounded 
domain, or an integer. The constraint holds if at any time during the 
start and end of each task, the total resource consumption of all tasks 
running at that time does not exceed the global resource limit (which is 
1 by default).
<var>Options</var> is a list of options. Currently, the only supported 
option is:

<dl class="latex">
<dt><strong>limit</strong>(<var>L</var>)</dt>
<dd class="defbody">
The integer <var>L</var> is the global resource limit.
</dd>
</dl>

<p>For example, given the following predicate that relates three tasks 
of durations 2 and 3 to a list containing their starting times:

<pre class="code">
tasks_starts(Tasks, [S1,S2,S3]) :-
        Tasks = [task(S1,3,_,1,_),
                 task(S2,2,_,1,_),
                 task(S3,2,_,1,_)].
</pre>

<p>We can use <a class="pred" href="clpfd.html#cumulative/2">cumulative/2</a> 
as follows, and obtain a schedule:

<pre class="code">
?- tasks_starts(Tasks, Starts), Starts ins 0..10,
   cumulative(Tasks, [limit(2)]), label(Starts).
Tasks = [task(0, 3, 3, 1, _G36), task(0, 2, 2, 1, _G45), ...],
Starts = [0, 0, 2] .
</pre>

</dd>
<dt class="pubdef"><a id="automaton/3"><strong>automaton</strong>(<var>+Signature, 
+Nodes, +Arcs</var>)</a></dt>
<dd class="defbody">
Describes a list of finite domain variables with a finite automaton. 
Equivalent to <code>automaton(_, _, Signature, Nodes, Arcs, [], [], _)</code>, 
a common use case of <a class="pred" href="clpfd.html#automaton/8">automaton/8</a>. 
In the following example, a list of binary finite domain variables is 
constrained to contain at least two consecutive ones:

<pre class="code">
:- use_module(library(clpfd)).

two_consecutive_ones(Vs) :-
        automaton(Vs, [source(a),sink(c)],
                  [arc(a,0,a), arc(a,1,b),
                   arc(b,0,a), arc(b,1,c),
                   arc(c,0,c), arc(c,1,c)]).
</pre>

<p>Example query:

<pre class="code">
?- length(Vs, 3), two_consecutive_ones(Vs), label(Vs).
Vs = [0, 1, 1] ;
Vs = [1, 1, 0] ;
Vs = [1, 1, 1].
</pre>

</dd>
<dt class="pubdef"><a id="automaton/8"><strong>automaton</strong>(<var>?Sequence, 
?Template, +Signature, +Nodes, +Arcs, +Counters, +Initials, ?Finals</var>)</a></dt>
<dd class="defbody">
Describes a list of finite domain variables with a finite automaton. 
True if the finite automaton induced by <var>Nodes</var> and <var>Arcs</var> 
(extended with <var>Counters</var>) accepts <var>Signature</var>. <var>Sequence</var> 
is a list of terms, all of the same shape. Additional constraints must 
link
<var>Sequence</var> to <var>Signature</var>, if necessary. <var>Nodes</var> 
is a list of
<code>source(Node)</code> and <code>sink(Node)</code> terms. <var>Arcs</var> 
is a list of
<code>arc(Node,Integer,Node)</code> and <code>arc(Node,Integer,Node,Exprs)</code> 
terms that denote the automaton's transitions. Each node is represented 
by an arbitrary term. Transitions that are not mentioned go to an 
implicit failure node. Exprs is a list of arithmetic expressions, of the 
same length as <var>Counters</var>. In each expression, variables 
occurring in <var>Counters</var> correspond to old counter values, and 
variables occurring in <var>Template</var> correspond to the current 
element of <var>Sequence</var>. When a transition containing expressions 
is taken, counters are updated as stated. By default, counters remain 
unchanged. <var>Counters</var> is a list of variables that must not 
occur anywhere outside of the constraint goal. <var>Initials</var> is a 
list of the same length as <var>Counters</var>. Counter arithmetic on 
the transitions relates the counter values in <var>Initials</var> to <var>Finals</var>.

<p>The following example is taken from Beldiceanu, Carlsson, Debruyne 
and Petit: "Reformulation of Global Constraints Based on Constraints 
Checkers", Constraints 10(4), pp 339-362 (2005). It relates a sequence 
of integers and finite domain variables to its number of inflexions, 
which are switches between strictly ascending and strictly descending 
subsequences:

<pre class="code">
:- use_module(library(clpfd)).

sequence_inflexions(Vs, N) :-
        variables_signature(Vs, Sigs),
        automaton(_, _, Sigs,
                  [source(s),sink(i),sink(j),sink(s)],
                  [arc(s,0,s), arc(s,1,j), arc(s,2,i),
                   arc(i,0,i), arc(i,1,j,[C+1]), arc(i,2,i),
                   arc(j,0,j), arc(j,1,j),
                   arc(j,2,i,[C+1])],
                  [C], [0], [N]).

variables_signature([], []).
variables_signature([V|Vs], Sigs) :-
        variables_signature_(Vs, V, Sigs).

variables_signature_([], _, []).
variables_signature_([V|Vs], Prev, [S|Sigs]) :-
        V #= Prev #&lt;==&gt; S #= 0,
        Prev #&lt; V #&lt;==&gt; S #= 1,
        Prev #&gt; V #&lt;==&gt; S #= 2,
        variables_signature_(Vs, V, Sigs).
</pre>

<p>Example queries:

<pre class="code">
?- sequence_inflexions([1,2,3,3,2,1,3,0], N).
N = 3.

?- length(Ls, 5), Ls ins 0..1,
   sequence_inflexions(Ls, 3), label(Ls).
Ls = [0, 1, 0, 1, 0] ;
Ls = [1, 0, 1, 0, 1].
</pre>

</dd>
<dt class="pubdef"><a id="transpose/2"><strong>transpose</strong>(<var>+Matrix, 
?Transpose</var>)</a></dt>
<dd class="defbody">
<var>Transpose</var> a list of lists of the same length. Example:

<pre class="code">
?- transpose([[1,2,3],[4,5,6],[7,8,9]], Ts).
Ts = [[1, 4, 7], [2, 5, 8], [3, 6, 9]].
</pre>

<p>This predicate is useful in many constraint programs. Consider for 
instance Sudoku:

<pre class="code">
:- use_module(library(clpfd)).

sudoku(Rows) :-
        length(Rows, 9), maplist(length_(9), Rows),
        append(Rows, Vs), Vs ins 1..9,
        maplist(all_distinct, Rows),
        transpose(Rows, Columns),
        maplist(all_distinct, Columns),
        Rows = [A,B,C,D,E,F,G,H,I],
        blocks(A, B, C), blocks(D, E, F), blocks(G, H, I).

length_(L, Ls) :- length(Ls, L).

blocks([], [], []).
blocks([A,B,C|Bs1], [D,E,F|Bs2], [G,H,I|Bs3]) :-
        all_distinct([A,B,C,D,E,F,G,H,I]),
        blocks(Bs1, Bs2, Bs3).

problem(1, [[_,_,_,_,_,_,_,_,_],
            [_,_,_,_,_,3,_,8,5],
            [_,_,1,_,2,_,_,_,_],
            [_,_,_,5,_,7,_,_,_],
            [_,_,4,_,_,_,1,_,_],
            [_,9,_,_,_,_,_,_,_],
            [5,_,_,_,_,_,_,7,3],
            [_,_,2,_,1,_,_,_,_],
            [_,_,_,_,4,_,_,_,9]]).
</pre>

<p>Sample query:

<pre class="code">
?- problem(1, Rows), sudoku(Rows), maplist(writeln, Rows).
[9, 8, 7, 6, 5, 4, 3, 2, 1]
[2, 4, 6, 1, 7, 3, 9, 8, 5]
[3, 5, 1, 9, 2, 8, 7, 4, 6]
[1, 2, 8, 5, 3, 7, 6, 9, 4]
[6, 3, 4, 8, 9, 2, 1, 5, 7]
[7, 9, 5, 4, 6, 1, 8, 3, 2]
[5, 1, 9, 2, 8, 6, 4, 7, 3]
[4, 7, 2, 3, 1, 9, 5, 6, 8]
[8, 6, 3, 7, 4, 5, 2, 1, 9]
Rows = [[9, 8, 7, 6, 5, 4, 3, 2|...], ... , [...|...]].
</pre>

</dd>
<dt class="pubdef"><a id="zcompare/3"><strong>zcompare</strong>(<var>?Order, 
?A, ?B</var>)</a></dt>
<dd class="defbody">
Analogous to <a class="pred" href="compare.html#compare/3">compare/3</a>, 
with finite domain variables <var>A</var> and <var>B</var>. Example:

<pre class="code">
:- use_module(library(clpfd)).

 n_factorial(N, F) :-
         zcompare(C, N, 0),
         n_factorial_(C, N, F).

 n_factorial_(=, _, 1).
 n_factorial_(&gt;, N, F) :-
      F #= F0*N, N1 #= N - 1,
      n_factorial(N1, F0).
</pre>

<p>This version is deterministic if the first argument is instantiated:

<pre class="code">
?- n_factorial(30, F).
F = 265252859812191058636308480000000.
</pre>

</dd>
<dt class="pubdef"><a id="chain/2"><strong>chain</strong>(<var>+Zs, 
+Relation</var>)</a></dt>
<dd class="defbody">
<var>Zs</var> form a chain with respect to <var>Relation</var>. <var>Zs</var> 
is a list of finite domain variables that are a chain with respect to 
the partial order
<var>Relation</var>, in the order they appear in the list. <var>Relation</var> 
must be #=,
#=<var>&lt;</var>, #<var>&gt;</var>=, <code>#&lt;</code> or #<var>&gt;</var>. 
For example:

<pre class="code">
?- chain([X,Y,Z], #&gt;=).
X#&gt;=Y,
Y#&gt;=Z.
</pre>

</dd>
<dt class="pubdef"><a id="fd_var/1"><strong>fd_var</strong>(<var>+Var</var>)</a></dt>
<dd class="defbody">
True iff <var>Var</var> is a CLP(FD) variable.</dd>
<dt class="pubdef"><a id="fd_inf/2"><strong>fd_inf</strong>(<var>+Var, 
-Inf</var>)</a></dt>
<dd class="defbody">
<var>Inf</var> is the infimum of the current domain of <var>Var</var>.</dd>
<dt class="pubdef"><a id="fd_sup/2"><strong>fd_sup</strong>(<var>+Var, 
-Sup</var>)</a></dt>
<dd class="defbody">
<var>Sup</var> is the supremum of the current domain of <var>Var</var>.</dd>
<dt class="pubdef"><a id="fd_size/2"><strong>fd_size</strong>(<var>+Var, 
-Size</var>)</a></dt>
<dd class="defbody">
Determine the size of a variable's domain. <var>Size</var> is the number 
of elements of the current domain of <var>Var</var>, or the atom <b>sup</b> 
if the domain is unbounded.</dd>
<dt class="pubdef"><a id="fd_dom/2"><strong>fd_dom</strong>(<var>+Var, 
-Dom</var>)</a></dt>
<dd class="defbody">
<var>Dom</var> is the current domain (see <a class="pred" href="clpfd.html#in/2">in/2</a>) 
of <var>Var</var>. This predicate is useful if you want to reason about 
domains. It is not needed if you only want to display remaining domains; 
instead, separate your model from the search part and let the toplevel 
display this information via residual goals.
</dd>
</dl>

<p></body></html>
swi-prolog-nox 6.6.4-2ubuntu1 / usr / lib / swi-prolog / doc / Manual / clpfd.html
