- ?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.
- ?BoolExprX <=> ?BoolExprY
- BoolExprX and BoolExprY are equivalent.
- <=>(?BoolExprX, ?BoolExprY, ?Bool)
- Bool is the truth value of the equivalence BoolExprX <=> BoolExprY being true.
- 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.
- reexport msg / 3 from ic_kernel
- reexport struct(ic(_, _, _, _, _, _, _, _)) from ic_kernel
- reexport ic_constraints
- reexport ic_search
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.
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,
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
123
0.1
0.1__0.2
pi, e
inf
+Expr
-Expr
+-Expr
abs(Expr)
floor(Expr)
ceiling(Expr)
truncate(Expr)
Expr1+Expr2
Expr1-Expr2
Expr1*Expr2
Expr1/Expr2
Expr1//Expr2
Expr1 rem Expr2
Expr1^Expr2
min(Expr1,Expr2)
max(Expr1,Expr2)
sqr(Expr)
sqrt(Expr)
exp(Expr)
ln(Expr)
sin(Expr)
cos(Expr)
atan(Expr)
sum(Vector)
sum(Vector1*Vector2)
min(Vector)
max(Vector)
BoolExpr1 and BoolExpr2
X>3 and Y<8
. Result is 0 or 1.
BoolExpr1 or BoolExpr2
X>3 or Y<8
. Result is 0 or 1.
BoolExpr1 => BoolExpr2
X>3 => Y<8
. Result is 0 or 1.
BoolExpr1 <=> BoolExpr2
X>3 <=> Y<8
. Result is 0 or 1.
neg BoolExpr
neg X>3
. Result is 0 or 1.
$=, $\=, $>, $>=, $<, $=<, #=, #\=, #>, #>=, #<, #=<
foo(Arg1, Arg2 ... ArgN), module:foo(Arg1, Arg2 ... ArgN)
eval(Var)
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 + Ybut 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 productHowever, 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}
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 = 1By setting the boolean to 0, the negation of the constraint can be enforced:
?- 0 #= (X#<4). X = X{4..1.0Inf}This increases modelling expressiveness, as it allows combining basic constraints via arbitrary boolean connectives (and, or, neg, =>, <=>). For example, disjunction can be expressed as
?- B1 #= (X #=< 5), B2 #= (X #>=8), B1 or B2.or, with the booleans hidden, directly as
?- (X #=< 5) or (X #>=8).
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.
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.
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).
:- 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).