Library for finite domain constraint solving.
An FD problem is specified as an expression of type FDConstr
using the constraints and expressions offered in this library.
FD variables are created by the operation domain
.
An FD problem is solved by calling solveFD
with labeling options,
the FD variables whose values should be included in the output,
and a constraint. Hence, the typical program structure to solve
an FD problem is as follows:
main :: [Int] main = let fdvars = take n (domain u o) fdmodel = {description of FD problem} in solveFD {options} fdvars fdmodel
where n
are the number of variables and [u..o]
is the
range of their possible values.
Author: Michael Hanus
Version: January 2024
domain
:: Int > Int > [FDExpr]
Operations to construct basic constraints. 
fd
:: Int > FDExpr
Represent an integer value as an FD expression. 
(=#)
:: FDExpr > FDExpr > FDConstr
Equality of FD expressions. 
(/=#)
:: FDExpr > FDExpr > FDConstr
Disequality of FD expressions. 
(<#)
:: FDExpr > FDExpr > FDConstr
"Less than" constraint on FD expressions. 
(<=#)
:: FDExpr > FDExpr > FDConstr
"Less than or equal" constraint on FD expressions. 
(>#)
:: FDExpr > FDExpr > FDConstr
"Greater than" constraint on FD expressions. 
(>=#)
:: FDExpr > FDExpr > FDConstr
"Greater than or equal" constraint on FD expressions. 
true
:: FDConstr
The always satisfied FD constraint. 
(/\)
:: FDConstr > FDConstr > FDConstr
Conjunction of FD constraints. 
andC
:: [FDConstr] > FDConstr
Conjunction of a list of FD constraints. 
allC
:: (a > FDConstr) > [a] > FDConstr
Maps a constraint abstraction to a list of FD constraints and joins them. 
allDifferent
:: [FDExpr] > FDConstr
"All different" constraint on FD variables. 
sum
:: [FDExpr] > FDRel > FDExpr > FDConstr
Relates the sum of FD variables with some integer of FD variable. 
scalarProduct
:: [FDExpr] > [FDExpr] > FDRel > FDExpr > FDConstr
(scalarProduct cs vs relop v)
is satisfied if (sum (cs*vs) relop v)
is satisfied.

count
:: FDExpr > [FDExpr] > FDRel > FDExpr > FDConstr
(count v vs relop c)
is satisfied if (n relop c) ,
where n
is the number of elements in the
list of FD variables vs
that are equal to v , is satisfied.

solveFD
:: [Option] > [FDExpr] > FDConstr > [Int]
Computes (nondeterministically) a solution for the FD variables (second argument) w.r.t. 
solveFDAll
:: [Option] > [FDExpr] > FDConstr > [[Int]]
Computes all solutions for the FD variables (second argument) w.r.t. 
solveFDOne
:: [Option] > [FDExpr] > FDConstr > [Int]
Computes a single solution for the FD variables (second argument) w.r.t. 
Possible relations between FD values.
Constructors:
Equ
:: FDRel
: Equal
Neq
:: FDRel
: Not equal
Lt
:: FDRel
: Less than
Leq
:: FDRel
: Less than or equal
Gt
:: FDRel
: Greater than
Geq
:: FDRel
: Greater than or equal
This datatype defines options to control the instantiation of FD variables in the solver (solveFD).
Constructors:
LeftMost
:: Option
: The leftmost variable is selected for instantiation (default)
FirstFail
:: Option
: The leftmost variable with the smallest domain is selected
(also known as firstfail principle)
FirstFailConstrained
:: Option
: The leftmost variable with the smallest domain
and the most constraints on it is selected.
Min
:: Option
: The leftmost variable with the smalled lower bound is selected.
Max
:: Option
: The leftmost variable with the greatest upper bound is selected.
Step
:: Option
: Make a binary choice between x=#b
and
x/=#b
for the selected variable
x
where b
is the lower or
upper bound of x
(default).
Enum
:: Option
: Make a multiple choice for the selected variable for all the values
in its domain.
Bisect
:: Option
: Make a binary choice between x<=#m
and
x>#m
for the selected variable
x
where m
is the midpoint
of the domain x
(also known as domain splitting).
Up
:: Option
: The domain is explored for instantiation in ascending order (default).
Down
:: Option
: The domain is explored for instantiation in descending order.
All
:: Option
: Enumerate all solutions by backtracking (default).
Minimize
:: Int > Option
: Find a solution that minimizes the domain variable v
(using a branchandbound algorithm).
Maximize
:: Int > Option
: Find a solution that maximizes the domain variable v
(using a branchandbound algorithm).
Assumptions
:: Int > Option
: The variable x is unified with the number of choices
made by the selected enumeration strategy when
a solution is found.
RandomVariable
:: Int > Option
: Select a random variable for instantiation
where x
is a seed value for the random numbers
(only supported by SWIProlog).
RandomValue
:: Int > Option
: Label variables with random integer values
where x
is a seed value for the random numbers
(only supported by SWIProlog).
Constructors:
Constructors:
Operations to construct basic constraints. Returns infinite list of FDVars with a given domain.

Represent an integer value as an FD expression.

Equality of FD expressions.

Disequality of FD expressions.

"Less than" constraint on FD expressions.

"Less than or equal" constraint on FD expressions.

"Greater than" constraint on FD expressions.

"Greater than or equal" constraint on FD expressions.

The always satisfied FD constraint.

Conjunction of FD constraints.

Maps a constraint abstraction to a list of FD constraints and joins them. 
"All different" constraint on FD variables.

Relates the sum of FD variables with some integer of FD variable.



Computes (nondeterministically) a solution for the FD variables (second argument) w.r.t. constraint (third argument), where the values in the solution correspond to the list of FD variables. The first argument contains options to control the labeling/instantiation of FD variables. 
Computes all solutions for the FD variables (second argument) w.r.t. constraint (third argument), where the values in each solution correspond to the list of FD variables. The first argument contains options to control the labeling/instantiation of FD variables. 
Computes a single solution for the FD variables (second argument) w.r.t. constraint (third argument), where the values in the solution correspond to the list of FD variables. The first argument contains options to control the labeling/instantiation of FD variables. 