理解clpfd中label/5的实现

编程问答 2022-07-30

问题描述

我正在尝试了解 clpfd 库中 label/5 谓词的实现（我了解用法）：

(copied from here)


1824label([],_,Consistency) :- !,1825        (   Consistency = upto_in(I0,I) -> I0 = I
1826        ;   true
1827        ).
1828label(Vars,Selection,Order,Choice,Consistency) :-
1829        (   Vars = [V|Vs],nonvar(V) -> label(Vs,Consistency)
1830        ;   select_var(Selection,Vars,Var,RVars),1831            (   var(Var) ->
1832                (   Consistency = upto_in(I0,I),fd_get(Var,Ps),all_dead(Ps) ->
1833                    fd_size(Var,Size),1834                    I1 is I0*Size,1835                    label(RVars,upto_in(I1,I))
1836                ;   Consistency = upto_in,all_dead(Ps) ->
1837                    label(RVars,Consistency)
1838                ;   choice_order_variable(Choice,RVars,Consistency)
1839                )
1840            ;   label(RVars,Consistency)
1841            )
1842        ).

尤其是标记部分（显然是重要的部分）让我感到困惑：

  • 我不太清楚fd_get（/3或/5）的作用
  • all_dead 使用某种 propagator（我还没有研究过）
  • 如何“枚举”Var？

我显然遗漏了可能需要为此理解的证明机制的一些组成部分，所以我很好奇关于这个实现的行为的一些更高级别的解释（可能有一些资源可以阅读）。

解决方法

免责声明：以下答案只是我在浏览代码并在 SWISH 中玩了一下之后的有根据的猜测。

首先，整个标记部分及其下方的两行（即 1836-1837 行）似乎与 labeling/2 的未记录选项有关，我将其称为 upto_in (在函子的名字之后）。我将尝试解释我认为此选项的作用。

通常，当调用 labeling/2 时，所有 FD 变量（在其第二个参数中）都以成功为基础。这就是标签的真正作用：一个接一个地分配变量，直到它们全部被分配。例如，在以下代码段中，labeling/2 在 X 和 Y 接地的情况下成功了 6 次：

?- [X,Y] ins 1..4,X #< Y,labeling([],[X,Y]).
X = 1,Y = 2 ;
X = 1,Y = 3 ;
X = 1,Y = 4 ;
X = 2,Y = 3 ;
X = 2,Y = 4 ;
X = 3,Y = 4

作为比较，当不使用 labeling/2 时，我们可以看到两个变量的（减少的）域以及约束仍然未决的事实。

?- [X,X #< Y.
X in 1..3,X #=< Y + -1,Y in 2..4

当约束处于待定状态时，这意味着变量值的每个组合（在本例中为 X 和 Y）可能是也可能不是解决方案。相反，如果没有待处理的约束，那么我们知道每个值的组合都是一个解决方案。在某些应用程序中，当我们确定所有值组合都是解决方案时，可能会考虑停止标记。简而言之，这就是选项 upto_in 的作用：它告诉在没有约束未决时避免标记。回到我们的运行示例，这显示为：

?- [X,labeling([upto_in],Y in 2..4 ;
X = 2,Y in 3..4 ;
X = 3,Y = 4

所以第一个解决方案意味着对于 X = 1，Y 可以采用从 2 到 4 的所有值。

请注意，upto_in 有两种风格，第一种如上所示，第二种带有参数，该参数表示生成的答案中包含的基本解决方案的数量。所以：

?- [X,labeling([upto_in(K)],Y in 2..4,K = 3 ;
X = 2,Y in 3..4,K = 2 ;
X = 3,Y = 4,K = 1

再举一个例子，如果删除唯一的约束，我们会看到（地面）解的数量是域的笛卡尔积（并且没有实际标记发生）。

?- [X,Y]).
K = 16,X in 1..4,Y in 1..4

这第二个选项可能很有用，例如当人们想要计算一个问题的解决方案的数量时。然后 upto_in/1 允许人们对“不相关”变量进行快捷标记以获得更好的性能，同时跟踪实际解决方案的数量。

现在，回答更具体的问题：

  • fd_get(V,D,Ps) “返回”变量 V：它的当前域 D 和一个结构 Ps 与（3 个）传播器关联。传播器基本上是已发布约束的内部实现，其作用是从域中删除不可能的值。在上面的示例中，Ps 将包含（表示？）不等式约束的传播器，并且该传播器在所有情况下都会从 1 和 { {1}} 来自 Y 的域。 4 还返回域的上限和下限。
  • X 似乎检查与变量关联的所有传播器是否“死”，这意味着在这种情况下，出现在其中的变量域中的所有值组合都是解决方案。 （我说“似乎”是因为这确实涉及到 fd_get/5 库的内部结构，我不想深入挖掘。）
  • 它并没有真正枚举 all_dead/1。为了解释标记代码在一个句子中的作用，我会写：“如果使用了 clpfd 选项并且没有可能进一步减少 Var 域的约束，那么跳过枚举 {{ 1}}（并将某个累加器乘以其域的大小）。”

希望这有助于您的理解。如果有知识渊博的人在我的解释中发现错误或漏洞，请随时纠正它们。

clpfdimplementationimplementationlabelingprologprologswi-prolog