% This LaTeX document was generated using the LaTeX backend of PlDoc,
% The SWI-Prolog documentation system



\subsection{Introduction}

\label{sec:clpfd-intro}

This library provides CLP(FD): Constraint Logic Programming over
Finite Domains. This is an instance of the general CLP(\textit{X})
scheme (\secref{clp}), extending logic programming with reasoning over
specialised domains. CLP(FD) lets us reason about \textbf{integers} in a
way that honors the relational nature of Prolog.

Read \href{https://www.metalevel.at/prolog}{\textbf{The Power of Prolog}} to
understand how this library is meant to be used in practice.

There are two major use cases of CLP(FD) constraints:

\begin{enumerate}
    \item \textbf{declarative integer arithmetic} (\secref{clpfd-integer-arith})
    \item solving \textbf{combinatorial problems} such as planning, scheduling
and allocation tasks.
\end{enumerate}

The predicates of this library can be classified as:

\begin{itemize}
    \item \textit{arithmetic} constraints like \predref{\Sceq}{2}, \predref{\Scgt}{2} and \predref{\Scne}{2}  (\secref{clpfd-arithmetic})
    \item the \textit{membership} constraints \predref{in}{2} and \predref{ins}{2}  (\secref{clpfd-membership})
    \item the \textit{enumeration} predicates \predref{indomain}{1}, \predref{label}{1} and \predref{labeling}{2}  (\secref{clpfd-enumeration})
    \item \textit{combinatorial} constraints like \predref{all_distinct}{1} and \predref{global_cardinality}{2}  (\secref{clpfd-global})
    \item \textit{reification} predicates such as \predref{\Scequal}{2}  (\secref{clpfd-reification-predicates})
    \item \textit{reflection} predicates such as \predref{fd_dom}{2}  (\secref{clpfd-reflection-predicates})
\end{itemize}

In most cases, \textit{arithmetic constraints} (\secref{clpfd-arith-constraints})
are the only predicates you will ever need from this library. When
reasoning over integers, simply replace low-level arithmetic
predicates like \verb$(is)/2$ and \verb$(>)/2$ by the corresponding CLP(FD)
constraints like \predref{\Sceq}{2} and \predref{\Scgt}{2} to honor and preserve declarative
properties of your programs. For satisfactory performance, arithmetic
constraints are implicitly rewritten at compilation time so that
low-level fallback predicates are automatically used whenever
possible.

Almost all Prolog programs also reason about integers. Therefore, it
is highly advisable that you make CLP(FD) constraints available in all
your programs. One way to do this is to put the following directive in
your \verb$<config>/init.pl$ initialisation file:

\begin{code}
:- use_module(library(clpfd)).
\end{code}

All example programs that appear in the CLP(FD) documentation assume
that you have done this.

Important concepts and principles of this library are illustrated by
means of usage examples that are available in a public git repository:
\href{https://github.com/triska/clpfd}{\textbf{github.com/triska/clpfd}}

If you are used to the complicated operational considerations that
low-level arithmetic primitives necessitate, then moving to CLP(FD)
constraints may, due to their power and convenience, at first feel to
you excessive and almost like cheating. It \textit{isn't}. Constraints are an
integral part of all popular Prolog systems, and they are designed
to help you eliminate and avoid the use of low-level and less general
primitives by providing declarative alternatives that are meant to be
used instead.

When teaching Prolog, CLP(FD) constraints should be introduced
\textit{before} explaining low-level arithmetic predicates and their
procedural idiosyncrasies. This is because constraints are easy to
explain, understand and use due to their purely relational nature. In
contrast, the modedness and directionality of low-level arithmetic
primitives are impure limitations that are better deferred to more
advanced lectures.

We recommend the following reference (PDF:
\href{https://www.metalevel.at/swiclpfd.pdf}{metalevel.at/swiclpfd.pdf}) for
citing this library in scientific publications:

\begin{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}
}
\end{code}

More information about CLP(FD) constraints and their implementation is
contained in: \href{https://www.metalevel.at/drt.pdf}{\textbf{metalevel.at/drt.pdf}}

The best way to discuss applying, improving and extending CLP(FD)
constraints is to use the dedicated \const{clpfd} tag on
\href{http://stackoverflow.com}{stackoverflow.com}. Several of the world's
foremost CLP(FD) experts regularly participate in these discussions
and will help you for free on this platform.

\subsection{Arithmetic constraints}

\label{sec:clpfd-arith-constraints}

In modern Prolog systems, \textbf{arithmetic constraints} subsume and
supersede low-level predicates over integers. The main advantage of
arithmetic constraints is that they are true \textit{relations} and can be
used in all directions. For most programs, arithmetic constraints are
the only predicates you will ever need from this library.

The most important arithmetic constraint is \predref{\Sceq}{2}, which subsumes both
\verb$(is)/2$ and \verb$(=:=)/2$ over integers. Use \predref{\Sceq}{2} to make your programs
more general. See declarative integer
arithmetic (\secref{clpfd-integer-arith}).

In total, the arithmetic constraints are:

\begin{quote}
\begin{tabulary}{0.9\textwidth}{|l|L|}
\hline
Expr1 \verb$#=$ Expr2 & Expr1 equals Expr2 \\
Expr1 \verb$#\=$ Expr2 & Expr1 is not equal to Expr2 \\
Expr1 \verb$#>=$ Expr2 & Expr1 is greater than or equal to Expr2 \\
Expr1 \verb$#=<$ Expr2 & Expr1 is less than or equal to Expr2 \\
Expr1 \verb$#>$ Expr2 & Expr1 is greater than Expr2 \\
Expr1 \verb$#<$ Expr2 & Expr1 is less than Expr2 \\
\hline
\end{tabulary}
\end{quote}

\arg{Expr1} and \arg{Expr2} denote \textbf{arithmetic expressions}, which are:

\begin{quote}
\begin{tabulary}{0.9\textwidth}{|l|L|}
\hline
\textit{integer} & Given value \\
\textit{variable} & Unknown integer \\
?(\textit{variable}) & Unknown integer \\
-Expr & Unary minus \\
Expr + Expr & Addition \\
Expr * Expr & Multiplication \\
Expr - Expr & Subtraction \\
Expr \Shat{} Expr & Exponentiation \\
\verb$min(Expr,Expr)$ & Minimum of two expressions \\
\verb$max(Expr,Expr)$ & Maximum of two expressions \\
Expr \const{mod} Expr & Modulo induced by floored division \\
Expr \const{rem} Expr & Modulo induced by truncated division \\
\verb$abs(Expr)$ & Absolute value \\
Expr \Sidiv{} Expr & Truncated integer division \\
Expr div Expr & Floored integer division \\
\hline
\end{tabulary}
\end{quote}

where \arg{Expr} again denotes an arithmetic expression.

The bitwise operations \verb$(\)/1$, \verb$(/\)/2$, \verb$(\/)/2$, \verb$(>>)/2$,
\verb$(<<)/2$, \predref{lsb}{1}, \predref{msb}{1}, \predref{popcount}{1} and \verb$(xor)/2$ are also
supported.

\subsection{Declarative integer arithmetic}

\label{sec:clpfd-integer-arith}

The \textit{arithmetic constraints} (\secref{clpfd-arith-constraints}) \predref{\Sceq}{2}, \predref{\Scgt}{2}
etc. are meant to be used \textit{instead} of the primitives \verb$(is)/2$,
\verb$(=:=)/2$, \verb$(>)/2$ etc. over integers. Almost all Prolog programs also
reason about integers. Therefore, it is recommended that you put the
following directive in your \verb$<config>/init.pl$ initialisation file to make
CLP(FD) constraints available in all your programs:

\begin{code}
:- use_module(library(clpfd)).
\end{code}

Throughout the following, it is assumed that you have done this.

The most basic use of CLP(FD) constraints is \textit{evaluation} of
arithmetic expressions involving integers. For example:

\begin{code}
?- X #= 1+2.
X = 3.
\end{code}

This could in principle also be achieved with the lower-level
predicate \verb$(is)/2$. However, an important advantage of arithmetic
constraints is their purely relational nature: Constraints can be used
in \textit{all directions}, also if one or more of their arguments are only
partially instantiated. For example:

\begin{code}
?- 3 #= Y+2.
Y = 1.
\end{code}

This relational nature makes CLP(FD) constraints easy to explain and
use, and well suited for beginners and experienced Prolog programmers
alike. In contrast, when using low-level integer arithmetic, we get:

\begin{code}
?- 3 is Y+2.
ERROR: is/2: Arguments are not sufficiently instantiated

?- 3 =:= Y+2.
ERROR: =:=/2: Arguments are not sufficiently instantiated
\end{code}

Due to the necessary operational considerations, the use of these
low-level arithmetic predicates is considerably harder to understand
and should therefore be deferred to more advanced lectures.

For supported expressions, CLP(FD) constraints are drop-in
replacements of these low-level arithmetic predicates, often yielding
more general programs. See \predref{n_factorial}{2} (\secref{clpfd-factorial}) for an
example.

This library uses \predref{goal_expansion}{2} to automatically rewrite
constraints at compilation time so that low-level arithmetic
predicates are \textit{automatically} used whenever possible. For example,
the predicate:

\begin{code}
positive_integer(N) :- N #>= 1.
\end{code}

is executed as if it were written as:

\begin{code}
positive_integer(N) :-
        (   integer(N)
        ->  N >= 1
        ;   N #>= 1
        ).
\end{code}

This illustrates why the performance of CLP(FD) constraints is almost
always completely satisfactory when they are used in modes that can be
handled by low-level arithmetic. To disable the automatic rewriting,
set the Prolog flag \verb$clpfd_goal_expansion$ to \const{false}.

If you are used to the complicated operational considerations that
low-level arithmetic primitives necessitate, then moving to CLP(FD)
constraints may, due to their power and convenience, at first feel to
you excessive and almost like cheating. It \textit{isn't}. Constraints are an
integral part of all popular Prolog systems, and they are designed
to help you eliminate and avoid the use of low-level and less general
primitives by providing declarative alternatives that are meant to be
used instead.

\subsection{Example: Factorial relation}

\label{sec:clpfd-factorial}

We illustrate the benefit of using \predref{\Sceq}{2} for more generality with a
simple example.

Consider first a rather conventional definition of \predref{n_factorial}{2},
relating each natural number \textit{N} to its factorial \textit{F}:

\begin{code}
n_factorial(0, 1).
n_factorial(N, F) :-
        N #> 0,
        N1 #= N - 1,
        n_factorial(N1, F1),
        F #= N * F1.
\end{code}

This program uses CLP(FD) constraints \textit{instead} of low-level
arithmetic throughout, and everything that \textit{would have worked} with
low-level arithmetic \textit{also} works with CLP(FD) constraints, retaining
roughly the same performance. For example:

\begin{code}
?- n_factorial(47, F).
F = 258623241511168180642964355153611979969197632389120000000000 ;
false.
\end{code}

Now the point: Due to the increased flexibility and generality of
CLP(FD) constraints, we are free to \textit{reorder} the goals as follows:

\begin{code}
n_factorial(0, 1).
n_factorial(N, F) :-
        N #> 0,
        N1 #= N - 1,
        F #= N * F1,
        n_factorial(N1, F1).
\end{code}

In this concrete case, \textit{termination} properties of the predicate are
improved. For example, the following queries now both terminate:

\begin{code}
?- n_factorial(N, 1).
N = 0 ;
N = 1 ;
false.

?- n_factorial(N, 3).
false.
\end{code}

To make the predicate terminate if \textit{any} argument is instantiated, add
the (implied) constraint \verb$F #\= 0$ before the recursive call.
Otherwise, the query \verb$n_factorial(N, 0)$ is the only non-terminating
case of this kind.

The value of CLP(FD) constraints does \textit{not} lie in completely freeing
us from \textit{all} procedural phenomena. For example, the two programs do
not even have the same \textit{termination properties} in all cases.
Instead, the primary benefit of CLP(FD) constraints is that they allow
you to try different execution orders and apply \href{https://www.metalevel.at/prolog/debugging}{\textbf{declarative
debugging}}
techniques \textit{at all}! Reordering goals (and clauses) can significantly
impact the performance of Prolog programs, and you are free to try
different variants if you use declarative approaches. Moreover, since
all CLP(FD) constraints \textit{always terminate}, placing them earlier can
at most \textit{improve}, never worsen, the termination properties of your
programs. An additional benefit of CLP(FD) constraints is that they
eliminate the complexity of introducing \verb$(is)/2$ and \verb$(=:=)/2$ to
beginners, since \textit{both} predicates are subsumed by \predref{\Sceq}{2} when reasoning
over integers.

In the case above, the clauses are mutually exclusive \textit{if} the first
argument is sufficiently instantiated. To make the predicate
deterministic in such cases while retaining its generality, you can
use \predref{zcompare}{3} to \textit{reify} a comparison, making the different cases
distinguishable by pattern matching. For example, in this concrete
case and others like it, you can use \verb$zcompare(Comp, 0, N)$ to obtain
as \arg{Comp} the symbolic outcome (\verb$<$, \verb$=$, \verb$>$) of 0 compared to N.

\subsection{Combinatorial constraints}

\label{sec:clpfd-combinatorial}

In addition to subsuming and replacing low-level arithmetic
predicates, CLP(FD) constraints are often used to solve combinatorial
problems such as planning, scheduling and allocation tasks. Among the
most frequently used \textbf{combinatorial constraints} are \predref{all_distinct}{1},
\predref{global_cardinality}{2} and \predref{cumulative}{2}. This library also provides
several other constraints like \predref{disjoint2}{1} and \predref{automaton}{8}, which are
useful in more specialized applications.

\subsection{Domains}

\label{sec:clpfd-domains}

Each CLP(FD) variable has an associated set of admissible integers,
which we call the variable's \textbf{domain}. Initially, the domain of each
CLP(FD) variable is the set of \textit{all} integers. CLP(FD) constraints
like \predref{\Sceq}{2}, \predref{\Scgt}{2} and \predref{\Scne}{2} can at most reduce, and never extend, the
domains of their arguments. The constraints \predref{in}{2} and \predref{ins}{2} let us
explicitly state domains of CLP(FD) variables. The process of
determining and adjusting domains of variables is called constraint
\textbf{propagation}, and it is performed automatically by this library. When
the domain of a variable contains only one element, then the variable
is automatically unified to that element.

Domains are taken into account when further constraints are stated,
and by enumeration predicates like \predref{labeling}{2}.

\subsection{Example: Sudoku}

\label{sec:clpfd-sudoku}

As another example, consider \textit{Sudoku}: It is a popular puzzle
over integers that can be easily solved with CLP(FD) constraints.

\begin{code}
sudoku(Rows) :-
        length(Rows, 9), maplist(same_length(Rows), Rows),
        append(Rows, Vs), Vs ins 1..9,
        maplist(all_distinct, Rows),
        transpose(Rows, Columns),
        maplist(all_distinct, Columns),
        Rows = [As,Bs,Cs,Ds,Es,Fs,Gs,Hs,Is],
        blocks(As, Bs, Cs),
        blocks(Ds, Es, Fs),
        blocks(Gs, Hs, Is).

blocks([], [], []).
blocks([N1,N2,N3|Ns1], [N4,N5,N6|Ns2], [N7,N8,N9|Ns3]) :-
        all_distinct([N1,N2,N3,N4,N5,N6,N7,N8,N9]),
        blocks(Ns1, Ns2, Ns3).

problem(1, [[_,_,_,_,_,_,_,_,_],
            [_,_,_,_,_,3,_,8,5],
            [_,_,1,_,2,_,_,_,_],
            [_,_,_,5,_,7,_,_,_],
            [_,_,4,_,_,_,1,_,_],
            [_,9,_,_,_,_,_,_,_],
            [5,_,_,_,_,_,_,7,3],
            [_,_,2,_,1,_,_,_,_],
            [_,_,_,_,4,_,_,_,9]]).
\end{code}

Sample query:

\begin{code}
?- problem(1, Rows), sudoku(Rows), maplist(portray_clause, 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|...], ... , [...|...]].
\end{code}

In this concrete case, the constraint solver is strong enough to find
the unique solution without any search. For the general case, see
search (\secref{clpfd-search}).

\subsection{Residual goals}

\label{sec:clpfd-residual-goals}

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

\begin{code}
?- X #> 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.

?- X #= Y #<==> B, X in 0..3, Y in 4..5.
B = 0,
X in 0..3,
Y in 4..5.
\end{code}

The answers emitted by the toplevel are called \textit{residual programs},
and the goals that comprise each answer are called \textbf{residual goals}.
In each case above, and as for all pure programs, the residual program
is declaratively equivalent to the original query. From the residual
goals, it is clear that the constraint solver has deduced additional
domain restrictions in many cases.

To inspect residual goals, it is best to let the toplevel display them
for us. Wrap the call of your predicate into \predref{call_residue_vars}{2} to
make sure that all constrained variables are displayed. To make the
constraints a variable is involved in available as a Prolog term for
further reasoning within your program, use \predref{copy_term}{3}. For example:

\begin{code}
?- X #= Y + Z, X in 0..5, copy_term([X,Y,Z], [X,Y,Z], Gs).
Gs = [clpfd: (X in 0..5), clpfd: (Y+Z#=X)],
X in 0..5,
Y+Z#=X.
\end{code}

This library also provides \textit{reflection} predicates (like \predref{fd_dom}{2},
\predref{fd_size}{2} etc.) with which we can inspect a variable's current
domain. These predicates can be useful if you want to implement your
own labeling strategies.

\subsection{Core relations and search}

\label{sec:clpfd-search}

Using CLP(FD) constraints to solve combinatorial tasks typically
consists of two phases:

\begin{enumerate}
    \item \textbf{Modeling}. In this phase, all relevant constraints are stated.
    \item \textbf{Search}. In this phase, \textit{enumeration predicates} are used
to search for concrete solutions.
\end{enumerate}

It is good practice to keep the modeling part, via a dedicated
predicate called the \textbf{core relation}, separate from the actual
search for solutions. This lets us observe termination and
determinism properties of the core relation in isolation from the
search, and more easily try different search strategies.

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:

\begin{code}
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.
\end{code}

Notice that we are \textit{not} using \predref{labeling}{2} in this predicate, so that
we can first execute and observe the modeling part in isolation.
Sample query and its result (actual variables replaced for
readability):

\begin{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]),
91*A2+A4+10*B3#=90*A3+C5,
A3 in 5..8,
A4 in 2..8,
B3 in 2..8,
C5 in 2..8.
\end{code}

From this answer, we see that this core relation \textit{terminates} and is in
fact \textit{deterministic}. Moreover, we see from the residual goals that
the constraint solver has deduced more stringent bounds for all
variables. Such observations are only possible if modeling and search
parts are cleanly separated.

Labeling can then be used to search for solutions in a separate
predicate or goal:

\begin{code}
?- puzzle(As+Bs=Cs), label(As).
As = [9, 5, 6, 7],
Bs = [1, 0, 8, 5],
Cs = [1, 0, 6, 5, 2] ;
false.
\end{code}

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.

\subsection{Example: Eight queens puzzle}

\label{sec:clpfd-n-queens}

We illustrate the concepts of the preceding sections by means of the
so-called \textit{eight queens puzzle}. The task is to place 8 queens on an
8x8 chessboard such that none of the queens is under attack. This
means that no two queens share the same row, column or diagonal.

To express this puzzle via CLP(FD) constraints, we must first pick a
suitable representation. Since CLP(FD) constraints reason over
\textit{integers}, we must find a way to map the positions of queens to
integers. Several such mappings are conceivable, and it is not
immediately obvious which we should use. On top of that, different
constraints can be used to express the desired relations. For such
reasons, \textit{modeling} combinatorial problems via CLP(FD) constraints
often necessitates some creativity and has been described as more of
an art than a science.

In our concrete case, we observe that there must be exactly one queen
per column. The following representation therefore suggests itself: We
are looking for 8 integers, one for each column, where each integer
denotes the \textit{row} of the queen that is placed in the respective
column, and which are subject to certain constraints.

In fact, let us now generalize the task to the so-called \textit{N queens
puzzle}, which is obtained by replacing 8 by \textit{N} everywhere it occurs
in the above description. We implement the above considerations in the
\textbf{core relation} \predref{n_queens}{2}, where the first argument is the number
of queens (which is identical to the number of rows and columns of the
generalized chessboard), and the second argument is a list of \textit{N}
integers that represents a solution in the form described above.

\begin{code}
n_queens(N, Qs) :-
        length(Qs, N),
        Qs ins 1..N,
        safe_queens(Qs).

safe_queens([]).
safe_queens([Q|Qs]) :- safe_queens(Qs, Q, 1), safe_queens(Qs).

safe_queens([], _, _).
safe_queens([Q|Qs], Q0, D0) :-
        Q0 #\= Q,
        abs(Q0 - Q) #\= D0,
        D1 #= D0 + 1,
        safe_queens(Qs, Q0, D1).
\end{code}

Note that all these predicates can be used in \textit{all directions}: We
can use them to \textit{find} solutions, \textit{test} solutions and \textit{complete}
partially instantiated solutions.

The original task can be readily solved with the following query:

\begin{code}
?- n_queens(8, Qs), label(Qs).
Qs = [1, 5, 8, 6, 3, 7, 2, 4] .
\end{code}

Using suitable labeling strategies, we can easily find solutions with
80 queens and more:

\begin{code}
?- n_queens(80, Qs), labeling([ff], Qs).
Qs = [1, 3, 5, 44, 42, 4, 50, 7, 68|...] .

?- time((n_queens(90, Qs), labeling([ff], Qs))).
% 5,904,401 inferences, 0.722 CPU in 0.737 seconds (98% CPU)
Qs = [1, 3, 5, 50, 42, 4, 49, 7, 59|...] .
\end{code}

Experimenting with different search strategies is easy because we have
separated the core relation from the actual search.

\subsection{Optimisation}

\label{sec:clpfd-optimisation}

We can use \predref{labeling}{2} to minimize or maximize the value of a CLP(FD)
expression, and generate solutions in increasing or decreasing order
of the value. See the labeling options \verb$min(Expr)$ and \verb$max(Expr)$,
respectively.

Again, to easily try different labeling options in connection with
optimisation, we recommend to introduce a dedicated predicate for
posting constraints, and to use \predref{labeling}{2} in a separate goal. This
way, we can observe properties of the core relation in isolation,
and try different labeling options without recompiling our code.

If necessary, we can use \predref{once}{1} to commit to the first optimal
solution. However, it is often very valuable to see alternative
solutions that are \textit{also} optimal, so that we can choose among optimal
solutions by other criteria. For the sake of
\href{https://www.metalevel.at/prolog/purity}{\textbf{purity}} and
completeness, we recommend to avoid \predref{once}{1} and other constructs that
lead to impurities in CLP(FD) programs.

Related to optimisation with CLP(FD) constraints are
\href{http://eu.swi-prolog.org/man/simplex.html}{\const{library(simplex)}} and
CLP(Q) which reason about \textit{linear} constraints over rational numbers.

\subsection{Reification}

\label{sec:clpfd-reification}

The constraints \predref{in}{2}, \predref{\Sceq}{2}, \predref{\Scne}{2}, \predref{\Sclt}{2}, \predref{\Scgt}{2}, \predref{\Scle}{2}, and \predref{\Scge}{2} can be
\textit{reified}, 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:

\begin{quote}
\begin{tabulary}{0.9\textwidth}{|l|L|}
\hline
\Scnot{} Q & True iff Q is false \\
P \Scor{} Q & True iff either P or Q \\
P \Scand{} Q & True iff both P and Q \\
P \Scnot{} Q & True iff either P or Q, but not both \\
P \Scequal{} Q & True iff P and Q are equivalent \\
P \Srimplies{} Q & True iff P implies Q \\
P \Slimplies{} Q & True iff Q implies P \\
\hline
\end{tabulary}
\end{quote}

The constraints of this table are reifiable as well.

When reasoning over Boolean variables, also consider using
CLP(B) constraints as provided by
\href{http://eu.swi-prolog.org/man/clpb.html}{\const{library(clpb)}}.

\subsection{Enabling monotonic CLP(FD)}

\label{sec:clpfd-monotonicity}

In the default execution mode, CLP(FD) constraints still exhibit some
non-relational properties. For example, \textit{adding} constraints can yield
new solutions:

\begin{code}
?-          X #= 2, X = 1+1.
false.

?- X = 1+1, X #= 2, X = 1+1.
X = 1+1.
\end{code}

This behaviour is highly problematic from a logical point of view, and
it may render declarative debugging techniques inapplicable.

Set the Prolog flag \prologflag{clpfd_monotonic} to \const{true} to make CLP(FD)
\textbf{monotonic}: This means that \textit{adding} new constraints \textit{cannot} yield
new solutions. When this flag is \const{true}, we must wrap variables that
occur in arithmetic expressions with the functor \verb$(?)/1$ or \verb$(#)/1$. For
example:

\begin{code}
?- set_prolog_flag(clpfd_monotonic, true).
true.

?- #(X) #= #(Y) + #(Z).
#(Y)+ #(Z)#= #(X).

?-          X #= 2, X = 1+1.
ERROR: Arguments are not sufficiently instantiated
\end{code}

The wrapper can be omitted for variables that are already constrained
to integers.

\subsection{Custom constraints}

\label{sec:clpfd-custom-constraints}

We can 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 \verb$oneground(X,Y,Z)$, where Z shall be 1 if at least
one of X and Y is instantiated:

\begin{code}
:- 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) -> clpfd:kill(MState), Z = 1
        ;   integer(Y) -> clpfd:kill(MState), Z = 1
        ;   true
        ).
\end{code}

First, \qpredref{clpfd}{make_propagator}{2} is used to transform a user-defined
representation of the new constraint to an internal form. With
\qpredref{clpfd}{init_propagator}{2}, 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, \qpredref{clpfd}{trigger_once}{1} is used to give the
propagator its first chance for propagation even though the variables'
domains have not yet changed. Finally, \qpredref{clpfd}{run_propagator}{2} 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
\qpredref{clpfd}{make_propagator}{2}, 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 \qpredref{clpfd}{kill}{1}. An example
of using the new constraint:

\begin{code}
?- oneground(X, Y, Z), Y = 5.
Y = 5,
Z = 1,
X in inf..sup.
\end{code}

\subsection{Applications}

\label{sec:clpfd-applications}

CLP(FD) applications that we find particularly impressive and worth
studying include:

\begin{itemize}
    \item Michael Hendricks uses CLP(FD) constraints for flexible reasoning
about \textit{dates} and \textit{times} in the
\href{http://www.swi-prolog.org/pack/list?p=julian}{\const{julian}} package.
    \item Julien Cumin uses CLP(FD) constraints for integer arithmetic in
\href{https://github.com/JCumin/Brachylog}{\const{Brachylog}}.
\end{itemize}

\subsection{Acknowledgments}

\label{sec:clpfd-acknowledgments}

This library gives you a glimpse of what \href{https://sicstus.sics.se/}{\textbf{SICStus
Prolog}} can do. The API is intentionally
mostly compatible with that of SICStus Prolog, so that you can easily
switch to a much more feature-rich and much faster CLP(FD) system when
you need it. I thank \href{https://www.sics.se/~matsc/}{Mats Carlsson}, the
designer and main implementor of SICStus Prolog, for his elegant
example. I first encountered his system as part of the excellent
\href{http://www.complang.tuwien.ac.at/ulrich/gupu/}{\textbf{GUPU}} teaching
environment by \href{http://www.complang.tuwien.ac.at/ulrich/}{Ulrich
Neumerkel}. Ulrich was also
the first and most determined tester of the present system, filing
hundreds of comments and suggestions for improvement. \href{https://people.cs.kuleuven.be/~tom.schrijvers/}{Tom
Schrijvers} has
contributed several constraint libraries to SWI-Prolog, and I learned
a lot from his coding style and implementation examples. \href{https://people.cs.kuleuven.be/~bart.demoen/}{Bart
Demoen} was a driving
force behind the implementation of attributed variables in SWI-Prolog,
and this library could not even have started without his prior work
and contributions. Thank you all!

\subsection{CLP(FD) predicate index}

\label{sec:clpfd-predicate-index}

In the following, each CLP(FD) predicate is described in more detail.

We recommend the following link to refer to this manual:

\url{http://eu.swi-prolog.org/man/clpfd.html}

\subsubsection{Arithmetic constraints}

\label{sec:clpfd-arithmetic}

\textit{Arithmetic} constraints are the most basic use of CLP(FD). Every time
you use \verb$(is)/2$ or one of the low-level arithmetic comparisons
(\verb$(<)/2$, \verb$(>)/2$ etc.) over integers, consider using CLP(FD)
constraints \textit{instead}. This can at most \textit{increase} the generality of
your programs. See declarative integer
arithmetic (\secref{clpfd-integer-arith}).

\begin{description}
    \infixop{\Sceq}{?X}{?Y}
The arithmetic expression \arg{X} equals \arg{Y}. This is the most important
arithmetic constraint (\secref{clpfd-arith-constraints}), subsuming and
replacing both \verb$(is)/2$ \textit{and} \verb$(=:=)/2$ over integers. See
declarative integer arithmetic (\secref{clpfd-integer-arith}).

    \infixop{\Scne}{?X}{?Y}
The arithmetic expressions \arg{X} and \arg{Y} evaluate to distinct integers.
When reasoning over integers, replace \verb$(=\=)/2$ by \predref{\Scne}{2} to obtain
more general relations. See declarative integer
arithmetic (\secref{clpfd-integer-arith}).

    \infixop{\Scge}{?X}{?Y}
Same as \arg{Y} \Scle{} \arg{X}. When reasoning over integers, replace \verb$(>=)/2$ by
\predref{\Scge}{2} to obtain more general relations. See declarative integer
arithmetic (\secref{clpfd-integer-arith}).

    \infixop{\Scle}{?X}{?Y}
The arithmetic expression \arg{X} is less than or equal to \arg{Y}. When
reasoning over integers, replace \verb$(=<)/2$ by \predref{\Scle}{2} to obtain more
general relations. See declarative integer
arithmetic (\secref{clpfd-integer-arith}).

    \infixop{\Scgt}{?X}{?Y}
Same as \arg{Y} \Sclt{} \arg{X}. When reasoning over integers, replace \verb$(>)/2$ by
\predref{\Scgt}{2} to obtain more general relations See declarative integer
arithmetic (\secref{clpfd-integer-arith}).

    \infixop{\Sclt}{?X}{?Y}
The arithmetic expression \arg{X} is less than \arg{Y}. When reasoning over
integers, replace \verb$(<)/2$ by \predref{\Sclt}{2} to obtain more general relations. See
declarative integer arithmetic (\secref{clpfd-integer-arith}).

In addition to its regular use in tasks 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:

\begin{code}
?- Vs = [A,B,C,D], Vs ins 1..4,
        all_different(Vs),
        A #< B, C #< D, A #< 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)].
\end{code}

\end{description}

\subsubsection{Membership constraints}

\label{sec:clpfd-membership}

If you are using CLP(FD) to model and solve combinatorial tasks, then
you typically need to specify the admissible domains of variables.
The \textit{membership constraints} \predref{in}{2} and \predref{ins}{2} are useful in such cases.

\begin{description}
    \infixop{in}{?Var}{+Domain}
\arg{Var} is an element of \arg{Domain}. \arg{Domain} is one of:

\begin{description}
    \termitem{\arg{Integer}}{}
Singleton set consisting only of \textit{\arg{Integer}}.
    \infixtermitem{..}{\arg{Lower}}{\arg{Upper}}
All integers \textit{I} such that \textit{\arg{Lower}} \Sle{} \textit{I} \Sle{} \textit{\arg{Upper}}.
\textit{\arg{Lower}} must be an integer or the atom \textbf{inf}, which
denotes negative infinity. \textit{\arg{Upper}} must be an integer or
the atom \textbf{sup}, which denotes positive infinity.
    \infixtermitem{\Sor}{\arg{Domain1}}{\arg{Domain2}}
The union of \arg{Domain1} and \arg{Domain2}.
\end{description}

    \infixop{ins}{+Vars}{+Domain}
The variables in the list \arg{Vars} are elements of \arg{Domain}. See \predref{in}{2} for
the syntax of \arg{Domain}.
\end{description}

\subsubsection{Enumeration predicates}

\label{sec:clpfd-enumeration}

When modeling combinatorial tasks, the actual search for solutions is
typically performed by \textit{enumeration predicates} like \predref{labeling}{2}. See
the the section about \textit{core relations} and search for more
information.

\begin{description}
    \predicate{indomain}{1}{?Var}
Bind \arg{Var} to all feasible values of its domain on backtracking. The
domain of \arg{Var} must be finite.

    \predicate{label}{1}{+Vars}
Equivalent to \verb$labeling([], Vars)$. See \predref{labeling}{2}.

    \predicate{labeling}{2}{+Options, +Vars}
Assign a value to each variable in \arg{Vars}. Labeling means systematically
trying out values for the finite domain variables \arg{Vars} until all of
them are ground. The domain of each variable in \arg{Vars} must be finite.
\arg{Options} is a list of options that let you exhibit some control over
the search process. Several categories of options exist:

The variable selection strategy lets you specify which variable of
\arg{Vars} is labeled next and is one of:

\begin{description}
    \termitem{leftmost}{}
Label the variables in the order they occur in \arg{Vars}. This is the
default.
    \termitem{ff}{}
\textit{First fail}. Label the leftmost variable with smallest domain next,
in order to detect infeasibility early. This is often a good
strategy.
    \termitem{ffc}{}
Of the variables with smallest domains, the leftmost one
participating in most constraints is labeled next.
    \termitem{min}{}
Label the leftmost variable whose lower bound is the lowest next.
    \termitem{max}{}
Label the leftmost variable whose upper bound is the highest next.
\end{description}

The value order is one of:

\begin{description}
    \termitem{up}{}
Try the elements of the chosen variable's domain in ascending order.
This is the default.
    \termitem{down}{}
Try the domain elements in descending order.
\end{description}

The branching strategy is one of:

\begin{description}
    \termitem{step}{}
For each variable X, a choice is made between X = V and X \Scne{} V,
where V is determined by the value ordering options. This is the
default.
    \termitem{enum}{}
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.
    \termitem{bisect}{}
For each variable X, a choice is made between X \Scle{} M and X \Scgt{} M,
where M is the midpoint of the domain of X.
\end{description}

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

The order of solutions can be influenced with:

\begin{shortlist}
    \item \verb$min(Expr)$
    \item \verb$max(Expr)$
\end{shortlist}

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

\begin{code}
?- [X,Y] ins 10..20, labeling([max(X),min(Y)],[X,Y]).
\end{code}

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
"\verb$maximize(Expr)$" and "\verb$minimize(Expr)$", use \predref{once}{1}, e.g.:

\begin{code}
once(labeling([max(Expr)], Vars))
\end{code}

Labeling is always complete, always terminates, and yields no
redundant solutions. See core relations and
search (\secref{clpfd-search}) for usage advice.
\end{description}

\subsubsection{Global constraints}

\label{sec:clpfd-global}

A \textit{global constraint} expresses a relation that involves many
variables at once. The most frequently used global constraints of this
library are the combinatorial constraints \predref{all_distinct}{1},
\predref{global_cardinality}{2} and \predref{cumulative}{2}.

\begin{description}
    \predicate{all_distinct}{1}{+Vars}
True iff \arg{Vars} are pairwise distinct. For example, \predref{all_distinct}{1}
can detect that not all variables can assume distinct values given
the following domains:

\begin{code}
?- maplist(in, Vs,
           [1\/3..4, 1..2\/4, 1..2\/4, 1..3, 1..3, 1..6]),
   all_distinct(Vs).
false.
\end{code}

    \predicate{all_different}{1}{+Vars}
Like \predref{all_distinct}{1}, but with weaker propagation. Consider using
\predref{all_distinct}{1} instead, since \predref{all_distinct}{1} is typically acceptably
efficient and propagates much more strongly.

    \predicate{sum}{3}{+Vars, +Rel, ?Expr}
The sum of elements of the list \arg{Vars} is in relation \arg{Rel} to \arg{Expr}.
\arg{Rel} is one of \#=, \#\bsl{}=, \#$<$, \#$>$, \Scle{} or \#$>$=. For example:

\begin{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.
\end{code}

    \predicate{scalar_product}{4}{+Cs, +Vs, +Rel, ?Expr}
True iff the scalar product of \arg{Cs} and \arg{Vs} is in relation \arg{Rel} to \arg{Expr}.
\arg{Cs} is a list of integers, \arg{Vs} is a list of variables and integers.
\arg{Rel} is \#=, \#\bsl{}=, \#$<$, \#$>$, \Scle{} or \#$>$=.

    \predicate{lex_chain}{1}{+Lists}
\arg{Lists} are lexicographically non-decreasing.

    \predicate{tuples_in}{2}{+Tuples, +Relation}
True iff all \arg{Tuples} are elements of \arg{Relation}. Each element of the
list \arg{Tuples} is a list of integers or finite domain variables.
\arg{Relation} is a list of lists of integers. 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:

\begin{code}
?- tuples_in([[X,Y]], [[1,2],[1,5],[4,0],[4,3]]), X = 4.
X = 4,
Y in 0\/3.
\end{code}

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.

\begin{code}
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 #> T1,
        T4 #> T3,
        trains(Ts),
        tuples_in(Ps, Ts).
\end{code}

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

\begin{code}
?- threepath(1, 4, Ps).
Ps = [[1, 2, 0, 1], [2, 3, 4, 5], [3, 4, 8, 9]].
\end{code}

    \predicate{serialized}{2}{+Starts, +Durations}
Describes a set of non-overlapping tasks.
\arg{Starts} = [S_1,...,S_n], is a list of variables or integers,
\arg{Durations} = [D_1,...,D_n] is a list of non-negative integers.
Constrains \arg{Starts} and \arg{Durations} to denote a set of
non-overlapping tasks, i.e.: S_i + D_i \Sle{} S_j or S_j + D_j \Sle{}
S_i for all 1 \Sle{} i $<$ j \Sle{} n. Example:

\begin{code}
?- length(Vs, 3),
   Vs ins 0..3,
   serialized(Vs, [1,2,3]),
   label(Vs).
Vs = [0, 1, 3] ;
Vs = [2, 0, 3] ;
false.
\end{code}

\begin{tags}
    \tag{See also}
Dorndorf et al. 2000, "Constraint Propagation Techniques for the
Disjunctive Scheduling Problem"
\end{tags}

    \predicate{element}{3}{?N, +Vs, ?V}
The \arg{N}-th element of the list of finite domain variables \arg{Vs} is \arg{V}.
Analogous to \predref{nth1}{3}.

    \predicate{global_cardinality}{2}{+Vs, +Pairs}
Global Cardinality constraint. Equivalent to
\verb$global_cardinality(Vs, Pairs, [])$. See \predref{global_cardinality}{3}.

Example:

\begin{code}
?- Vs = [_,_,_], global_cardinality(Vs, [1-2,3-_]), label(Vs).
Vs = [1, 1, 3] ;
Vs = [1, 3, 1] ;
Vs = [3, 1, 1].
\end{code}

    \predicate{global_cardinality}{3}{+Vs, +Pairs, +Options}
Global Cardinality constraint. \arg{Vs} is a list of finite domain
variables, \arg{Pairs} 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 \arg{Vs} is equal to some key, and for each Key-Num pair
in \arg{Pairs}, the number of occurrences of Key in \arg{Vs} is Num. \arg{Options}
is a list of options. Supported options are:

\begin{description}
    \termitem{consistency}{value}
A weaker form of consistency is used.
    \termitem{cost}{Cost, Matrix}
\arg{Matrix} is a list of rows, one for each variable, in the order
they occur in \arg{Vs}. Each of these rows is a list of integers, one
for each key, in the order these keys occur in \arg{Pairs}. When
variable v_i is assigned the value of key k_j, then the
associated cost is \arg{Matrix}_\{ij\}. \arg{Cost} is the sum of all costs.
\end{description}

    \predicate{circuit}{1}{+Vs}
True iff the list \arg{Vs} of finite domain variables induces a
Hamiltonian circuit. The k-th element of \arg{Vs} denotes the
successor of node k. Node indexing starts with 1. Examples:

\begin{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] .
\end{code}

    \predicate{cumulative}{1}{+Tasks}
Equivalent to \verb$cumulative(Tasks, [limit(1)])$. See \predref{cumulative}{2}.

    \predicate{cumulative}{2}{+Tasks, +Options}
Schedule with a limited resource. \arg{Tasks} is a list of tasks, each of
the form \verb$task(S_i, D_i, E_i, C_i, T_i)$. 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 iff at each time slot 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. \arg{Options} is a list of options. Currently, the only supported
option is:

\begin{description}
    \termitem{limit}{L}
The integer \arg{L} is the global resource limit. Default is 1.
\end{description}

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

\begin{code}
tasks_starts(Tasks, [S1,S2,S3]) :-
        Tasks = [task(S1,3,_,1,_),
                 task(S2,2,_,1,_),
                 task(S3,2,_,1,_)].
\end{code}

We can use \predref{cumulative}{2} as follows, and obtain a schedule:

\begin{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] .
\end{code}

    \predicate{disjoint2}{1}{+Rectangles}
True iff \arg{Rectangles} are not overlapping. \arg{Rectangles} is a list of
terms of the form F(X_i, W_i, Y_i, H_i), where F is any functor,
and the arguments are finite domain variables or integers that
denote, respectively, the X coordinate, width, Y coordinate and
height of each rectangle.

    \predicate{automaton}{3}{+Vs, +Nodes, +Arcs}
Describes a list of finite domain variables with a finite
automaton. Equivalent to \verb$automaton(Vs, _, Vs, Nodes, Arcs, [], [], _)$, a common use case of \predref{automaton}{8}. In the following
example, a list of binary finite domain variables is constrained to
contain at least two consecutive ones:

\begin{code}
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)]).
\end{code}

Example query:

\begin{code}
?- length(Vs, 3), two_consecutive_ones(Vs), label(Vs).
Vs = [0, 1, 1] ;
Vs = [1, 1, 0] ;
Vs = [1, 1, 1].
\end{code}

    \predicate{automaton}{8}{+Sequence, ?Template, +Signature, +Nodes, +Arcs, +Counters, +Initials, ?Finals}
Describes a list of finite domain variables with a finite
automaton. True iff the finite automaton induced by \arg{Nodes} and \arg{Arcs}
(extended with \arg{Counters}) accepts \arg{Signature}. \arg{Sequence} is a list of
terms, all of the same shape. Additional constraints must link
\arg{Sequence} to \arg{Signature}, if necessary. \arg{Nodes} is a list of
\verb$source(Node)$ and \verb$sink(Node)$ terms. \arg{Arcs} is a list of
\verb$arc(Node,Integer,Node)$ and \verb$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. \arg{Exprs} is a list of arithmetic expressions,
of the same length as \arg{Counters}. In each expression, variables
occurring in \arg{Counters} symbolically refer to previous counter
values, and variables occurring in \arg{Template} refer to the current
element of \arg{Sequence}. When a transition containing arithmetic
expressions is taken, each counter is updated according to the
result of the corresponding expression. When a transition without
arithmetic expressions is taken, all counters remain unchanged.
\arg{Counters} is a list of variables. \arg{Initials} is a list of finite
domain variables or integers denoting, in the same order, the
initial value of each counter. These values are related to \arg{Finals}
according to the arithmetic expressions of the taken transitions.

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:

\begin{code}
sequence_inflexions(Vs, N) :-
        variables_signature(Vs, Sigs),
        automaton(Sigs, _, 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 #<==> S #= 0,
        Prev #< V #<==> S #= 1,
        Prev #> V #<==> S #= 2,
        variables_signature_(Vs, V, Sigs).
\end{code}

Example queries:

\begin{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].
\end{code}

    \predicate{chain}{2}{+Zs, +Relation}
\arg{Zs} form a chain with respect to \arg{Relation}. \arg{Zs} is a list of finite
domain variables that are a chain with respect to the partial order
\arg{Relation}, in the order they appear in the list. \arg{Relation} must be \#=,
\#=$<$, \#$>$=, \Sclt{} or \#$>$. For example:

\begin{code}
?- chain([X,Y,Z], #>=).
X#>=Y,
Y#>=Z.
\end{code}

\end{description}

\subsubsection{Reification predicates}

\label{sec:clpfd-reification-predicates}

Many CLP(FD) constraints can be \textit{reified}. This means that their truth
value is itself turned into a CLP(FD) variable, so that we can
explicitly reason about whether a constraint holds or not. See
reification (\secref{clpfd-reification}).

\begin{description}
    \prefixop{\Scnot}{+Q}
\arg{Q} does \textit{not} hold. See reification (\secref{clpfd-reification}).

For example, to obtain the complement of a domain:

\begin{code}
?- #\ X in -3..0\/10..80.
X in inf.. -4\/1..9\/81..sup.
\end{code}

    \infixop{\Scequal}{?P}{?Q}
\arg{P} and \arg{Q} are equivalent. See reification (\secref{clpfd-reification}).

For example:

\begin{code}
?- X #= 4 #<==> B, X #\= 4.
B = 0,
X in inf..3\/5..sup.
\end{code}

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

\begin{code}
vs_n_num(Vs, N, Num) :-
        maplist(eq_b(N), Vs, Bs),
        sum(Bs, #=, Num).

eq_b(X, Y, B) :- X #= Y #<==> B.
\end{code}

Sample queries and their results:

\begin{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.
\end{code}

    \infixop{\Srimplies}{?P}{?Q}
\arg{P} implies \arg{Q}. See reification (\secref{clpfd-reification}).

    \infixop{\Slimplies}{?P}{?Q}
\arg{Q} implies \arg{P}. See reification (\secref{clpfd-reification}).

    \infixop{\Scand}{?P}{?Q}
\arg{P} and \arg{Q} hold. See reification (\secref{clpfd-reification}).

    \infixop{\Scor}{?P}{?Q}
\arg{P} or \arg{Q} holds. See reification (\secref{clpfd-reification}).

For example, the sum of natural numbers below 1000 that are
multiples of 3 or 5:

\begin{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.
\end{code}

    \infixop{\Scnot}{?P}{?Q}
Either \arg{P} holds or \arg{Q} holds, but not both. See
reification (\secref{clpfd-reification}).

    \predicate{zcompare}{3}{?Order, ?A, ?B}
Analogous to \predref{compare}{3}, with finite domain variables \arg{A} and \arg{B}.

Think of \predref{zcompare}{3} as \textit{reifying} an arithmetic comparison of two
integers. This means that we can explicitly reason about the
different cases \textit{within} our programs. As in \predref{compare}{3}, the atoms
\verb$<$, \verb$>$ and \verb$=$ denote the different cases of the
trichotomy. In contrast to \predref{compare}{3} though, \predref{zcompare}{3} works
correctly for \textit{all modes}, also if only a subset of the arguments is
instantiated. This allows you to make several predicates over
integers deterministic while preserving their generality and
completeness. For example:

\begin{code}
n_factorial(N, F) :-
        zcompare(C, N, 0),
        n_factorial_(C, N, F).

n_factorial_(=, _, 1).
n_factorial_(>, N, F) :-
        F #= F0*N,
        N1 #= N - 1,
        n_factorial(N1, F0).
\end{code}

This version of \predref{n_factorial}{2} is deterministic if the first argument
is instantiated, because argument indexing can distinguish the
different clauses that reflect the possible and admissible outcomes
of a comparison of \arg{N} against 0. Example:

\begin{code}
?- n_factorial(30, F).
F = 265252859812191058636308480000000.
\end{code}

Since there is no clause for \verb$<$, the predicate automatically
\textit{fails} if \arg{N} is less than 0. The predicate can still be used in
all directions, including the most general query:

\begin{code}
?- n_factorial(N, F).
N = 0,
F = 1 ;
N = F, F = 1 ;
N = F, F = 2 .
\end{code}

In this case, all clauses are tried on backtracking, and \predref{zcompare}{3}
ensures that the respective ordering between N and 0 holds in each
case.

The truth value of a comparison can also be reified with (\Scequal{})/2
in combination with one of the \textit{arithmetic
constraints} (\secref{clpfd-arith-constraints}). See
reification (\secref{clpfd-reification}). However, \predref{zcompare}{3} lets you
more conveniently distinguish the cases.
\end{description}

\subsubsection{Reflection predicates}

\label{sec:clpfd-reflection-predicates}

Reflection predicates let us obtain, in a well-defined way,
information that is normally internal to this library. In addition to
the predicates explained below, also take a look at
\predref{call_residue_vars}{2} and \predref{copy_term}{3} to reason about CLP(FD)
constraints that arise in programs. This can be useful in program
analyzers and declarative debuggers.

\begin{description}
    \predicate{fd_var}{1}{+Var}
True iff \arg{Var} is a CLP(FD) variable.

    \predicate{fd_inf}{2}{+Var, -Inf}
\arg{Inf} is the infimum of the current domain of \arg{Var}.

    \predicate{fd_sup}{2}{+Var, -Sup}
\arg{Sup} is the supremum of the current domain of \arg{Var}.

    \predicate{fd_size}{2}{+Var, -Size}
Reflect the current size of a domain. \arg{Size} is the number of
elements of the current domain of \arg{Var}, or the atom \textbf{sup} if the
domain is unbounded.

    \predicate{fd_dom}{2}{+Var, -Dom}
\arg{Dom} is the current domain (see \predref{in}{2}) of \arg{Var}. This predicate is
useful if you want to reason about domains. It is \textit{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.

For example, to implement a custom labeling strategy, you may need
to inspect the current domain of a finite domain variable. With the
following code, you can convert a \textit{finite} domain to a list of
integers:

\begin{code}
dom_integers(D, Is) :- phrase(dom_integers_(D), Is).

dom_integers_(I)      --> { integer(I) }, [I].
dom_integers_(L..U)   --> { numlist(L, U, Is) }, Is.
dom_integers_(D1\/D2) --> dom_integers_(D1), dom_integers_(D2).
\end{code}

Example:

\begin{code}
?- X in 1..5, X #\= 4, fd_dom(X, D), dom_integers(D, Is).
D = 1..3\/5,
Is = [1,2,3,5],
X in 1..3\/5.
\end{code}

    \predicate[det]{fd_degree}{2}{+Var, -Degree}
\arg{Degree} is the number of constraints currently attached to \arg{Var}.
\end{description}

\subsubsection{FD set predicates}

\label{sec:clpfd-fdset-predicates}

These predicates allow operating directly on the internal representation
of CLP(FD) domains. In this context, such an internal domain
representation is called an \textbf{FD set}.

Note that the exact term representation of FD sets is unspecified and
will vary across CLP(FD) implementations or even different versions of
the same implementation. FD set terms should be manipulated \textbf{only}
using the predicates in this section. The behavior of other operations
on FD set terms is undefined. In particular, you should \textbf{not} construct
or deconstruct FD sets by unification, and you \textbf{cannot} reliably compare
FD sets using unification or generic term equality/comparison
predicates.

\begin{description}
    \infixop{in_set}{?Var}{+Set}
\arg{Var} is an element of the FD set \arg{Set}.

    \predicate[det]{fd_set}{2}{?Var, -Set}
\arg{Set} is the FD set representation of the current domain of \arg{Var}.

    \predicate[semidet]{is_fdset}{1}{@Set}
\arg{Set} is currently bound to a valid FD set.

    \predicate[det]{empty_fdset}{1}{-Set}
\arg{Set} is the empty FD set.

    \predicate[semidet]{fdset_parts}{4}{?Set, ?Min, ?Max, ?Rest}
\arg{Set} is a non-empty FD set representing the domain \arg{Min}..\arg{Max} \Sor{} \arg{Rest},
where \arg{Min}..\arg{Max} is a non-empty interval (see \predref{fdset_interval}{3})
and \arg{Rest} is another FD set (possibly empty).

If \arg{Max} is \textbf{sup}, then \arg{Rest} is the empty FD set. Otherwise, if \arg{Rest}
is non-empty, all elements of \arg{Rest} are greater than \arg{Max}+1.

This predicate should only be called with either \arg{Set} or all other
arguments being ground.

    \predicate[semidet]{empty_interval}{2}{+Min, +Max}
\arg{Min}..\arg{Max} is an empty interval. \arg{Min} and \arg{Max} are integers or one of the
atoms \textbf{inf} or \textbf{sup}.

    \predicate[semidet]{fdset_interval}{3}{?Interval, ?Min, ?Max}
\arg{Interval} is a non-empty FD set consisting of the single interval
\arg{Min}..\arg{Max}.
\arg{Min} is an integer or the atom \textbf{inf} to denote negative infinity.
\arg{Max} is an integer or the atom \textbf{sup} to denote positive infinity.

Either \arg{Interval} or \arg{Min} and \arg{Max} must be ground.

    \predicate[semidet]{fdset_singleton}{2}{?Set, ?Elt}
\arg{Set} is the FD set containing the single integer \arg{Elt}.

Either \arg{Set} or \arg{Elt} must be ground.

    \predicate[semidet]{fdset_min}{2}{+Set, -Min}
\arg{Min} is the lower bound (infimum) of the non-empty FD set \arg{Set}.
\arg{Min} is an integer or the atom \textbf{inf} if \arg{Set} has no lower bound.

    \predicate[semidet]{fdset_max}{2}{+Set, -Max}
\arg{Max} is the upper bound (supremum) of the non-empty FD set \arg{Set}.
\arg{Max} is an integer or the atom \textbf{sup} if \arg{Set} has no upper bound.

    \predicate[det]{fdset_size}{2}{+Set, -Size}
\arg{Size} is the number of elements of the FD set \arg{Set}, or the atom \textbf{sup}
if \arg{Set} is infinite.

    \predicate[det]{list_to_fdset}{2}{+List, -Set}
\arg{Set} is an FD set containing all elements of \arg{List}, which must be a
list of integers.

    \predicate[det]{fdset_to_list}{2}{+Set, -List}
\arg{List} is a list containing all elements of the finite FD set \arg{Set},
in ascending order.

    \predicate[det]{range_to_fdset}{2}{+Domain, -Set}
\arg{Set} is an FD set equivalent to the domain \arg{Domain}. \arg{Domain} uses the
same syntax as accepted by (in)/2.

    \predicate[det]{fdset_to_range}{2}{+Set, -Domain}
\arg{Domain} is a domain equivalent to the FD set \arg{Set}. \arg{Domain} is returned
in the same format as by \predref{fd_dom}{2}.

    \predicate[det]{fdset_add_element}{3}{+Set1, +Elt, -Set2}
\arg{Set2} is the same FD set as \arg{Set1}, but with the integer \arg{Elt} added.
If \arg{Elt} is already in \arg{Set1}, the set is returned unchanged.

    \predicate[det]{fdset_del_element}{3}{+Set1, +Elt, -Set2}
\arg{Set2} is the same FD set as \arg{Set1}, but with the integer \arg{Elt} removed.
If \arg{Elt} is not in \arg{Set1}, the set returned unchanged.

    \predicate[semidet]{fdset_disjoint}{2}{+Set1, +Set2}
The FD sets \arg{Set1} and \arg{Set2} have no elements in common.

    \predicate[semidet]{fdset_intersect}{2}{+Set1, +Set2}
The FD sets \arg{Set1} and \arg{Set2} have at least one element in common.

    \predicate[det]{fdset_intersection}{3}{+Set1, +Set2, -Intersection}
\arg{Intersection} is an FD set (possibly empty) of all elements that the
FD sets \arg{Set1} and \arg{Set2} have in common.

    \predicate[nondet]{fdset_member}{2}{?Elt, +Set}
The integer \arg{Elt} is a member of the FD set \arg{Set}. If \arg{Elt} is unbound,
\arg{Set} must be finite and all elements are enumerated on backtracking.

    \predicate[semidet]{fdset_eq}{2}{+Set1, +Set2}
True if the FD sets \arg{Set1} and \arg{Set2} are equal, i. e. contain exactly
the same elements. This is not necessarily the same as unification or
a term equality check, because some FD sets have multiple possible
term representations.

    \predicate[semidet]{fdset_subset}{2}{+Set1, +Set2}
The FD set \arg{Set1} is a (non-strict) subset of \arg{Set2}, i. e. every element
of \arg{Set1} is also in \arg{Set2}.

    \predicate[det]{fdset_subtract}{3}{+Set1, +Set2, -Difference}
The FD set \arg{Difference} is \arg{Set1} with all elements of \arg{Set2} removed,
i. e. the set difference of \arg{Set1} and \arg{Set2}.

    \predicate[det]{fdset_union}{3}{+Set1, +Set2, -Union}
The FD set \arg{Union} is the union of FD sets \arg{Set1} and \arg{Set2}.

    \predicate[det]{fdset_union}{2}{+Sets, -Union}
The FD set \arg{Union} is the n-ary union of all FD sets in the list \arg{Sets}.
If \arg{Sets} is empty, \arg{Union} is the empty FD set.

    \predicate[det]{fdset_complement}{2}{+Set, -Complement}
The FD set \arg{Complement} is the complement of the FD set \arg{Set}.
Equivalent to \verb$fdset_subtract(inf..sup, Set, Complement)$.
\end{description}

\subsubsection{FD miscellaneous predicates}

\label{sec:clpfd-misc-predicates}

The predicates in this section are not \verb$clp(fd)$ predicates. They ended up
in this library for historical reasons and may be moved to other libraries
in the future.

\begin{description}
    \predicate{transpose}{2}{+Matrix, ?Transpose}
\arg{Transpose} a list of lists of the same length. Example:

\begin{code}
?- transpose([[1,2,3],[4,5,6],[7,8,9]], Ts).
Ts = [[1, 4, 7], [2, 5, 8], [3, 6, 9]].
\end{code}

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

\begin{code}
sudoku(Rows) :-
        length(Rows, 9), maplist(same_length(Rows), Rows),
        append(Rows, Vs), Vs ins 1..9,
        maplist(all_distinct, Rows),
        transpose(Rows, Columns),
        maplist(all_distinct, Columns),
        Rows = [As,Bs,Cs,Ds,Es,Fs,Gs,Hs,Is],
        blocks(As, Bs, Cs), blocks(Ds, Es, Fs), blocks(Gs, Hs, Is).

blocks([], [], []).
blocks([N1,N2,N3|Ns1], [N4,N5,N6|Ns2], [N7,N8,N9|Ns3]) :-
        all_distinct([N1,N2,N3,N4,N5,N6,N7,N8,N9]),
        blocks(Ns1, Ns2, Ns3).

problem(1, [[_,_,_,_,_,_,_,_,_],
            [_,_,_,_,_,3,_,8,5],
            [_,_,1,_,2,_,_,_,_],
            [_,_,_,5,_,7,_,_,_],
            [_,_,4,_,_,_,1,_,_],
            [_,9,_,_,_,_,_,_,_],
            [5,_,_,_,_,_,_,7,3],
            [_,_,2,_,1,_,_,_,_],
            [_,_,_,_,4,_,_,_,9]]).
\end{code}

Sample query:

\begin{code}
?- problem(1, Rows), sudoku(Rows), maplist(portray_clause, 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|...], ... , [...|...]].
\end{code}

\end{description}

\subsection{Closing and opening words about CLP(FD)}

\label{sec:clpfd-closing-opening}

CLP(FD) constraints are one of the main reasons why logic programming
approaches are picked over other paradigms for solving many tasks of
high practical relevance. The usefulness of CLP(FD) constraints for
scheduling, allocation and combinatorial optimization tasks is
well-known both in academia and industry.

With this library, we take the applicability of CLP(FD) constraints
one step further, following the road that visionary systems like
SICStus Prolog have already clearly outlined: This library is designed
to completely subsume and \textit{replace} low-level predicates over
integers, which were in the past repeatedly found to be a major
stumbling block when introducing logic programming to beginners.

Embrace the change and new opportunities that this paradigm allows!
Use CLP(FD) constraints in your programs. The use of CLP(FD)
constraints instead of low-level arithmetic is also a good indicator
to judge the quality of any introductory Prolog text.