SWI-Пролог и ограничения, библиотека CLP(FD)

Question

Я играю с ограничениями в прологе (swi), используя библиотеку clpfd.

Я пытаюсь определить, когда один набор ограничений инкапсулирует или включает в себя другой, например, X<4 инкапсулирует X<7, так как всякий раз, когда первое истинно, последнее истинно. Это можно легко представить с помощью логического подтекста. Однако я не смог заставить оператор #==> дать мне нужный результат, поэтому я прибегнул к использованию not(Co1 #/\ #\Co2), где Co1 и Co2 - ограничения. Это хорошо для отдельных ограничений, но затем я хотел передать соединения ограничений в Co1 и Co2.

Теперь вот руб. Когда я пытаюсь

X#<7 #/\ #\X#<4.

Я вернусь

X in 4..6,
X+1#=_G822,
X+1#=_G834,
_G822 in 5..7,
_G834 in 5..7.

(как ни странно, выполнение этого в Sicstus приводит к ошибке сегментации)

Когда я прохожу в

X#<7,X#<4

Я получаю желаемое

X in inf..3.

Очевидно, я не могу передать последнее в not(Co1 #/\ #\Co2), но первое не дает мне желаемого результата. Может кто-нибудь объяснить, почему два подхода дают разные результаты, и как я могу заставить первый действовать как второй?

Answer 1

Кажется, вы имеете дело с CLP(FD). Эти решатели различают этап настройки и этап маркировки для решения проблемы ограничения.

Решатель CLP (FD) не полностью устраняет проблему на этапе установки. Так как у него есть шанс уменьшить переменные диапазоны на этапе маркировки. Таким образом, может случиться так, что во время установки будет поставлена ​​проблема, которая может быть уменьшена другими решателями до "Нет", но это не будет с решателем CLP(FD). Только во время маркировки будет обнаружено "Нет".

Степень сокращения, достигнутая на этапе настройки, сильно зависит от конкретной системы CLP(FD). Некоторые системы CLP (FD) делают большее сокращение на этапе настройки, в то время как другие делают меньше. Например, в GNU Prolog используется некоторое индексное распространение, а в SWI Prolog - нет. Итак, мы находим, например, не ваш пример:

SWI-Prolog:

?- X #< Y, Y #< Z, Z #< X.
Z#=<X+ -1,
X#=<Y+ -1,
Y#=<Z+ -1.

GNU Prolog:

?- X #< Y, Y #< Z, Z #< X.
(7842 ms) no

Кроме того, поскольку вы используете ограничения reified, это также немного зависит от того, насколько умным является reification. Но я думаю, что в данном случае это только вопрос распространения. Теперь мы найдем для вашего примера:

SWI-Prolog:

?- X #< 4 #==> X #< 7.
X+1#=_G1330,
X+1#=_G1342,
7#>=_G1330#<==>_G1354,
_G1354 in 0..1,
_G1377#==>_G1354,
_G1377 in 0..1,
4#>=_G1342#<==>_G1377.

GNU Prolog:

?- X #< 4 #==> X #< 7.
X = _#22(0..268435455)

Существует компромисс между выполнением большего сокращения на этапе настройки и передачей большей работы на этап маркировки. И все дело также зависит от приведенного примера. Но если у вас также есть метки рядом с настройкой, вы не увидите никакой разницы с точки зрения результата:

SWI-Prolog:

?- X in 0..9, X #< 4 #==> X #< 7, label([X]).
X = 0 ;
X = 1 ;
X = 2 ;
X = 3 ;
X = 4 ;
X = 5 ;
X = 6 ;
X = 7 ;
X = 8 ;
X = 9.

GNU Prolog:

?- fd_domain(X,0,9), X #< 4 #==> X #< 7, fd_labeling([X]).
X = 0 ? ;
X = 1 ? ;
X = 2 ? ;
X = 3 ? ;
X = 4 ? ;
X = 5 ? ;
X = 6 ? ;
X = 7 ? ;
X = 8 ? ;
X = 9

Я не тестировал с SICStus Prolog или B-Prolog. Но я думаю, что они будут вести себя где-то в непосредственной близости от SWI-Prolog и GNU Prolog.

CLP (Q) не является реальной альтернативой, если ваш домен действительно FD, поскольку он пропустит некоторые сокращения "Нет", которые не пропустит CLP(FD). Например, следующее является неудовлетворительным в CLP(FD), но удовлетворительным в CLP(Q):

X = Y + 1, Y < Z, Z < X.

до свидания

Answer 2

Подчинение общих арифметических ограничений над целыми числами вообще неразрешимо, поэтому все правильные решатели имеют присущие им пределы, за которыми им приходится откладывать ответы до тех пор, пока не станет известно больше. Если вы знаете, что ваши домены являются конечными, вы можете опубликовать домены, а затем попытаться найти контрпримеры, которые сделают импликацию недействительной, используя предикат /2 для метки ограничителя. Учтите также, что линейные неравенства над Q разрешимы, и что библиотека SWI-Prolog (clpq) для них полна. Таким образом, вы можете попробовать свои ограничения в CLP(Q) с помощью:

?- use_module(library(clpq)).
true.

?- { X < 4, X >= 7 }.
false.

и видим, что такого контрпримера не существует в Q (следовательно, также и в Z), и, следовательно, импликация имеет место.