Функция по модулю и переменная область


Вот простое отношение CLPFD:

1 #= 81 mod X.

Это возвращает:

X in inf.. -1/1..sup,
81 mod X#=1.

Если моя математика полностью неверна, не должна ли область X быть -80.. -1/1..80?

2 3

2 ответа:

Прежде всего:

Есть ли ошибка в решателе ограничений?

Нет (t обязательно), потому что все допустимые решения все еще содержатся в области, которая выводится, и никакие неправильные решения не сообщаются. Домен, который вы вывели, является правильным подмножеством того, что сообщает решатель.

Распространяется ли решатель ограничений так же хорошо, как он мог бы в этом случае?

Нет , очевидно, нет, как уже показывают ваши более сильные границы. На самом деле допустимая область даже меньше, чем то, что вы вывели: X in 2..80 будет также допустимой, потому что X определенно может не быть отрицательной, и это также не может быть равно 1.

Упражнение : является ли X in 2..80 наименьшей (по отношению к включению множества) областью, которая может быть выведена в этом случае? Почему (нет)? И в каком смысле она минимальна?

Итак, что же происходит - здесь?

Объяснение довольно простое: реализация (mod)/2, (rem)/2, (div)/2 и-в несколько меньшей степени-даже (*)/2 таким образом, что они распространяются как можно больше во всех случаях жестоко трудно получить право, и явно не было сделано в этом случае.

Должны ли мы жить с этим недостатком?

Нет , потому что мы можем улучшить решатель ограничений для обработки таких случаев тоже! То есть мы можем добавить логика такова, что она распространяется сильнее ! Делать это элегантно и правильно - это вообще нерешенная проблемаи предмет активного исследования . См., например: обучение решателя ограничений конечной области, ссылки включены в него, а также в ряд других документов. Конечно, мечта состояла бы в том, чтобы каким-то образом вывести распространение непосредственно из спецификации этих операций, которая находится по крайней мере через десятилетия. До тех пор, такие вопросы находят и совершенствуют скорееad hoc .

Отказ от ответственности: я не знаю, о чем я говорю, я просто хотел сам увидеть, что происходит, и подумал, что было бы полезно поделиться.

С SWI-прологом и библиотекой (clpfd):

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

?- 1 #= 81 rem X.
X in inf.. -1\/1..sup,
81 rem X#=1.

?- 1 #= 81 mod X.
X in inf.. -1\/1..sup,
81 mod X#=1.

?- 1 #= 81 - X * (81 // X ).
X in -80.. -1\/1..80,
X*_G1053#=80,
81//X#=_G1053,
_G1053 in -80.. -1\/1..80.

Странно, разве выражение в последнем примере не должно быть таким, как определено деление по модулю?

Если вы берете Gnu-Prolog (mod не поддерживается напрямую):

| ?- 1 #= 81 rem X.

X = _#4(2..80)

yes
| ?- 1 #= 81 - X * (81 // X).

no

Хм. Что если вы просто переупорядочите выражение:

| ?- 1 #= 81 - (81 // X) * X.

X = _#4(2..80)

yes

Вывод: да, похоже что написать хорошую библиотеку CLP(FD) действительно непросто. Можно даже создать впечатление, что эти библиотеки демонстрируют эмерджентное поведение, о котором авторы не всегда полностью осведомлены.