如何解决理解clpfd中label/5的实现
我正在尝试了解 clpfd
库中 label/5 谓词的实现(我了解用法):
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}}(并将某个累加器乘以其域的大小)。”
希望这有助于您的理解。如果有知识渊博的人在我的解释中发现错误或漏洞,请随时纠正它们。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。