clpBNR: B or B

[swi]

@ridgeworks

leap/1 can now be implemented as:

leap2(Y) :-
   Y::integer(1583,_),
   [Q4,Q100,Q400]::real(0,_),
   { Y == Q4*4,
     Y == Q100*100,
     Y == Q400*400,
     isint(Q4),                       % Y must be multiple of 4
     (isint(Q100) -> isint(Q400))     % if Y is a multiple of 100, Y must be  a multiple of 400
   }.

This is very nice and clean, I also like the use of an implication to capture the whole logic in a simple way.

@ridgeworks

While isint probably has more uses than this one, I’m not overly happy about adding new primitives piecemeal to address issues like this.

Although isint was added to solve this particular case, I think it fills a major gap that used to exist in clpBNR. Before, you could only specify integer constraints for variables by declaring them with ::integer. It was very difficult to specify an integer constraint for an expression. So you had to do tricks like what I did in my first attempt, or somehow play with a mixture of boolean expressions and other constraints. This would lead to having extra helper variables that needed to be narrowed to find a solution, and in some cases (like leap/1) it would make the system unusable.

Of course, it would be great to have failed reified constraints to become 0 or false, but even if we had that, I think isint would be needed to efficiently solve a subset of problems (all those types of problems for which a set of real equations mostly expresses the solution, but intermediate variables need to be constrained to an integer in order to further apply some of the remaining equations; this is common in real physical systems which impose integer constraints on some of the values).

So all things considered, I think isint is a worthy addition to clpBNR and expands the usability surface of the library even though its need was found because of leap/1.

By the way, I didn’t see isint in the master branch, is it in some other branch?

[ridgeworks]

@swi

So all things considered, I think isint is a worthy addition to clpBNR and expands the usability surface of the library even though its need was found because of leap/1.

OK, I’ll add a primitive providing this functionality to the next release. Still have a couple of issues to think about, e.g., it should probably narrow any interval argument if possible. And I think I should probably change the name from isint to just plain integer.

@swi

By the way, I didn’t see isint in the master branch, is it in some other branch?

Only my local branch. I use github to capture releases and I still consider this a work in progress. Also have to update documentation, but I won’t undertake any more significant changes before I commit the next release (0.10.2).

[swi]

@ridgeworks

OK, I’ll add a primitive providing this functionality to the next release. Still have a couple of issues to think about, e.g., it should probably narrow any interval argument if possible. And I think I should probably change the name from isint to just plain integer.

Those two make sense to me, certainly I would expect it to narrow the interval, and I think naming it integer is much better. Thank you so much for your work on this!

Just a side note: once I heard O’Keeffe say that he built prolog programs several times (forgot if it was two or three times), the first one was throw away, to better understand the problem; then he re-wrote it from scratch, and kept only the final version. This just came to my mind since you mentioned you had to start from scratch to solve the reified boolean issue. It’s not a hint , just sharing something I thought was quite interesting from someone like O’Keeffe.

[ridgeworks]

I’ve pushed a new version (v0.10.2) to github with main feature addition being integer/1 as a constraint. In testing, I arrived at this even simpler version of leap/1.

leap(Y) :-
   Y::integer(1583,_),
   { integer(Y/4),                        % Y is evenly divisible by 4
     (integer(Y/100) -> integer(Y/400))   % if Y is evenly divisible by  100, Y must be evenly divisible by  400
   }.

with test:

?- leap(Y), member(Y,[1583,1584,1585,1586,1587,1588,1600,1700,1800,1900,2000,2100]).
Y = 1584 ;
Y = 1588 ;
Y = 1600 ;
Y = 2000 ;
false.

A “corollary” test:

not_leap(Y) :-
   Y::integer,
	{ (Y < 1583) or
	  ~integer(Y/4) or
	  (integer(Y/100) and ~integer(Y/400))
	}.

ao:

?- not_leap(Y),member(Y,[1583,1584,1585,1586,1587,1588,1600,1700,1800,1900,2000,2100]).
Y = 1583 ;
Y = 1585 ;
Y = 1586 ;
Y = 1587 ;
Y = 1700 ;
Y = 1800 ;
Y = 1900 ;
Y = 2100.

