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

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

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

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

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

Answer 2

Кажется, вы имеете дело с 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, это такжеНемного зависит от того, насколько умным является воплощение.Но я думаю, что в данном случае это только вопрос распространения.Теперь мы найдем для вашего примера:

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.

Пока