Fab*_*der 3 implementation prolog swi-prolog labeling clpfd
我试图了解库中label/5 谓词的实现（我了解用法）clpfd：
（从这里复制）
1824label([], _, _, _, 一致性) :- !, 1825（一致性= upto_in（I0，I）-> I0 = I 1826 年；真的 1827 年）。 1828label（变量、选择、顺序、选择、一致性）：- 1829 (Vars = [V|Vs], nonvar(V) -> label(Vs, Selection, Order, Choice, Consistency) 1830 年；select_var（选择，Vars，Var，RVars）， 1831 ( var(Var) -> 1832（一致性= upto_in（I0，I），fd_get（Var，_，Ps），all_dead（Ps）-> 第 1833 章 1834 I1是I0*大小， 1835标签（RVars，选择，顺序，选择，upto_in（I1，I）） 1836 年；一致性 = upto_in, fd_get(Var, _, Ps), all_dead(Ps) -> 1837 标签（RVars、选择、顺序、选择、一致性） 1838 年；choice_order_variable（选择、顺序、变量、RVars、变量、选择、一致性） 第1839章 1840 年；标签（RVars，选择，顺序，选择，一致性） 第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,Y] ins 1..4, X #< Y.
X in 1..3, X #=< Y + -1, Y in 2..4
当约束处于待定状态时，这意味着变量的每个值组合（在本例中为X和Y）可能是也可能不是解决方案。相反，如果没有待处理的约束，那么我们知道每个值的组合都是一个解决方案。在某些应用程序中，当我们确定所有值组合都是解决方案时，可能会考虑停止标记。简而言之，这就是该选项的upto_in作用：它告诉在没有未决约束时避免标记。回到我们的运行示例，这显示为：
?- [X,Y] ins 1..4, X #< Y, labeling([upto_in],[X,Y]).
X = 1, Y in 2..4 ;
X = 2, Y in 3..4 ;
X = 3, Y = 4
所以第一个解决方案意味着 for X = 1，Y可以采用从 2 到 4 的所有值。
请注意，upto_in它有两种风格，第一种如上所示，第二种带有参数，它表示生成的答案中包含的基本解决方案的数量。所以：
?- [X,Y] ins 1..4, X #< Y, labeling([upto_in(K)],[X,Y]).
X = 1, Y in 2..4, K = 3 ;
X = 2, Y in 3..4, K = 2 ;
X = 3, Y = 4, K = 1
再举一个例子，如果删除唯一的约束，我们会看到（地面）解决方案的数量是域的笛卡尔积（并且没有实际标记发生）。
?- [X,Y] ins 1..4, labeling([upto_in(K)],[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从 的域Y和4的域中删除X。fd_get/5此外返回域的上限和下限。all_dead/1似乎检查与变量关联的所有传播器是否“死”，这意味着在这种情况下，出现在其中的变量域中的所有值组合都是解决方案。（我说“似乎”是因为这确实涉及到clpfd图书馆的内部结构，我不想深入挖掘。）Var。为了解释标记代码在一个句子中的作用，我会写：“如果使用该upto_in选项并且没有可能Var进一步减少域的约束，则跳过枚举Var（并将某些累加器乘以其域的大小） .”希望这有助于您的理解。如果更有知识的人在我的解释中发现错误或漏洞，请随时修复它们。