I think integer/1 is a useful addition requiring minimal effort - thanks for bringing the issue to my attention.

@swi

Just a side note: once I heard O’Keeffe say that he built prolog programs several times (forgot if it was two or three times), the first one was throw away, to better understand the problem; then he re-wrote it from scratch, and kept only the final version.

I feel like I’ve already gone through this process several times - the first few versions (before 0.3) didn’t make even it to github. But nothing’s perfect - evolution and, occasionally, revolution, continue. It’s just that my pain threshold and the payback aren’t what they used to be.

[swi]

@ridgeworks

leap(Y) :-
   Y::integer(1583,_),
   { integer(Y/4),                        % Y is evenly divisible by 4
     (integer(Y/100) -> integer(Y/400))   % if Y is evenly divisible by  100, Y must be evenly divisible by  400
   }.

This is much, much better and couldn’t be cleaner and clearer. It didn’t occur to me that an integer constraint would solve this so cleanly. Thanks for thinking of this. I am sure integer has many more unsuspected uses.

@ridgeworks

not_leap(Y) :-
   Y::integer,
	{ (Y < 1583) or
	  ~integer(Y/4) or
	  (integer(Y/100) and ~integer(Y/400))
	}.

Nice to see you can just apply boolean logic easily with integer.

By the way, years before 1583 were leap if they were divisible by 4 (the further rule of integer(Y/100) -> integer(Y/400) was added in 1582 to come closer to the true solar year. Interesting fact is that Thursday 4 October 1582 was followed by Friday 15 October 1582.

@ridgeworks

It’s just that my pain threshold and the payback aren’t what they used to be.

I do appreciate your effort, and I am very grateful that you made clpBNR available!

[swi]

Why does the following not produce a solution?

2 ?- I::real(1,10), { ~integer(I/4) }, solve(I).
I::real(1, 10).

EDIT: I think the answer is because there are infinite solutions, and the result simply says that the solutions are in the specified interval which can’t be narrowed. right?

[ridgeworks]

@swi

EDIT: I think the answer is because there are infinite solutions, and the result simply says that the solutions are in the specified interval which can’t be narrowed. right?

Right. solve works by picking a point in the interval and then executing the constraint conjunction {X =< Pt} ; {Pt =< X}. And it does so recursively until it fails, eliminating that sub-interval, or it hits the precision limit to terminate bisection and produces an “answer”. On backtracking the Prolog disjunction permits the search of other branches.

Also solve attempts to pick a bisecting point that isn’t a solution to avoid creating noise by bisecting a valid solution. So it’s meant for use with an interval where solutions are sparse, e.g., finding the roots of a polynomial. In this case it gives up searching for a bisection point fairly quickly.

splitsolve has the reverse problem, it splits anywhere, so you get a ton of solutions when almost every point is a solution, which isn’t useful for the opposite reason.

?- I::real(1,10), { ~integer(I/4) }, splitsolve(I).
I::real(1, 1.000000536441803) ;
I:: 1.000001... ;
I:: 1.000001... ;
I:: 1.000002... ;
I:: 1.000002... ;
I:: 1.000003... ;
I:: 1.000003... ;
I:: 1.000004... ;
I:: 1.000004... .

So you need to have some feel for the problem when picking an appropriate “labelling” predicate. But there’s nothing very special or clever about these general purpose search predicates. For any given problem, it may be desirable to write a custom “solver” tailored to that class of problem.

Also note that the example query, as stated, isn’t of much use for narrowing purposes, because any narrowing must include the value {integer(I/4)} for soundness purposes (for the same reason that < and > are unsound on reals). But it will constrain any answers involving unification, as in:

?- I::real(1,10), { ~integer(I/4) }, I=8.
false.

?- I::real(1,10), { ~integer(I/4) }, I=6.
I = 6.

I think there are some interval arithmetic systems that support both open and closed intervals, (clpBNR supports only closed), but I’ve not seen a compelling argument (or practical application) to justify the added complexity.

[swi]

Thank you for the explanation, it improved my understanding about splitsolve/1 and solve/1 which was somewhat fuzzy before.