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

Question

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

Я пытаюсь определить, когда один набор ограничений инкапсулирует или объединяет другой, например. X < 4 инкапсулирует X < 7 как всегда, когда первое верно, последнее верно. Это можно легко представить с помощью логической импликации. Однако я не мог заставить оператор # ==> дать мне результат, который мне нужен, поэтому я прибегал к использованию не (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 

I получите желаемое

X in inf..3. 

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

Answer 1

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

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

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

SWI-Пролог:

?- 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 

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

SWI-Пролог:

?- 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. 

Bye

Answer 2

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

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

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

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