Library for finite domain constraint solving.
The general structure of a specification of an FD problem is as follows:
domainconstraint & fdconstraint & labeling
where:
domain_constraint
specifies the possible range of the FD variables (see constraint domain
)
fd_constraint
specifies the constraint to be satisfied by a valid solution
(see constraints #+, #, allDifferent, etc below)
labeling
is a labeling function to search for a concrete solution.
Note: This library is based on the corresponding library of SicstusProlog but does not implement the complete functionality of the SicstusProlog library. However, using the PAKCS interface for external functions, it is relatively easy to provide the complete functionality.
Author: Michael Hanus
Version: June 2012
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. 
A datatype to represent reifyable constraints.
Constructors:
This datatype contains all options to control the instantiated of FD variables
with the enumeration constraint labeling
.
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 firstfail 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 x=#b
and
x/=#b
for the selected variable
x
where b
is the lower or
upper bound of x
(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 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
:: 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 branchandbound algorithm).
Maximize
:: Int > LabelingOption
: Find a solution that maximizes the domain variable v
(using a branchandbound 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 SWIProlog).
RandomValue
:: Int > LabelingOption
: Label variables with random integer values
where x
is a seed value for the random numbers
(only supported by SWIProlog).
Constraint to specify the domain of all finite domain variables.

Addition of FD variables.

Subtraction of FD variables.

Multiplication of FD variables.

Equality of FD variables.

Disequality of FD variables.

"Less than" constraint on FD variables.

"Less than or equal" constraint on FD variables.

"Greater than" constraint on FD variables.

"Greater than or equal" constraint on FD variables.

Reifyable equality constraint on FD variables.

Reifyable inequality constraint on FD variables.

Reifyable "less than" constraint on FD variables.

Reifyable "less than or equal" constraint on FD variables.

Reifyable "greater than" constraint on FD variables.

Reifyable "greater than or equal" constraint on FD variables.

The resulting constraint is satisfied if both argument constraints are satisfied.

The resulting constraint is satisfied if both argument constraints are satisfied.

The resulting constraint is satisfied if both argument constraints are satisfied.

The resulting constraint is satisfied if the first argument constraint do not hold or both argument constraints are satisfied.

The resulting constraint is satisfied if both argument constraint are either satisfied and do not hold.

Solves a reified constraint. 
Relates the sum of FD variables with some integer of FD variable. 
(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 
(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 
"All different" constraint on FD variables.

For backward compatibility. Use 
Instantiate a single FD variable to its values in the specified domain. 
Instantiate FD variables to their values in the specified domain.
