问题描述:

I am doing some toy tests with the CLPFD library in swi-prolog.

Does anybody know why the program below does not work?

`start(X,Y):-`

Vars = [X,Y],

Vars ins 1..3,

abs(X-Y) #>= 2,

X #>= Y,

nl,

write([X,Y]), nl.

The expected answer for start(X,Y) would be X=3 and Y=1. However, swi-prolog indicates me multiple answers. The program works properly if I replace

`abs(X-Y) #>= 2`

by

`X-Y #>= 2`

My question is whether I am using the abs operator in the right way.

First of all, constraints and side-effects do not flock together. Instead, simply stick to the pure part of your program:

```
start(X,Y):-
Vars = [X,Y],
Vars ins 1..3,
abs(X-Y) #>= 2,
X #>= Y.
```

And now, query your relation:

```
?- start(X,Y).
X in 1..3,
X#>=Y,
abs(X-Y)#>=2,
Y in 1..3.
```

The answer is a conditional one:

Yes, there are solutions for

`X`

and`Y`

provided all these conditions hold.

To get actual values, you have to eliminate all these conditions. You have several options:

In this case, you can use `labeling/2`

:

```
?- start(X,Y), labeling([], [X,Y]).
X = 3,
Y = 1.
```

So there is exactly one solution. The `clpfd`

-solver alone was not powerful enough to come to this conclusion, it needed some extra help.

Even better would be to use `contracting/1`

:

```
?- start(X,Y), clpfd:contracting([X,Y]).
X = 3,
Y = 1.
```

In contrast to labeling, contracting tries to reduce the size of the domain without (visible) search. This makes the solver a bit stronger.

Reasons why the solver is not powerful enough

in the very general case solving such arithmetic problems is undecidable.

in more specific cases the algorithms would be extremely costly. In fact, there is more than one diophant in the room.

even simpler algorithms are very costly in terms of both implementation effort and runtime.

for many situations, the solver boils down to maintaining consistencies within one constraint

^{1}. So the only way to "communicate" between different constraints are the domains of variables.

In your case, the abs-constraint admits more solutions!

```
?- [X,Y]ins 1..3, abs(X-Y)#>=2, labeling([],[X,Y]).
X = 1,
Y = 3 ;
X = 3,
Y = 1.
?- [X,Y]ins 1..3, X-Y#>=2, labeling([],[X,Y]).
X = 3,
Y = 1.
```

What you expect is that the extra constraint `X #>= Y`

would help. Alas, the concrete consistency mechanisms are too weak. And not even `X #> Y`

helps:

```
?- [X,Y]ins 1..3, abs(X-Y)#>=2, X#>Y.
X in 2..3,
Y#=<X+ -1,
abs(X-Y)#>=2,
Y in 1..2.
```

However, if you switch from SWI to SICStus, things are a bit different:

```
| ?- assert(clpfd:full_answer).
yes
| ?- X in 1..3, Y in 1..3, abs(X-Y)#>=2.
Y+_A#=X,
X in 1..3,
Y in 1..3,
_A in{-2}\/{2} ? ;
no
| ?- X in 1..3, Y in 1..3, abs(X-Y)#>=2, X#>Y.
X = 3,
Y = 1 ? ;
no
```

Please note how abs is resolved!

And using SICStus with `library(clpz)`

has the same strength:

```
| ?- X in 1..3, Y in 1..3, abs(X-Y)#>=2, X#>Y.
X = 3,
Y = 1 ? ;
no
```

^{1 Note that I avoid to use the notion of local consistency as opposed to global consistency, since quite often also global consistency only refers to consistency within one "global" constraint.}

您可能感兴趣的文章：

- android - How to handle with Events.RRULE
- python - Issue with unit test for tiny Flask app
- hudson - How to manage resource pool dynamically on Jenkins
- django - "TypeError: argument must be a context" after update from Python 3.4 to 3.5
- Extract data from variable based on column heading in R
- php - Reading a specific line from a text file
- clr - Any implementation of an Unrolled Linked List in C#?
- Finding Hudson Log Files
- Forward to a payment-gateway together with POST data using cURL (or any other PHP server side solution)
- WCF in Winforms app - is it always single-threaded?

随机阅读：

**推荐内容**-

**热点内容**-
- php - Reading a specific line from a text file
- clr - Any implementation of an Unrolled Linked List in C#?
- Finding Hudson Log Files
- Forward to a payment-gateway together with POST data using cURL (or any other PHP server side solution)
- WCF in Winforms app - is it always single-threaded?
- git svn - git svn fetch does not fetch a Subversion commit message modified after initial clone
- java me - Why I am getting the bad length exception when I am running this application?
- java - How to get string.format to complain at compile time
- ruby on rails - Trigger observer of parent class on change
- python - Issue with URL pattern in Django with webmonkey tutorial