Module CLP.FD

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: December 2018

Summary of exported operations:

domain :: Int -> Int -> [FDExpr]  Non-deterministic 
Operations to construct basic constraints.
fd :: Int -> FDExpr  Deterministic 
Represent an integer value as an FD expression.
(=#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 
Equality of FD expressions.
(/=#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 
Disequality of FD expressions.
(<#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 
"Less than" constraint on FD expressions.
(<=#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 
"Less than or equal" constraint on FD expressions.
(>#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 
"Greater than" constraint on FD expressions.
(>=#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 
"Greater than or equal" constraint on FD expressions.
true :: FDConstr  Deterministic 
The always satisfied FD constraint.
(/\) :: FDConstr -> FDConstr -> FDConstr  Deterministic 
Conjunction of FD constraints.
andC :: [FDConstr] -> FDConstr  Deterministic 
Conjunction of a list of FD constraints.
allC :: (a -> FDConstr) -> [a] -> FDConstr  Deterministic 
Maps a constraint abstraction to a list of FD constraints and joins them.
allDifferent :: [FDExpr] -> FDConstr  Deterministic 
"All different" constraint on FD variables.
sum :: [FDExpr] -> FDRel -> FDExpr -> FDConstr  Deterministic 
Relates the sum of FD variables with some integer of FD variable.
scalarProduct :: [FDExpr] -> [FDExpr] -> FDRel -> FDExpr -> FDConstr  Deterministic 
(scalarProduct cs vs relop v) is satisfied if (sum (cs*vs) relop v) is satisfied.
count :: FDExpr -> [FDExpr] -> FDRel -> FDExpr -> FDConstr  Deterministic 
(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]  Deterministic 
Computes (non-deterministically) a solution for the FD variables (second argument) w.r.t.
solveFDAll :: [Option] -> [FDExpr] -> FDConstr -> [[Int]]  Deterministic 
Computes all solutions for the FD variables (second argument) w.r.t.
solveFDOne :: [Option] -> [FDExpr] -> FDConstr -> [Int]  Deterministic 
Computes a single solution for the FD variables (second argument) w.r.t.

Exported datatypes:

FDRel

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
Option

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 first-fail 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 branch-and-bound algorithm).
  • Maximize :: Int -> Option : Find a solution that maximizes the domain variable v (using a branch-and-bound 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 SWI-Prolog).
  • RandomValue :: Int -> Option : Label variables with random integer values where x is a seed value for the random numbers (only supported by SWI-Prolog).
FDExpr

Constructors:

FDConstr

Constructors:

Exported operations:

domain :: Int -> Int -> [FDExpr]  Non-deterministic 

Operations to construct basic constraints. Returns infinite list of FDVars with a given domain.

Example call:
(domain min max)
Parameters:
  • min : minimum value for all variables in xs
  • max : maximum value for all variables in xs

fd :: Int -> FDExpr  Deterministic 

Represent an integer value as an FD expression.

Further infos:
  • solution complete, i.e., able to compute all solutions

(=#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 

Equality of FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(/=#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 

Disequality of FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(<#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 

"Less than" constraint on FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(<=#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 

"Less than or equal" constraint on FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(>#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 

"Greater than" constraint on FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

(>=#) :: FDExpr -> FDExpr -> FDConstr  Deterministic 

"Greater than or equal" constraint on FD expressions.

Further infos:
  • defined as non-associative infix operator with precedence 4
  • solution complete, i.e., able to compute all solutions

true :: FDConstr  Deterministic 

The always satisfied FD constraint.

Further infos:
  • solution complete, i.e., able to compute all solutions

(/\) :: FDConstr -> FDConstr -> FDConstr  Deterministic 

Conjunction of FD constraints.

Further infos:
  • defined as right-associative infix operator with precedence 3
  • solution complete, i.e., able to compute all solutions

andC :: [FDConstr] -> FDConstr  Deterministic 

Conjunction of a list of FD constraints.

allC :: (a -> FDConstr) -> [a] -> FDConstr  Deterministic 

Maps a constraint abstraction to a list of FD constraints and joins them.

allDifferent :: [FDExpr] -> FDConstr  Deterministic 

"All different" constraint on FD variables.

Example call:
(allDifferent xs)
Parameters:
  • xs : list of FD variables
Returns:
satisfied if the FD variables in the argument list xs have pairwise different values.
Further infos:
  • solution complete, i.e., able to compute all solutions

sum :: [FDExpr] -> FDRel -> FDExpr -> FDConstr  Deterministic 

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

Further infos:
  • solution complete, i.e., able to compute all solutions

scalarProduct :: [FDExpr] -> [FDExpr] -> FDRel -> FDExpr -> FDConstr  Deterministic 

(scalarProduct cs vs relop v) is satisfied if (sum (cs*vs) relop v) is satisfied. The first argument must be a list of integers. The other arguments are as in sum.

Further infos:
  • solution complete, i.e., able to compute all solutions

count :: FDExpr -> [FDExpr] -> FDRel -> FDExpr -> FDConstr  Deterministic 

(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. The first argument must be an integer. The other arguments are as in sum.

Further infos:
  • solution complete, i.e., able to compute all solutions

solveFD :: [Option] -> [FDExpr] -> FDConstr -> [Int]  Deterministic 

Computes (non-deterministically) 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.

solveFDAll :: [Option] -> [FDExpr] -> FDConstr -> [[Int]]  Deterministic 

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.

solveFDOne :: [Option] -> [FDExpr] -> FDConstr -> [Int]  Deterministic 

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.