Module CLPFD

Library for finite domain constraint solving. p The general structure of a specification of an FD problem is as follows:

codedomainconstraint & fdconstraint & labeling/code

where:

codedomain_constraint</code> specifies the possible range of the FD variables (see constraint <code>domain</code>)

codefd_constraint</code> specifies the constraint to be satisfied by a valid solution (see constraints #+, #-, allDifferent, etc below)

codelabeling/code is a labeling function to search for a concrete solution.

Note: This library is based on the corresponding library of Sicstus-Prolog but does not implement the complete functionality of the Sicstus-Prolog library. However, using the PAKCS interface for external functions, it is relatively easy to provide the complete functionality.

Author: Michael Hanus

Version: June 2012

Summary of exported operations:

 domain :: [Int] -> Int -> Int -> Bool    Constraint to specify the domain of all finite domain variables. (+#) :: Int -> Int -> Int    Addition of FD variables. (-#) :: Int -> Int -> Int    Subtraction of FD variables. (*#) :: Int -> Int -> Int    Multiplication of FD variables. (=#) :: Int -> Int -> Bool    Equality of FD variables. (/=#) :: Int -> Int -> Bool    Disequality of FD variables. (<#) :: Int -> Int -> Bool    "Less than" constraint on FD variables. (<=#) :: Int -> Int -> Bool    "Less than or equal" constraint on FD variables. (>#) :: Int -> Int -> Bool    "Greater than" constraint on FD variables. (>=#) :: Int -> Int -> Bool    "Greater than or equal" constraint on FD variables. (#=#) :: Int -> Int -> Constraint    Reifyable equality constraint on FD variables. (#/=#) :: Int -> Int -> Constraint    Reifyable inequality constraint on FD variables. (#<#) :: Int -> Int -> Constraint    Reifyable "less than" constraint on FD variables. (#<=#) :: Int -> Int -> Constraint    Reifyable "less than or equal" constraint on FD variables. (#>#) :: Int -> Int -> Constraint    Reifyable "greater than" constraint on FD variables. (#>=#) :: Int -> Int -> Constraint    Reifyable "greater than or equal" constraint on FD variables. neg :: Constraint -> Constraint    The resulting constraint is satisfied if both argument constraints are satisfied. (#/\#) :: Constraint -> Constraint -> Constraint    The resulting constraint is satisfied if both argument constraints are satisfied. (#\/#) :: Constraint -> Constraint -> Constraint    The resulting constraint is satisfied if both argument constraints are satisfied. (#=>#) :: Constraint -> Constraint -> Constraint    The resulting constraint is satisfied if the first argument constraint do not hold or both argument constraints are satisfied. (#<=>#) :: Constraint -> Constraint -> Constraint    The resulting constraint is satisfied if both argument constraint are either satisfied and do not hold. solve :: Constraint -> Bool    Solves a reified constraint. sum :: [Int] -> (Int -> Int -> Bool) -> Int -> Bool    Relates the sum of FD variables with some integer of FD variable. scalarProduct :: [Int] -> [Int] -> (Int -> Int -> Bool) -> Int -> Bool    (scalarProduct cs vs relop v) is satisfied if ((cs*vs) relop v) is satisfied. count :: Int -> [Int] -> (Int -> Int -> Bool) -> Int -> Bool    (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. allDifferent :: [Int] -> Bool    "All different" constraint on FD variables. all_different :: [Int] -> Bool    For backward compatibility. indomain :: Int -> Bool    Instantiate a single FD variable to its values in the specified domain. labeling :: [LabelingOption] -> [Int] -> Bool    Instantiate FD variables to their values in the specified domain.

Exported datatypes:

Constraint

A datatype to represent reifyable constraints.

Constructors:

LabelingOption

This datatype contains all options to control the instantiated of FD variables with the enumeration constraint codelabeling/code.

Constructors:

• LeftMost :: LabelingOption : The leftmost variable is selected for instantiation (default)
• FirstFail :: LabelingOption : The leftmost variable with the smallest domain is selected (also known as first-fail principle)
• FirstFailConstrained :: LabelingOption : The leftmost variable with the smallest domain and the most constraints on it is selected.
• Min :: LabelingOption : The leftmost variable with the smalled lower bound is selected.
• Max :: LabelingOption : The leftmost variable with the greatest upper bound is selected.
• Step :: LabelingOption : Make a binary choice between codex=#b/code and codex/=#b/code for the selected variable codex/code where codeb/code is the lower or upper bound of codex/code (default).
• Enum :: LabelingOption : Make a multiple choice for the selected variable for all the values in its domain.
• Bisect :: LabelingOption : Make a binary choice between codex&lt;=#m/code and codex&gt;#m/code for the selected variable codex/code where codem/code is the midpoint of the domain codex/code (also known as domain splitting).
• Up :: LabelingOption : The domain is explored for instantiation in ascending order (default).
• Down :: LabelingOption : The domain is explored for instantiation in descending order.
• All :: LabelingOption : Enumerate all solutions by backtracking (default).
• Minimize :: Int -> LabelingOption : Find a solution that minimizes the domain variable v (using a branch-and-bound algorithm).
• Maximize :: Int -> LabelingOption : Find a solution that maximizes the domain variable v (using a branch-and-bound algorithm).
• Assumptions :: Int -> LabelingOption : The variable x is unified with the number of choices made by the selected enumeration strategy when a solution is found.
• RandomVariable :: Int -> LabelingOption : Select a random variable for instantiation where x is a seed value for the random numbers (only supported by SWI-Prolog).
• RandomValue :: Int -> LabelingOption : Label variables with random integer values where x is a seed value for the random numbers (only supported by SWI-Prolog).

Exported operations:

 domain :: [Int] -> Int -> Int -> Bool    Constraint to specify the domain of all finite domain variables. Example call: (domain xs min max) Parameters: xs : list of finite domain variables min : minimum value for all variables in xs max : maximum value for all variables in xs
 (+#) :: Int -> Int -> Int    Addition of FD variables. Further infos: defined as left-associative infix operator with precedence 6
 (-#) :: Int -> Int -> Int    Subtraction of FD variables. Further infos: defined as left-associative infix operator with precedence 6
 (*#) :: Int -> Int -> Int    Multiplication of FD variables. Further infos: defined as left-associative infix operator with precedence 7
 (=#) :: Int -> Int -> Bool    Equality of FD variables. Further infos: defined as non-associative infix operator with precedence 4
 (/=#) :: Int -> Int -> Bool    Disequality of FD variables. Further infos: defined as non-associative infix operator with precedence 4
 (<#) :: Int -> Int -> Bool    "Less than" constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4
 (<=#) :: Int -> Int -> Bool    "Less than or equal" constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4
 (>#) :: Int -> Int -> Bool    "Greater than" constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4
 (>=#) :: Int -> Int -> Bool    "Greater than or equal" constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4
 (#=#) :: Int -> Int -> Constraint    Reifyable equality constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4 solution complete, i.e., able to compute all solutions
 (#/=#) :: Int -> Int -> Constraint    Reifyable inequality constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4 solution complete, i.e., able to compute all solutions
 (#<#) :: Int -> Int -> Constraint    Reifyable "less than" constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4 solution complete, i.e., able to compute all solutions
 (#<=#) :: Int -> Int -> Constraint    Reifyable "less than or equal" constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4 solution complete, i.e., able to compute all solutions
 (#>#) :: Int -> Int -> Constraint    Reifyable "greater than" constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4 solution complete, i.e., able to compute all solutions
 (#>=#) :: Int -> Int -> Constraint    Reifyable "greater than or equal" constraint on FD variables. Further infos: defined as non-associative infix operator with precedence 4 solution complete, i.e., able to compute all solutions
 neg :: Constraint -> Constraint    The resulting constraint is satisfied if both argument constraints are satisfied. Further infos: solution complete, i.e., able to compute all solutions
 (#/\#) :: Constraint -> Constraint -> Constraint    The resulting constraint is satisfied if both argument constraints are satisfied. Further infos: defined as right-associative infix operator with precedence 3 solution complete, i.e., able to compute all solutions
 (#\/#) :: Constraint -> Constraint -> Constraint    The resulting constraint is satisfied if both argument constraints are satisfied. Further infos: defined as right-associative infix operator with precedence 2 solution complete, i.e., able to compute all solutions
 (#=>#) :: Constraint -> Constraint -> Constraint    The resulting constraint is satisfied if the first argument constraint do not hold or both argument constraints are satisfied. Further infos: defined as right-associative infix operator with precedence 1 solution complete, i.e., able to compute all solutions
 (#<=>#) :: Constraint -> Constraint -> Constraint    The resulting constraint is satisfied if both argument constraint are either satisfied and do not hold. Further infos: defined as right-associative infix operator with precedence 1 solution complete, i.e., able to compute all solutions
 solve :: Constraint -> Bool    Solves a reified constraint.
 sum :: [Int] -> (Int -> Int -> Bool) -> Int -> Bool    Relates the sum of FD variables with some integer of FD variable.
 scalarProduct :: [Int] -> [Int] -> (Int -> Int -> Bool) -> Int -> Bool    (scalarProduct cs vs relop v) is satisfied if ((cs*vs) relop v) is satisfied. The first argument must be a list of integers. The other arguments are as in sum.
 count :: Int -> [Int] -> (Int -> Int -> Bool) -> Int -> Bool    (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 codesum/code.
 allDifferent :: [Int] -> Bool    "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.
 all_different :: [Int] -> Bool    For backward compatibility. Use codeallDifferent/code.
 indomain :: Int -> Bool    Instantiate a single FD variable to its values in the specified domain.
 labeling :: [LabelingOption] -> [Int] -> Bool    Instantiate FD variables to their values in the specified domain. Example call: (labeling options xs) Parameters: options : list of option to control the instantiation of FD variables xs : list of FD variables that are non-deterministically instantiated to their possible values.