library(ic)

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).

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}

        ?- X #:: 0..5.
        X = X{0..5}

        ?- X #:: [0..3,5,8..9].
        X = X{[0..3,5,8,9]}

        ?- B #:: 0..1.
        B = B{0..1}

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})

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 (integer or real, depending on the context).

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.

floor(Expr)

Expr rounded down to nearest integer.

ceiling(Expr)

Expr rounded up to nearest integer.

truncate(Expr)

Expr rounded to nearest integer toward zero.

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

Integer division, rounding towards zero. This is only defined over integral arguments and yields an integral result.

Expr1 rem Expr2

Remainder corresponding to integer division //. This is only defined over integral arguments and yields an integral result.

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.)

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 conjunctione, 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.

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

    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

   ?- 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

        ?- 0 #= (X#<4).
        X = X{4..1.0Inf}

        ?- B1 #= (X #=< 5), B2 #= (X #>=8), B1 or B2.

        ?- (X #=< 5) or (X #>=8).

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.
   

   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

• Author: Warwick Harvey, Andrew Sadler, Andrew Cheadle

See Also