Scryer-prolog: clpz limits?

[notoria]

The following happens:

?- use_module(library(clpz)).
   true.
?- A ^ B #= C, [A, B, C] ins -2..2, labeling([], [A, B, C]).
   C = 1, A = -2, B = 0
;  C = -2, A = -2, B = 1
;  caught: error(type_error(float,-1),(^)/2)
?- [A, B, C] ins inf..sup, A ^ B #= C.
   clpz:(A^B#=C)
;  false.
?- 

The domain of B isn't restricted/reduced to 0..sup.
I also tested:

?- B #> 1, E #>= 0, B ^ E #=< X, X #< B ^ (E + 1), B #= 10, X #= 2^10.
   B = 10, X = 1024, clpz:(E+1#=_A), clpz:(10^_A#=_B), clpz:(10^E#=_J), clpz:(_J in 1..1000), clpz:(_B in 1025..10000), clpz:(_A in 1..4), clpz:(E in 0..3)
;  false.

It doesn't seem like X #< B ^ (E + 1) is being taken into account for clpz:(E in 0..3), it should have been smaller (maybe clpz:(E in 2..3)) but for larger X it doesn't get better.

It would be nice to extend some operators like xor (it may be the only one), so this have a value:

?- 11 #= 2 * X + 1. % This have a value.
   X = 5
;  false.
?- 1 #= X xor 2. % This doesn't have a value.
   clpz:(1#=X xor 2)
;  false.
?- 

[triska]

Thank you for reporting these issues!

I have filed the float issue as #548.

Regarding the propagation of A^B #= C, where we currently get:

?- A^B #= C.
   clpz:(A^B#=C)

Let's consider a specialisation of the query:

?- A^B #= C, A #= 1, B in -2..0, indomain(B).
   C = 1, A = 1, B = -2
;  C = 1, A = 1, B = -1
;  C = 1, A = 1, B = 0
;  false.

If B were restricted to 0..sup even in this specific case, let alone in the more general case, two of these solutions would be incorrectly removed.

Stronger xor propagation would indeed be a very nice feature!

[notoria]

I understand the negative numbers are solutions too. Is it possible to have the following:

?- A ^ B #= C.
   clpz:(A in -1\/1), clpz:(B in inf..sup), clpz:(C in -1\/1)
;  clpz:(A in inf..-2\/0\/2..sup), clpz:(B in 0..sup), clpz:(C in inf..-2\/0\/2..sup)
;  false
?-

And for B #> 1, X #< B ^ (E + 1), is it possible to change the domain of E?

[triska]

From a declarative perspective, that would be possible. However, it would counteract the purpose of constraints: Our goal with CLP is to have all constraints available deterministically, so that labeling/2 can reason about all constraints at once.

If we introduce nondeterminism within constraints, then we again get an exponential search space, for example if we have:

?- A^B #= C, D^E #= F, G^H #=I, ...

then backtracking these out by itself already produces answers that are exponential in the number of posted constraints.

We know from Matiyasevich's theorem that there will always be cases that are not propagated, no matter how much effort we put into it. So, the goal in the implementation is to propagate nicely and efficiently in cases that are needed in practice. I recommend to let these cases be guided by concrete use cases, and show where more propagation would benefit.

Propagation is not free: It costs computation time too. So, we must strike a sensible trade-off between strength and efficiency of propagation. For example, a compelling argument for more propagation would be a case where an unbounded domain becomes finite. If the only benefit is the removal of specific elements, then the implementation cost and complexity must be heavily weighted against the possible benefit.

[notoria]

OK, so for B #> 1, X #< B ^ (E + 1), it isn't possible to change the domain of E? Or the price would be too high. The domain of E could have a lower bound.

It's minus infinity without E #>= 0 but for B #= 2, X #= 2^(2^17) then clpz:(E in 0..39456), so labeling/2 is a bit slow.

Could a nonnegative version of power help with that? Like:

?- pow(B, E, R).
   clpz:(B in 0..sup), clpz:(E in 0..sup), clpz:(R in 0..sup)
;  false
?-

And the lower bound could be computed then?

[triska]

Here is the logic for propagating Z #= X^Y, analyzing the cases and imposing restrictions on the arguments:

https://github.com/mthom/scryer-prolog/blob/fefd262c2e7703e394be9dccf109dbaebd045c0f/src/prolog/lib/clpz.pl#L5187

It is a giant case distinction, taking into account which arguments (if any) are already instantiated, and what is known about their domains.

It is very error prone to add further restrictions. If you could suggest specific changes to the predicate, I would definitely be grateful. However, it may also lead us down a wrong path: Ideally, such deductions should be derived automatically, from the laws of arithmetic. Maybe that is possible! If we find a way to do it, we could be more certain about its correctness, if the same approach is also used to deduce bounds in other propagators.

[notoria]

The operator (**) seems to be missing and since (^) can't handle all negative numbers in the case ?- X #= B ^ E, B #= -1, E #= -2., would it be extended?

[triska]

I have filed #559 about this: This should actually be made to work in the core engine. Thank you a lot for noting this!