[ Reference Manual | Alphabetic Index ]

library(ic)

Hybrid integer/real interval arithmetic constraint solver   [more]

Predicates

?Vars #:: ++Domain
Constrain Vars to be integral and have the domain Domain.
#::(?Var, ++Domain, ?Bool)
Reflect into Bool the truth of Var having the domain Domain.
?ExprX #< ?ExprY
ExprX is less than ExprY (with integrality constraints).
#<(?ExprX, ?ExprY, ?Bool)
Reified ExprX is less than ExprY (with integrality constraints).
?ExprX #= ?ExprY
ExprX is equal to ExprY (with integrality constraints).
#=(?ExprX, ?ExprY, ?Bool)
Reified ExprX is equal to ExprY (with integrality constraints).
?ExprX #=< ?ExprY
ExprX is less than or equal to ExprY (with integrality constraints).
#=<(?ExprX, ?ExprY, ?Bool)
Reified ExprX is less than or equal to ExprY (with integrality constraints).
?ExprX #> ?ExprY
ExprX is strictly greater than ExprY (with integrality constraints).
#>(?ExprX, ?ExprY, ?Bool)
Reified ExprX is strictly greater than ExprY (with integrality constraints).
?ExprX #>= ?ExprY
ExprX is greater than or equal to ExprY (with integrality constraints).
#>=(?ExprX, ?ExprY, ?Bool)
Reified ExprX is greater than or equal to ExprY (with integrality constraints).
?ExprX #\= ?ExprY
ExprX is not equal to ExprY (with integrality constraints).
#\=(?ExprX, ?ExprY, ?Bool)
Reified ExprX is not equal to ExprY (with integrality constraints).
?Vars $:: ++Lo..++Hi
Constrain Vars to only take real values in the given Domain.
$::(?Var, ++Lo..++Hi, ?Bool)
Reflect into Bool the truth of Var having the domain Domain. Does not impose integrality.
?ExprX $< ?ExprY
ExprX is strictly less than ExprY.
$<(?ExprX, ?ExprY, ?Bool)
Reified ExprX is strictly less than ExprY.
?ExprX $= ?ExprY
ExprX is equal to ExprY.
$=(?ExprX, ?ExprY, ?Bool)
Reified ExprX is equal to ExprY.
?ExprX $=< ?ExprY
ExprX is less than or equal to ExprY.
$=<(?ExprX, ?ExprY, ?Bool)
Reified ExprX is less than or equal to ExprY.
?ExprX $> ?ExprY
ExprX is strictly greater than ExprY.
$>(?ExprX, ?ExprY, ?Bool)
Reified ExprX is strictly greater than ExprY.
?ExprX $>= ?ExprY
ExprX is greater than or equal to ExprY.
$>=(?ExprX, ?ExprY, ?Bool)
Reified ExprX is greater than or equal to ExprY.
?ExprX $\= ?ExprY
ExprX is not equal to ExprY.
$\=(?ExprX, ?ExprY, ?Bool)
Reified ExprX is not equal to ExprY.
?Vars :: ++Domain
Constrain Vars to have the domain Domain.
::(?Var, ++Domain, ?Bool)
Reflect into Bool the truth of Var having the domain Domain.
ic:(?ExprX < ?ExprY)
ExprX is strictly less than ExprY.
ic:(?ExprX =:= ?ExprY)
ExprX is equal to ExprY.
ic:(?ExprX =< ?ExprY)
ExprX is less than or equal to ExprY.
?BoolExprX => ?BoolExprY
BoolExprX being true implies BoolExprY must be true.
=>(?BoolExprX, ?BoolExprY, ?Bool)
Bool is the truth value of BoolExprX => BoolExprY being true.
ic:(?ExprX =\= ?ExprY)
ExprX is not equal to ExprY.
ic:(?ExprX > ?ExprY)
ExprX is strictly greater than ExprY.
ic:(?ExprX >= ?ExprY)
ExprX is greater than or equal to ExprY.
ac_eq(?X, ?Y, ++C)
Arc-consistent implementation of X #= Y + C.
alldifferent(+Vars)
Constrains all elements of a list to be pairwise different.
alldifferent_cst(+Vars, ++Offsets)
The values of each element plus corresponding offset are pair-wise different.
?BoolExprX and ?BoolExprY
BoolExprX and BoolExprY must both be true.
and(?BoolExprX, ?BoolExprY, ?Bool)
Bool is the truth value of BoolExprX and BoolExprY being true.
circuit(+Successors)
The vector Successors describes a Hamiltonain circuit
delayed_goals_number(?Var, -Number)
Returns the number of goals delayed on the ic attribute of Var.
delete(-X, +List, -R, ++Arg, ++Select)
Choose a domain variable from a list according to selection criterion.
element(?Index, +Values, ?Element)
Element is the Index'th element of the collection Values.
get_bounds(?Var, -Lo, -Hi)
Retrieve the current bounds of Var.
get_delta(?Var, -Width)
Returns the width of the interval of Var.
get_domain(?Var, -Domain)
Returns a ground representation of the current IC domain of a variable.
get_domain_as_list(?Var, -DomainList)
List of all the elements in the IC domain of Var
get_domain_size(?Var, -Size)
Size is the number of integer elements in the IC domain for Var
get_finite_integer_bounds(?Var, -Lo, -Hi)
Retrieve the current (finite, integral) bounds of Var.
get_float_bounds(?Var, -Lo, -Hi)
Retrieve the current bounds of Var as floats.
get_integer_bounds(?Var, -Lo, -Hi)
Retrieve the current bounds of (integral) Var.
get_max(?Var, -Hi)
Retrieve the current upper bound of Var.
get_median(?Var, -Median)
Returns the median of the interval of the IC variable Var.
get_min(?Var, -Lo)
Retrieve the current lower bound of Var.
get_solver_type(?Var, -Type)
Retrieve the type of a variable.
get_threshold(-Threshold)
Returns the current propagation threshold.
indomain(?Var)
Instantiates an integer IC variable to an element of its domain.
indomain(?Var, ++Method)
a flexible way to assign values to finite domain variables
integers(?Vars)
Vars' domain is the integer numbers.
is_exact_solver_var(?Term)
Succeeds iff Term is an IC integer variable.
is_in_domain(++Val, ?Var)
Succeeds iff Val is in the domain of Var
is_in_domain(++Val, ?Var, -Result)
Binds Result to indicate presence of Val in domain of Var
is_solver_type(?Term)
Succeeds iff Term is an IC variable or a number.
is_solver_var(?Term)
Succeeds iff Term is an IC variable.
labeling(+Vars)
Instantiates all variables in a collection to elements of their domains.
locate(+Vars, ++Precision)
Locate solution intervals for Vars by splitting and search.
locate(+Vars, ++Precision, ++LinLog)
Locate solution intervals for Vars by splitting and search.
locate(+LocateVars, +SquashVars, ++Precision, ++LinLog)
Locate solution intervals for LocateVars, interleaving search with squashing.
max(+Vars, ?Max)
Constrains Max to be the largest element in Vars.
maxlist(+Vars, ?Max)
Constrains Max to be the largest element in Vars.
min(+Vars, ?Min)
Constrains Min to be the smallest element in Vars.
minlist(+Vars, ?Min)
Constrains Min to be the smallest element in Vars.
neg ?BoolExpr
BoolExpr is 0 (disentailed).
neg(?BoolExpr, ?Bool)
Bool is the logical negation of BoolExpr.
nth_value(+Domain, ++N, -Value)
return the nth value in a domain
?BoolExprX or ?BoolExprY
At least one of the constraints BoolExprX or BoolExprY must be true.
or(?BoolExprX, ?BoolExprY, ?Bool)
Bool is the truth value of BoolExprX or BoolExprY being true.
piecewise_linear(?X, ++Points, ?Y)
Relates X and Y according to a piecewise linear function.
print_solver_var(?Var, -Printed)
Returns a representation of the IC variable Var suitable for printing.
reals(?Vars)
Vars' domain is the real numbers.
search(+L, ++Arg, ++Select, +Choice, ++Method, +Option)
A generic search routine for finite domains or IC which implements different partial search methods (complete, credit, lds, bbs, dbs, sbds, gap_sbds, gap_sbdd)
set_threshold(++Threshold)
Sets the propagation threshold.
set_threshold(++Threshold, +WakeVars)
Sets the propagation threshold with recomputation.
squash(+Vars, ++Precision, ++LinLog)
Refine the intervals of Vars by the squashing algorithm.

