clpBNR: integer division

@ridgeworks, I’ve searched the documentation to find the operator for integer division (and modulo) in constraints, first I supposed // would work, but it doesn’t:


64 ?- [A,B,C]::integer, { A == B // C }.
% Add {_3184{integer(-72057594037927936,72057594037927935)}==_3242{integer(-72057594037927936,72057594037927935)}//_3300{integer(-72057594037927936,72057594037927935)}}
% {} failure due to bad constraint: {_3184{integer(-72057594037927936,72057594037927935)}==_3242{integer(-72057594037927936,72057594037927935)}//_3300{integer(-72057594037927936,72057594037927935)}}
false.

then I searched the documentation, but didn’t find it. Perhaps I am missing something obvious. Thanks for your help!

Interesting question, and no, you didn’t miss anything obvious. There are no integer specific arithmetic operations in clpBNR. All arithmetic is done assuming real values (integers are a subset of reals) and then truncated as needed for integer variables (interval bounds are rounded inwards).

If you want the result of a division to be an integer, use just use / and constrain it as in your example. (Note that B and C don’t necessarily have to be integers.) Do you have a particular application in mind where this wouldn’t be what you want?

The underlying issue is that to implement an interval arithmetic primitive to support a clpBNR constraint, it needs to have a mathematical definition (as in algebra) which includes its inverse so that, for example, {A == B/C} is equivalent to {B == A*C} since multiplication is the mathematical inverse of division. I don’t think // (or mod) has such an inverse.

Yes, what I actually need in this case is the value of the integer division to drive the constraint rather than simply having an integer as a result of B/C.

I found a way to do it like this:

 div_rem(A,B,Div,Rem) :-
   Div::integer(0,_),
   { A >= Div * B },
   global_minimum(A - Div * B, Rem).

It works for positive A and B, which is all I need for now, but it is easy to extend for negative values. The only thing is that it is a little expensive, perhaps there is a faster implementation.

EDIT:

I don’t think global_minium/2 has an inverse either, and yet it applies a constraint to the space of possible solutions; or is it the case that by the word ‘constraint’ you have in mind a more strict definition related to intervals?

There is no floor primitive currently either but that’s an an interesting possibility as a first step.

I’m still not sure how it’s used, but put that aside for now.

global_minimum is very expensive - it’s really a directed search. @j4n_bur53 suggested a floor primitive which looks like it might be doable. Would floor(B/C) meet your requirements? Prototype examples:

?- X::real(-2.5,2.5), {F==floor(X)}.
X::real(-2.5000000000000004, 2.5000000000000004),
F::integer(-3, 2).

?- F::integer(-3,2), {F==floor(X)}.
F::integer(-3, 2),
X::real(-3, 3).

?- {A==floor(B/C)}, B=7, C=2.
A = 3,
B = 7,
C = 2.

?- {A==floor(B/C)}, B=8, C=2.
A = 4,
B = 8,
C = 2.

No, global_minimum is not a constraint; as I said above it’s a directed search for a minimum value of an expression and is built on top of the constraint infrastructure (like solve and enumerate). clpBNR constraints are the expressions using the primitive operations that appear between curly brackets and get “compiled” into the constraint network.

Certainly, this will work. Thank you so much for the prompt reply. Perhaps, for completeness, you can add ceiling(X) along the way, since I suspect it will be similar to floor.

One conceptual question I have, is that floor(X) doesn’t have an algebraic inverse; since you mentioned this was required, I was wondering whether an algebraic inverse is required in some cases and not in others.

I see, thanks for the explanation, this clears it up for me.

So what should be added to clpBNR in the next release? My problem is that I don’t have a use-case to base a decision on. Some possibilities:

  1. Do nothing. Good for me, but you probably wouldn’t be happy. OTOH I could tell you the half-dozen lines of code (in two files) that would allow you to add floor to your custom version.

  2. Add floor as a primitive which enables the user to it in any way he sees fit. Integer divide and modulo would be two examples that could be implemented using floor.

  3. Add // and mod as constraints which use an undocumented floor primitive as suggested by @j4n_bur53 .

  4. = 2.+3. , i.e., make floor, // and mod first class primitives.

I’m generally a minimalist so I’m looking for some context (help me out here) for making a decision. (And ceiling would not be difficult, but it’s even less clear what it would be used for.)

To the extent that floor itself has an algebraic definition, it’s inverse can be somewhat manufactured. Look at the second example. Given the interval of the floor(X) is integer(L,H) what can we say about X? Namely,X::real(L,H+1). That’s sufficiently useful to define a constraint primitive. This approach works if the function is simple enough, as is the case here, but for more general mathematical functions (addition, multiplication, log, power, trig functions, etc.) an algeraic inverse is needed.

Thanks; in terms of libraries I am also a minimalist in general, but as for applications I tend to favor a batteries-included approach. I would argue that floor,ceiling, mod and integer division are all part of a minimalist approach, because:

  1. almost any language that provides mathematical expressions for reals has built-in support for floor,ceiling,mod/rem and integer division. Some are so basic, that even hardware has support for it (e.g. idiv in x86 assembly returns both integer quotient and remainder).
  2. clpfd provides mod,rem,// (floor integer division) and div (truncated integer division). People moving code from clpfd to your library will certainly benefit. I think this in itself is a major use case, because your library beautifully blends and allows using constraints in the boolean, real and integer domains.
  3. I don’t really see any benefit from not including floor/celing/mod/integer division (besides not having to write the initial implementation). I would think they don’t add any major maintenance cost, since they are basic functions whose semantics will not need to change in the future.

I’m having trouble getting my point across, so let me try and tackle it from a different perspective.

The fundamental problem is that integers are not closed under division, i.e., dividing two integers does not always produce an integer result - see Division (mathematics) - Wikipedia. The Wikipedia article offers five alternatives when the result of division is not an integer.

Now the “domain of discourse” for clpfd is the set of integers, including infinity values. This reduces the set of possible alternatives when dividing two integers to 1. (partial function) and 5. (integer division). clpfd made the decision to only support 5. and uses the integer divide operator // rather than the division operator / (and rightly so).

Most programming languages (and computers) also support IEEE floating point arithmetic. This extends the “domain of discourse” to a subset of real numbers (actually rational numbers), and, although floating point arithmetic is notoriously unsound, it’s adequate for most practical purposes. This domain extension to a subset of reals opens up the possibility of alternative 2., i.e., dividing two integers can yield a floating point value as an approximation to the real result. But since, in most cases, they also want 5. as an option, they end up with two integer division operations.

The “domain of discourse” for clpBNR is the entire set of reals, and reals are closed under division - dividing a real by a real always produces a real. This only requires one division operator/function. So a clpBNR integer is not a separate domain with a different set of operators. Instead it’s a constraint on the possible values of a real. The reason why clpBNR " … blends and allows using constraints in the boolean, real and integer domains " is that, in fact, they’re not really separate domains at all; they’re all reals.

So clpBNR currently supports alternatives 1. and 2. depending on how the result is constrained, e.g., [A,B,C]::integer, {A==B/C} corresponds to option 1. and [B,C]::integer, {A==B/C} corresponds to option 2. (or 3. under most circumstances).

The question I would like to answer is, given the above, whether there is a need to support 5. and why? Do we have any examples of real problems to which clpBNR can be applied and can only be done with 5. ? I need an explanation for two divide operations in clpBNR beyond “lots/most of other arithmetic systems have it”. I see no point in adding “features” that nobody is going to use.

And these are the people I’d like to hear from, surely they have relevant examples. (On the other hand, I’m not sure why anyone would port a working clpfd program to clpBNR, so that would be a useful discussion as well.)

Note that I’m not questioning the usefulness of integer division in general, just in a clpBNR context. It’s not hard to think of useful examples using standard functional arithmetic; converting numeric values to strings comes to mind. But why would I use clpBNR for that?

And I’m not questioning it on the basis of any practical implementation/maintenance considerations. I’d be all over it if I could figure out a good reason for doing it, because then I could explain it.

1 Like

This is a great explanation, certainly gives me a much clearer idea about clpBNR. Thanks!

To make it simple, suppose you have a problem where you need the largest integer A, such that A can’t be higher than B/C (e.g it is a limited resource limited by parameters B,C), A::integer(0,_), [B,C]::real(0,_); A needs to be as close as possible to {B/C}. A,B and C are constrained by the rest of the program in some way. As far as I can see (perhaps I am wrong) neither 1 or 2 will help to solve this. Only option 5 will. Am I mistaken in thinking this?

Of course you can implement it with global_minimum/2 like I did in my example above, but that seems to me a waste of resources if you can have floor(X). (note: because of the application domain, we know that a solution exists such that {A==B//C} ).

So isn’t that the constraint {A<B/C} or {A=<B/C}? After applying any other constraints, the highest possible value of A is its upper bound (if it hasn’t already narrowed to a point value). Maybe I’m missing something?

Ahh, this is what I was missing. I was thinking of obtaining solutions using enumerate/2 or solve/2. It didn’t cross my mind the fact that the solution was already present in the upper bound and that I could use upper_bound/1 to get the solution.

As I understand it now, thanks to your reply, if I have the following:

20 ?- [B,C]::real(0,_), [A]::integer(0,_), {A=<B/C}. %plus some other constraints

the upper bound of A is guaranteed to be the result of the integer division of B/C, if B and C can be narrowed to a point value, and if a solution exists (thinking now only of positive values). Am I correct?

Almost. To be precise, if B and C narrow enough such that the interval B/C only contains one integer value, A will be the result of the integer division of B/C (assuming positive `B’ and ‘C’).

Aside: If B or C have floating point bounds, they won’t ever narrow to points due to conservative arithmetic rounding. (You can force them to be points by unifying them with a numeric value as long as the value doesn’t end up violating any other constraints.)

You may still have to run some variant of solve at some point on some subset of the intervals if the local constraint propagation results in insufficient narrowing to unify A with a point value. But that all depends on the rest of the problem details.

hmmm…are there any guarantees for the upper bound of A in other cases? or is it the case that the only guarantee is when B and C are narrow enough to include only one integer?

More specifically, could it ever be the case that the upper bound of A, let’s call it H, fails to satisfy the constraint{H=<B/C} (assuming a solution exists)?

Constraints are always active. Once you add the constraint {A=<B/C} the upper bound of A will always be =< the lower bound of B/C.

But I was wrong when I said that A would narrow to a point; in fact, the lower bound of A is unaffected by changes in B and C.

Try it, e.g.,

?- A::integer(0,_),[B,C]::real(0,_),{A=<B/C}.
A::integer(0, 72057594037927935),
B::real(0, 1.0e+16),
C::real(0, 1.0e+16).

?- A::integer(0,_),[B,C]::real(0,_),{A=<B/C}, {B=<100, C>=10}.
A::integer(0, 10),
B::real(0, 100),
C::real(10, 1.0e+16).

?- A::integer(0,_),[B,C]::real(0,_),{A=<B/C}, {B=<24.8, C>=12.1}.
A::integer(0, 2),
B::real(0, 24.800000000000004),
C::real(12.099999999999998, 1.0e+16).

?- A::integer(0,_),[B,C]::real(0,_),{A=<B/C}, B=99, C=17.2.
B = 99,
C = 17.2,
A::integer(0, 5).

As the ranges of B and C narrow through the addition of constraints, the upper bound of A decreases. (Intervals can only get narrower.)

Great, I think this solves it for me; appreciate your work and most of all you taking time to help me understand better.

And thanks for the discussion and taking interest. It’s always educational when someone new gets involved.

I am still open to adding additional constraint ops (like the integer operations that triggered all this) given a few motivational examples.