/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 5.11.18 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
{ background-color: #c5e1ff;
}

dt.multidef
{ background-color: #c8ffc7;
}

.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: #202020;
}

/* Footnotes */

sup.fn { color: blue; text-decoration: underline; }
span.fn-text { display: none; }
sup.fn span {display: none;}
sup:hover span
{ display: block !important;
position: absolute; top: auto; left: auto; width: 80%;
color: #000; background: white;
border: 2px solid;
padding: 5px; margin: 10px; z-index: 100;
font-size: smaller;
}
</STYLE>
</HEAD>
<BODY BGCOLOR="white">
<DIV class="navigate"><A class="nav" href="index.html"><IMG SRC="home.gif" BORDER=0 ALT="Home"></A>
<A class="nav" href="Contents.html"><IMG SRC="index.gif" BORDER=0 ALT="Contents"></A>
<A class="nav" href="DocIndex.html"><IMG SRC="yellow_pages.gif" BORDER=0 ALT="Index"></A>
<A class="nav" href="summary.html"><IMG SRC="info.gif" BORDER=0 ALT="Summary"></A>
<A class="nav" href="check.html"><IMG SRC="prev.gif" BORDER=0 ALT="Previous"></A>
<A class="nav" href="clpqr.html"><IMG SRC="next.gif" BORDER=0 ALT="Next"></A>
</DIV>

<H2><A NAME="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 NAME="sec:clpfd"></A>

<DL>
<DT><B>author</B><DD> Markus Triska
</DL>

<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. A finite domain <I>expression</I> is one of:
<BLOCKQUOTE>
<TABLE BORDER=2 FRAME=box RULES=groups>
<TR VALIGN=top><TD>an integer</TD><TD>Given value </TD></TR>
<TR VALIGN=top><TD>a variable</TD><TD>Unknown value </TD></TR>
<TR VALIGN=top><TD>-Expr</TD><TD>Unary minus </TD></TR>
<TR VALIGN=top><TD>Expr + Expr</TD><TD>Addition </TD></TR>
<TR VALIGN=top><TD>Expr * Expr</TD><TD>Multiplication </TD></TR>
<TR VALIGN=top><TD>Expr - Expr</TD><TD>Subtraction </TD></TR>
<TR VALIGN=top><TD>Expr <CODE>^</CODE> Expr</TD><TD>Exponentiation </TD></TR>
<TR VALIGN=top><TD>min(Expr,Expr)</TD><TD>Minimum of two expressions </TD></TR>
<TR VALIGN=top><TD>max(Expr,Expr)</TD><TD>Maximum of two expressions </TD></TR>
<TR VALIGN=top><TD>Expr mod Expr</TD><TD>Modulo </TD></TR>
<TR VALIGN=top><TD>abs(Expr)</TD><TD>Absolute value </TD></TR>
<TR VALIGN=top><TD>Expr / Expr</TD><TD>Integer division </TD></TR>
</TABLE>

</BLOCKQUOTE>

<P>The most important finite domain constraints are:
<BLOCKQUOTE>
<TABLE BORDER=2 FRAME=box RULES=groups>
<TR VALIGN=top><TD>Expr1 <CODE>#&gt;=</CODE> Expr2</TD><TD>Expr1 is 
larger than or equal to Expr2 </TD></TR>
<TR VALIGN=top><TD>Expr1 <CODE>#=&lt;</CODE> Expr2</TD><TD>Expr1 is 
smaller than or equal to Expr2 </TD></TR>
<TR VALIGN=top><TD>Expr1 <CODE>#=</CODE> Expr2</TD><TD>Expr1 equals 
Expr2 </TD></TR>
<TR VALIGN=top><TD>Expr1 <CODE>#\=</CODE> Expr2</TD><TD>Expr1 is not 
equal to Expr2 </TD></TR>
<TR VALIGN=top><TD>Expr1 <CODE>#&gt;</CODE> Expr2</TD><TD>Expr1 is 
strictly larger than Expr2 </TD></TR>
<TR VALIGN=top><TD>Expr1 <CODE>#&lt;</CODE> Expr2</TD><TD>Expr1 is 
strictly smaller than Expr2 </TD></TR>
</TABLE>

</BLOCKQUOTE>

<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 BORDER=2 FRAME=box RULES=groups>
<TR VALIGN=top><TD><CODE>#\</CODE> Q</TD><TD>True iff Q is false </TD></TR>
<TR VALIGN=top><TD>P <CODE>#\/</CODE> Q</TD><TD>True iff either P or Q </TD></TR>
<TR VALIGN=top><TD>P <CODE>#/\</CODE> Q</TD><TD>True iff both P and Q </TD></TR>
<TR VALIGN=top><TD>P <CODE>#&lt;==&gt;</CODE> Q</TD><TD>True iff P and Q 
are equivalent </TD></TR>
<TR VALIGN=top><TD>P <CODE>#==&gt;</CODE> Q</TD><TD>True iff P implies Q </TD></TR>
<TR VALIGN=top><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. If a variable 
occurs at the place of a constraint that is being reified, it is 
implicitly constrained to the Boolean values 0 and 1. Therefore, the 
following queries all fail: <CODE>?-</CODE> <CODE>#\</CODE> 2., <CODE>?-</CODE> <CODE>#\</CODE> <CODE>#\</CODE> 
2. etc.

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

