CODEWITHSUNDEEP
prologclpfd
Erhannis
Erhannis

Reputation: 4462

Prolog CLPFD Transitivity

"Obvious" is not a word lightly bandied about, but why does SWI-Prolog's CLPFD correctly solve this:

?- A+1 #= A*2.
A = 1.

but not this:

?- B #= A + 1, B #= A * 2.
A+1#=B,
A*2#=B.

(label and indomain yield Arguments are not sufficiently instantiated.)

Is it just...the solver doesn't catch that case? (I'd sure have expected it to apply transitivity.) Or is it a symptom of some deeper syntactic conundrum, or something?

Upvotes: 3

Views: 108

Answers (1)

OmG
OmG

Reputation: 18838

It tries to solve the constraint from the values in the domain of each variable! As the domain of B and A is infinite and not bound, backtracking over a constraint satisfaction will be delayed and the program is stopped.

It means it tries to find some solution for the constraint B #= A + 1, but it finds many (infinite values for A and B) and also the same for the second constraint. Hence it will be stopped here as the possible values of A and B are infinite. However, the result is not No. It is Yes with 2 delayed goals.

B = B{-1.0Inf .. 1.0Inf}
A = A{-1.0Inf .. 1.0Inf}
There are 2 delayed goals.

To solve this, you need to bound at least one of the A or B. For example, if you run this query A::1..1000, B#=A+1, B #= A*2., you will get the same result as for the first query in your examples. And also, there is not any deduction in clpfd to resolve the transitivity as it uses from the backtracking method.

In sum, it is one of the shortcomings of the library that you are using, as it will be stopped when the domain of a constraint with more than one variable has an infinite domain and you can solve it by setting a bounded domain for at least one of the variables.

Upvotes: 3

Related Questions