Reexports

reexport msg / 3 from ic_kernel
reexport struct(ic(_, _, _, _, _, _, _, _)) from ic_kernel
reexport ic_constraints
reexport ic_search

Description

Overview

The IC (Interval Constraint) library is a hybrid integer/real interval arithmetic constraint solver. Its allows modelling problems involving integer variables, continuous (real) variables, or a mixture of those. A variety of linear and nonlinear constraints are supported. Additional global constraints over the same variable domain are provided by separate libraries of the ic_xxx family.

The integer variables and constraints are similar to those available in traditional finite-domain solvers (such as the old `fd' library). Constraints which are not specifically integer constraints can be applied to either real or integer variables (or a mix) seamlessly. Crucially, an integer variable is just a real variable with an additional integrality constraint.

For more information, see the IC section of the Constraint Library Manual or the documentation for the individual IC predicates.

The solver is loaded either interactively by typing lib(ic) at the query prompt, or, more commonly, by having a

        :- lib(ic).
directive at the beginning of a program.

Variables and Domains

The central notion of the solver is the domain variable; this is a variable than is constrained to take only numeric values in a given domain. It is advisable to declare every variable via a domain constraint. For real-valued variables, initial bounds should be given, e.g.

        ?- X $:: 0.0..4.5.
        X = X{0.0..4.5}
Similarly for integer variables, but here a more precise domain may be given in the form of a list of elements or intervals:
        ?- X #:: 0..5.
        X = X{0..5}

        ?- X #:: [0..3,5,8..9].
        X = X{[0..3,5,8,9]}
Binary (0/1) variables are a special case of integers:
        ?- B #:: 0..1.
        B = B{0..1}
As a general convention, the #-forms of constraints indicate that the constraint imposes integrality, while the $-forms do not. Note how domain variables are printed with their domain in curly brackets (the domain is a part of the variable's attributes).

Collections of variables (such as lists, arrays, matrices) can be given a domain together:

        ?- dim(Xs,[4]), Xs #:: 0..5.
        Xs = [](_432{0..5}, _446{0..5}, _460{0..5}, _474{0..5})
If no a-priori bounds are known, use infinity (written as 1.0Inf or inf), or use the pure type-constraints reals/1 or integers/1. Often, when the variables get implicitly bounded by the other constraints they occur in, domain constraints can be omitted altogether,

Basic arithmetic constraints

The basic arithmetic constraints are equalities ($=), inequalities ($<, $=<, $>=, $>) and disequalities ($\=). These all have #-forms (#=, #<, #=<, #>=, #>, #\=) that require all variables, constants and intermediate result to be integral.

The following arithmetic expressions can be used in these constraints:

X
Variables. If X is not yet an interval variable, it is turned into one.
123
Integer constants.
0.1
Floating point constants ($-constraints only). These are assumed to be exact and are converted to zero-width bounded reals.
0.1__0.2
Bounded real constants ($-constraints only), representing a value that is not exactly known, or not exactly representable.
pi, e
Intervals enclosing the constants pi and e respectively.
inf
Floating point infinity.
+Expr
Identity.
-Expr
Sign change.
+-Expr
Expr or -Expr (the inverse of the abs-function).
abs(Expr)
The absolute value of Expr.
Expr1+Expr2
Addition.
Expr1-Expr2
Subtraction.
Expr1*Expr2
Multiplication.
Expr1/Expr2
Division. Inside #-constraints, this only has a solution if the result is integral.
Expr1^Expr2
Exponentiation.
min(Expr1,Expr2)
Minimum.
max(Expr1,Expr2)
Maximum.
sqr(Expr)
Square. Logically equivalent to Expr*Expr, but with better operational behaviour.
sqrt(Expr)
Square root (always positive).
exp(Expr)
Same as e^Expr.
ln(Expr)
Natural logarithm, the reverse of the exp function.
sin(Expr)
Sine.
cos(Expr)
Cosine.
atan(Expr)
Arcus tangens. (Returns value between -pi/2 and pi/2.)
rsqr(Expr)
Reverse of the sqr function. The same as +-sqrt(Expr).
rpow(Expr1,Expr2)
Reverse of exponentiation. i.e. finds X in Expr1 = X^Expr2.
sub(Expr)
A subinterval of Expr.
sum(Vector)
Sum of the vector elements. The vector can be a list, array or any of the vector expressions supported by eval_to_list/2.
sum(Vector1*Vector2)
Scalar product: The sum of the products of the corresponding elements in the two vectors. The vectors can be lists, arrays or any of the vector expressions supported by eval_to_list/2. If the vectors are of different length, the shorter one is padded with trailing zeros.
min(Vector)
Minimum of the vector elements. The vector can be a list, array or any of the vector expressions supported by eval_to_list/2.
max(Vector)
Maximum of the vector elements. The vector can be a list, array or any of the vector expressions supported by eval_to_list/2.
BoolExpr1 and BoolExpr2
Boolean conjunction. e.g. X>3 and Y<8. Result is 0 or 1.
BoolExpr1 or BoolExpr2
Boolean disjunction. e.g. X>3 or Y<8.Result is 0 or 1.
BoolExpr1 => BoolExpr2
Boolean implication. e.g. X>3 => Y<8. Result is 0 or 1.
neg BoolExpr
Boolean negation. e.g. neg X>3. Result is 0 or 1.
$=, $\=, $>, $>=, $<, $=<, #=, #\=, #>, #>=, #<, #=<
Embedded constraints whose value is their reified truth value (0..1).
foo(Arg1, Arg2 ... ArgN), module:foo(Arg1, Arg2 ... ArgN)
Call user-defined constraint/function foo.
eval(Var)
where Var will be one of the above expression at run-time.

Linear expressions are very common in constraint modelling and are specially handled by the solver. They can be written either with explicit additions and multiplications, such as in the cryptarithmetic example below:

                     1000*S + 100*E + 10*N + D
                   + 1000*M + 100*O + 10*R + E
        #= 10000*M + 1000*O + 100*N + 10*E + Y
but are often written using scalar product notation, as in this subset-sum problem:
    model(Amounts) :-
        Total = 1505,
        Prices = [215, 275, 335, 355, 420, 580],
        length(Prices, N),
        length(Amounts, N),
        Amounts #:: 0..Total//min(Prices),
        sum(Amounts*Prices) #= Total.           % scalar product
However, this library is not limited to linear constraints, so it can be used to solve general problems like:
   ?- ln(X) $>= sin(X).
   X = X{0.36787944117144228 .. 1.0Inf}
   

Reified Constraints

All the basic constraints have reified versions. This means they can not only be used as normal constraints, but they can occur in arithmetic or logical expressions, where they represent their truth value in the form of a 0 or 1. For example:

        ?- X #:: 1..3,  B #= (X#<4).
        X = X{1..3}
        B = 1
By setting the boolean to 0, the negation of the constraint can be enforced:
        ?- 0 #= (X#<4).
        X = X{4..1.0Inf}
The feature is especially useful for modelling logical connectives such as disjunction, which are otherwise difficult to handle, e.g.
        ?- (X #=< 5) or (X #>=8), X=7.
        No (0.00s cpu)

Other Constraints

The basic IC library implements only a few other constraints, such as element/3 (a constraint version of indexed array access), circuit/1, piecewise_linear/3, and a basic form of alldifferent/1. Most more complex constraints are provided in separate libraries, such as ic_global and ic_global_gac.

The library ic_kernel contains low-level primitives useful for implementing user-defined constraints.

Search

Once a problem has been modelled with domain variables and constraints, it can be solved by search. This means looking for variable assignments that satisfy the constraints, usually by non-deterministically exploring the different domain values that the variables can take. The library provides labeling/1 and search/6 for integer variables, and locate/4 for real variables, among others.

For the implementation of custom search routines, the get_xxx predicates provide access to information about variable domains.

Implementation details and Pitfalls

User-defined functions/constraints are treated in a similar manner to user defined functions found in expressions handled by is/2. Note, however, that user defined constraints/functions, when used in IC, should be (semi-)deterministic. User defined constraints/functions which leave choice points may not behave as expected.

Linear constraints are handled by a single propagator, whereas non-linear constraints are broken down into simpler ternary/binary/unary propagators. The value of any constraint found in an expression is its reified truth value (0..1).

Variables appearing in arithmetic IC constraints at compile-time are assumed to be IC variables unless they are wrapped in an eval/1 term. The eval/1 wrapper inside arithmetic constraints is used to indicate that a variable will be bound to an expression at run-time. This feature will only be used by programs which generate their constraints dynamically at run-time, for example.

   broken_sum(Xs,Sum):-
       (
	   foreach(X,Xs),
	   fromto(Expr,S1,S2,0)
       do
	   S1 = X + S2
       ),
       Sum $= Expr.
   
The above implementation of a summation constraint will not work as intended because the variable Expr will be treated like an IC variable when it is in fact the term +(X1,+(X2,+(...))) which is constructed in the for-loop. In order to get the desired functionality, one must wrap the variable Expr in an eval/1.
   working_sum(Xs,Sum):-
       (
	   foreach(X,Xs),
	   fromto(Expr,S1,S2,0)
       do
	   S1 = X + S2
       ),
       Sum $= eval(Expr).
   

Examples

:- lib(ic).


% A famous cryptarithmetic puzzle

sendmore(Digits) :-
        Digits = [S,E,N,D,M,O,R,Y],
        Digits :: [0..9],

        alldifferent(Digits),
        S #\= 0,
        M #\= 0,
                     1000*S + 100*E + 10*N + D
                   + 1000*M + 100*O + 10*R + E
        #= 10000*M + 1000*O + 100*N + 10*E + Y,

        labeling(Digits).


% Sudoku puzzle

sudoku(Board) :-
        dim(Board, [N,N]),
        Board :: 1..N,

        ( for(I,1,N), param(Board) do
            alldifferent(Board[I,*]),
            alldifferent(Board[*,I])
        ),
        NN is integer(sqrt(N)),
        ( multifor([I,J],1,N,NN), param(Board,NN) do
            alldifferent(concat(Board[I..I+NN-1, J..J+NN-1]))
        ),

        labeling(Board).


% N-queens problem

queens_arrays(N, Board) :-
        dim(Board, [N]),
        Board #:: 1..N,

        ( for(I,1,N), param(Board,N) do
            ( for(J,I+1,N), param(Board,I) do
                Board[I] #\= Board[J],
                Board[I] #\= Board[J]+J-I,
                Board[I] #\= Board[J]+I-J
            )
        ),

        labeling(Board).


% Fractions puzzle - a problem with a non-integer constraint.
% Find 9 distinct non-zero digits that satisfy:
%       A    D    G
%       -- + -- + -- == 1
%       BC   EF   HI

fractions(Digits) :-
        Digits = [A,B,C,D,E,F,G,H,I],
        Digits #:: 1..9,
 
        A/(10*B+C) + D/(10*E+F) + G/(10*H+I) $= 1,
        alldifferent(Digits),

        labeling(Digits).

About

See Also

library(ic_global), library(ic_global_gac), library(branch_and_bound), library(propia)
Generated from ic.eci on 2020-02-26 22:26