<PRE class="code">
?- [library(clpfd)].
% library(clpfd) compiled into clpfd 0.06 sec, 3,308 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>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:

<PRE class="code">
?- puzzle(As+Bs=Cs).
As = [9, _G10107, _G10110, _G10113],
Bs = [1, 0, _G10128, _G10107],
Cs = [1, 0, _G10110, _G10107, _G10152],
_G10107 in 4..7,
1000*9+91*_G10107+ -90*_G10110+_G10113+ -9000*1+ -900*0+10*_G10128+ -1*_G10152#=0,
all_different([_G10107, _G10110, _G10113, _G10128, _G10152, 0, 1, 9]),
_G10110 in 5..8,
_G10113 in 2..8,
_G10128 in 2..8,
_G10152 in 2..8.
</PRE>

<P>Here, the constraint solver has deduced more stringent bounds for all 
variables. Keeping the modeling part separate from the search lets you 
view these residual goals, observe termination and determinism 
properties of the modeling part in isolation from the search, and more 
easily experiment with different search strategies. Labeling can then be 
used to search for solutions:

<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>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 n_factorial(N, 0) is the only non-terminating case 
of this kind.

<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 
clpfd_goal_expansion to false.

<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 "oneground(X,Y,Z)", 
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 NAME="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>Integer</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>Lower</I> <CODE>=&lt;</CODE> <I>I</I> <CODE>=&lt;</CODE> <I>Upper</I>.
<I>Lower</I> must be an integer or the atom <B>inf</B>, which denotes 
negative infinity. <I>Upper</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 Domain1 and Domain2.
</DD>
</DL>

</DD>
<DT class="pubdef"><A NAME="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 NAME="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 NAME="label/1"><STRONG>label</STRONG>(<VAR>+Vars</VAR>)</A></DT>
<DD class="defbody">
Equivalent to labeling([], <VAR>Vars</VAR>).</DD>
<DT class="pubdef"><A NAME="labeling/2"><STRONG>labeling</STRONG>(<VAR>+Options, 
+Vars</VAR>)</A></DT>
<DD class="defbody">
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:

<DL class="latex">
<DT><STRONG>min</STRONG>(<VAR>Expr</VAR>)
<DT><STRONG>max</STRONG>(<VAR>Expr</VAR>)</DT>
<DD class="defbody">
</DD>
</DL>

<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 
"maximize(Expr)" and "minimize(Expr)", 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.<DT class="pubdef"><A NAME="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 NAME="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>, where <VAR>Rel</VAR> is #=, #<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 NAME="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 NAME="#>=/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 NAME="#=</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 NAME="#=/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 NAME="#\=/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 NAME="#>/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 NAME="#</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 NAME="#\/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 NAME="#<==>/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 NAME="#==>/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 NAME="#<==/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 NAME="#/\/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 NAME="#\//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 NAME="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 NAME="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 NAME="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 NAME="serialized/2"><STRONG>serialized</STRONG>(<VAR>+Starts, 
+Durations</VAR>)</A></DT>
<DD class="defbody">
Constrain a set of intervals to a non-overlapping sequence.
<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>
<DT><B>See also</B><DD> Dorndorf et al. 2000, "Constraint Propagation 
Techniques for the Disjunctive Scheduling Problem"
</DL>

</DD>
<DT class="pubdef"><A NAME="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 NAME="global_cardinality/2"><STRONG>global_cardinality</STRONG>(<VAR>+Vs, 
+Pairs</VAR>)</A></DT>
<DD class="defbody">
Equivalent to global_cardinality(<VAR>Vs</VAR>, <VAR>Pairs</VAR>, []). 
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 NAME="global_cardinality/3"><STRONG>global_cardinality</STRONG>(<VAR>+Vs, 
+Pairs, +Options</VAR>)</A></DT>
<DD class="defbody">
<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">
Matrix 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 
Matrix_{ij}. Cost is the sum of all costs.
</DD>
</DL>

</DD>
<DT class="pubdef"><A NAME="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, where 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 NAME="automaton/3"><STRONG>automaton</STRONG>(<VAR>+Signature, 
+Nodes, +Arcs</VAR>)</A></DT>
<DD class="defbody">
Equivalent to automaton(_, _, <VAR>Signature</VAR>, <VAR>Nodes</VAR>, <VAR>Arcs</VAR>, 
[], [], _), 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)]).

?- 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 NAME="automaton/8"><STRONG>automaton</STRONG>(<VAR>?Sequence, 
?Template, +Signature, +Nodes, +Arcs, +Counters, +Initials, ?Finals</VAR>)</A></DT>
<DD class="defbody">
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 
source(Node) and sink(Node) terms. <VAR>Arcs</VAR> is a list of 
arc(Node,Integer,Node) and arc(Node,Integer,Node,Exprs) 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 NAME="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 NAME="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 NAME="chain/2"><STRONG>chain</STRONG>(<VAR>+Zs, 
+Relation</VAR>)</A></DT>
<DD class="defbody">
<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 NAME="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 NAME="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 NAME="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 NAME="fd_size/2"><STRONG>fd_size</STRONG>(<VAR>+Var, 
-Size</VAR>)</A></DT>
<DD class="defbody">
<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 NAME="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 5.10.4-3ubuntu1 / usr / lib / swi-prolog / doc / Manual / clpfd.html
