Функция по модулю и переменная область
Вот простое отношение CLPFD:
1 #= 81 mod X.
Это возвращает:
X in inf.. -1/1..sup,
81 mod X#=1.
Если моя математика полностью неверна, не должна ли область X
быть -80.. -1/1..80
?
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) действительно непросто. Можно даже создать впечатление, что эти библиотеки демонстрируют эмерджентное поведение, о котором авторы не всегда полностью осведомлены.