Что может привести к тому, что Prolog преуспеет в совпадении, но потерпит неудачу, когда его попросят пометить выходные данные?

По-видимому, вы не «правильно» сопоставили проблему с FD, так как вы получаете «нет», когда пытаетесь пометить переменные.

Что вы делаете в программировании логики ограничений, так это настраиваете модель ограничений, в которой у вас есть переменные с доменом (в вашем случае логические значения с доменом [0,1]) и ряд ограничений между этими переменными. Каждое ограничение имеет правило распространения, которое пытается достичь согласованности для доменов переменных, для которых размещено ограничение. Несогласованные значения удаляются из доменов. Существует несколько типов непротиворечивости, но у них есть одна общая черта: ограничения сами по себе обычно не дают вам полного решения или даже не сообщают вам, существует ли решение для модели ограничений.

В качестве примера предположим, что у вас есть две переменные X и Y, обе с доменами [1..10] и ограничение X ‹ Y. Тогда правило распространения удалит значение 1 из домена Y и удалит 10 из домена из X. Затем он остановится, поскольку домены теперь согласованы: для каждого значения в одном домене существует значение в другом домене, так что ограничение выполняется.

Чтобы получить решение (где все переменные привязаны к значениям), вам нужно пометить переменные. Каждая маркировка пробуждает ограничения, связанные с помеченной переменной, запуская новый раунд распространения. Это приведет к решению (все переменные привязаны к значениям, ответ: да) или неудаче (в каждой ветви дерева поиска какая-то переменная заканчивается пустым доменом, ответ: нет)

Поскольку каждое ограничение направлено только на согласованность доменов переменных, для которых оно размещено, возможно, что невозможность, возникающая из-за комбинации ограничений, не будет обнаружена на этапе распространения. Например, три переменные X, Y, Z с областями значений [1..2] и парные ограничения-неравенства. Похоже, это произошло с вашей моделью ограничений.

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

Если вы не видите какой-либо очевидной невыполнимости (например, некоторые противоречащие друг другу ограничения, подобные приведенному выше примеру с неравенством), вам необходимо отладить свою программу. Если возможно, не используйте встроенный предикат маркировки, а напишите свой собственный. Затем вы можете добавить некоторый выходной предикат, который позволит вам отслеживать, какая переменная была создана и какие изменения в логических переменных решения это вызвало или привело ли это к сбою.

(@twinterer уже дал объяснение, мой ответ пытается взять его с другого ракурса)

Когда вы вводите запрос в Prolog, вы получаете ответ. Часто ответ содержит решение, иногда содержит несколько решений, а иногда вообще не содержит никакого решения. Довольно часто эти два понятия путают. Давайте посмотрим на примеры с GNU Prolog:

| ?- length(Vs,3), fd_domain_bool(Vs).                                       

Vs = [_#0(0..1),_#19(0..1),_#38(0..1)]

yes

Здесь у нас есть ответ, который содержит 8 решений. Это:

| ?- length(Vs,3), fd_domain_bool(Vs), fd_labeling(Vs).

Vs = [0,0,0] ? ;

Vs = [0,0,1] ? ;

...

Vs = [1,1,1]

yes

А теперь другой запрос. Это пример, на который ссылается @twinterer.

| ?- length(Vs,3), fd_domain_bool(Vs), fd_all_different(Vs).

Vs = [_#0(0..1),_#19(0..1),_#38(0..1)]

yes

Ответ выглядит так же, как и раньше. Однако он больше не содержит решения.

| ?- length(Vs,3), fd_domain_bool(Vs), fd_all_different(Vs), fd_labeling(Vs).

no

В идеале в таком случае верхний уровень сказал бы не «да», а «может быть». Фактически, CLP(R), одна из самых первых систем ограничений, сделала это.

Еще один способ сделать это немного менее загадочным — показать фактические задействованные ограничения. SWI делает это:

?- length(Vs,3), Vs ins 0..1, all_different(Vs).
Vs = [_G565,_G568,_G571],
_G565 in 0..1,
all_different([_G565,_G568,_G571]),
_G568 in 0..1,
_G571 in 0..1.

?- length(Vs,3), Vs ins 0..1, all_different(Vs), labeling([], Vs).
false.

Таким образом, SWI показывает вам все ограничения, которые должны быть соблюдены, чтобы получить конкретное решение. Прочтите ответ SWI так: Да, решение есть, если все это мелким шрифтом правда! Увы, мелкий шрифт неверен.

И еще один способ решить эту проблему — получить реализацию all_different/1 с более высокой согласованностью. Но это работает только в конкретных случаях.

?- length(Vs,3), Vs ins 0..1, all_distinct(Vs).
false.

В общем случае вы не можете ожидать, что система будет поддерживать глобальную согласованность. Причины:

• Поддержание последовательности может быть очень дорогим. Зачастую такие решения лучше делегировать маркировке. На самом деле простой all_different/1 часто быстрее, чем all_distinct/1.

• Алгоритмы лучшей согласованности часто очень сложны.

• В общем случае сохранение глобальной согласованности — неразрешимая проблема.