CLP (FD) вариабельные домены и распространение - PullRequest
Новая
       45

CLP (FD) вариабельные домены и распространение

3 голосов
/ 09 января 2020

В моем курсе Пролог в прошлом семестре я немного отстал от времени, когда был введен CLP. Теперь я пытаюсь наверстать упущенное и попробовал свои силы на прошедшем экзамене, который профессор дал всем студентам.

В частности, возник такой вопрос:

Что является областью переменной решения Z в CLP (FD) после следующего запроса:

?- X in 1..7, Y in -3..100, Y #> X, Z #\= 0, Z #= Y - X.

Мне кажется, что ответ должен быть 

Z in 1..99

но когда я запустил его в своей установке SWI-Prolog для двойной проверки, я получил 

Z in -5.. -1\/1..99

, который, кажется, основан на наивном сравнении максимальных и минимальных значений X & Y, без учета ограничения, связывающего их (Y #> X).

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

Мои вопросы

  1. Я предполагаю, что это связано с тем, как CLP решает распространять (или не распространять) различные ограничения внутри, но я не понять, как это происходит - для меня все это черный ящик. Каким образом (или приблизительно, если это не удается) CLP распространяет свои ограничения?
  2. Существует ли какой-либо способ заставить CLP (FD) соответствующим образом применить ограничение, возможно, путем переупорядочения? Я уже пытался добавить дополнительный Y #> X в конце, но это не изменило ни один из доменов переменных.

1 Ответ

2 голосов
/ 09 января 2020

Мне кажется, что ответ должен быть 

Z in 1..99

Как вы можете быть настолько уверены, что вы правы? Это одно из приятных свойств ограничений: вы можете проверить это проще всего: 

?- X in 1..7, Y in -3..100, Y #> X, Z #\= 0, Z #= Y -X.
X in 1..7,
Z+X#=Y,
X#=<Y+ -1,
Z in -5.. -1\/1..99,
Y in 2..100.

?- X in 1..7, Y in -3..100, Y #> X, Z #\= 0, Z #= Y -X, Z #< 0.
false.

Хорошо, теперь я верю тому, что вы сказали.

Итак, вы обнаружили здесь несоответствие , которое присутствует также в нативном library(clpfd) SICStus, а также library(clpz). Во-первых, обратите внимание, что ответ не был неправильным! Он сказал: да, есть решения при условии X in 1..7, Z+X#=Y, X#=<Y+ -1, Z in -5.. -1\/1..99, Y in 2..100. верно. Хелас, это не правда.

Так что этот ответ немного похож на юридический во многих страховых договорах, где говорят, что да, мы будем платить, при условии, что все эти крошечные нечитаемые отпечатки удерживаются, но в действительности вы могли бы заменить это стена микротекста с большой жирной false.

В общем, такие несоответствия неизбежны, так как CLP (FD) / CLP (Z), как определено в вышеупомянутых системах, позволяет сформулировать неразрешимые проблемы. Таким образом, независимо от того, насколько эволюционировал ваш решатель ограничений, у нас есть гарантия, что всегда будут случаи, которые мы не можем решить. Это научный c, математический закон, гораздо более надежный, чем эмпирический aws, такой как гравитация или этот предел скорости.

Несоответствие здесь фактически является инженерным компромиссом. Пока никто не жалуется и не имеет убедительного варианта использования, разработчики таких систем не увидят причины для улучшения. В конце концов, такое улучшение может замедлить существующие варианты использования.

  1. Как именно (или приблизительно не сработает) CLP распространяет свои ограничения?

На самом деле, для любой проблемы реалистичности c размера никто не знает. Но и в этом нет необходимости. В случае CLP (FD) фундаментальным элементом являются домены, связанные с логическими переменными. Вы видите их как (in)/2 целей, таких как Z in -5.. -1\/1..99. Между ними связаны реальные ограничения. В вашем случае Y #> X и Z #= Y-X. Эти ограничения теперь видят только домены переменных и пытаются поддерживать согласованность между ними. В качестве еще более грубого приближения домены рассматриваются как интервалы, поэтому Z in -5 .. 99 вместо вышеупомянутых. Чего (большинство из них) не видят, так это других ограничений. В этом случае нет прямой связи между Y #> X и Z #= Y-X. И, таким образом, несоответствие. Такие ограниченные проверки непротиворечивости гораздо проще реализовать, а также довольно быстро и часто превосходят более полные алгоритмы. С открытием лучших алгоритмов вещи развиваются. Хорошим примером является all_distinct/1, который поддерживает согласованность между всеми переменными, используя алгоритм Реджина, тогда как all_different/1 поддерживает согласованность только между каждой парой переменных. Но в любом случае: эти вещи развиваются, и это немного удивительно, что это экзаменационный вопрос.

Есть ли способ заставить CLP (FD) применить ограничение соответствующим образом ...? 
?- X in 1..7, Y in -3..100, Y #> X, Z #\= 0, Z #= Y -X, clpfd:contracting([X,Y,Z]).
X in 1..7,
Z+X#=Y,
X#=<Y+ -1,
Z in 1..99,
Y in 2..100.

Но большинство проигнорирует эту проблему и просто добавит labeling([],[X,Y])

Что такое домен Z?

Это неоднозначный вопрос. Дайте оба в ответ.

...