ridgeworks
commented
1 year ago {X>Y, Y>X} is an obvious inconsistent constraint so the question is can CLP(BNR) prove it. I think it can but there are some caveats.
The first point is that > (as well as < and <>) is mathematically unsound over reals in CLP(BNR). As an example:
?- {X>1}.
X::real(1.0000000000000002, 1.0Inf).This is incorrect because there are solutions between 1 and 1.0000000000000002 that have been omitted in the answer. (The basic reason is that there's no finite numeric representation for a number greater than 1 that has no real values between itself and 1. ) However, < (and the others) is sound over integers:
?- X::integer(-inf,inf),{X>1}.
X::integer(2, 1.0Inf).However, over a large finite set of integers:
?- [X,Y]::integer,{X>Y, Y>X}.
X::integer(-72057594037925648, 72057594037925646),
Y::integer(-72057594037925648, 72057594037925645).which still isn't the expected result. But if I specify a smaller domain:
?- [X,Y]::integer(-500,500),{X>Y, Y>X}.
false.which, I believe, is the answer you would expect. It arrives at this answer via the fixed point iteration which successively narrows the two intervals by 1 for each iteration until one becomes "empty" causing failure. Although guaranteed to terminate for finite domains, this can take a long time for large domains. So to avoid the appearance of non-termination, CLP(BNR) employs a throttling mechanism to terminate the fixed point iteration before failure or steady state occurs. With the default setting of flag clpBNR_iteration_limit, this happens for this query at integer(-500,500). Larger domains can be accomodated with a larger limit.
FWIW, it works exactly the same way with reals, except the decease in the width of a real interval is only a floating point epsilon for each iteration, so that can take a very long time. And it's still unsound.
solve desn't really help with this fundamental issue, but it does permit handling of larger domains by sub-dividing them into smaller domains that can fail within the throttling limit:
?- [X,Y]::integer(-50000,50000),{X>Y, Y>X}, solve(X).
false.So I believe, in general, the inconsistent set of constraints {X>Y, Y>X} can be proven to be false over finite integer domains. But there is a pragmatic throttling mechanism (user controllable) in place which limits the size of the domains for which this is the case.
There are other examples of constraints which have similar characteristics, e.g., {X == X+1} (which is sound over reals).
Aa couple of final points. As documented in the User Guide, success of a query does not guarantee the existence of a solution; only that if a solution exists it's "contained" in the answer. (Failure does guarantee the absence of a solution.) This is obviously the case when throttling terminates the fixed point iteration, but also generally if any intervals remain in the answer.
And there is no "meta-interpretation" of constraints in CLP(BNR). So the only way of detecting inconsistent constraints is by proving them so via constraint propagation.
Using in Void Linux:
I expected this to fail.