SWI-Prolog 使用位移 CLPFD 报告错误答案

Question

我在一个更大的代码库中遇到了这个问题，但将其缩减为一个最小的可重现示例。这是汇编程序的一些代码：

:- use_module(library(clpfd)).

bigconst(X) :- X #=< 0x3FF, X #>= 0.

asm(instruction('ADD', [A]), R) :-
  bigconst(A),
  R #= 0b0000 + (A << 4).
asm(instruction('SUB', [A]), R) :-
  bigconst(A),
  R #= 0b0001 + (A << 4).

组装时似乎可以工作：

?- asm(instruction('SUB', [5]), R).
R = 81.

但是在拆卸的时候好像失败了：

?- asm(I, 81).
I = instruction('ADD', [_42146]),
_42146 in 0..1023,
81#=_42146<<4 .

这是我的程序中的错误还是 Prolog 中的错误？我该如何解决这个问题？

Answer 1

当我找到答案时，它是大声笑。我使用了许多奇怪的模式来解决问题，但这是我以前从未使用过的模式。一旦我看到它起作用，我就知道我有一个用于工具箱的闪亮的新工具。

对于 CLP(FD) 问题，它们通常可以双向工作，这正是您想要的。您遇到的第一个问题是您有bigconst(A)，它的作用类似于警卫声明。所以把它扔掉吧。

接下来的事情是R #= 0b0000 + (A << 4) 按预期工作，但遇到问题，两种方式都不能按预期工作，

?- X #= 4 << 4.
X = 64.

?- 64 #= X << 4.
64#=X<<4.

反之亦然

B #= A >> 4.

也可以按预期工作，但也遇到了同样的问题。

?- X #= 64 >> 4.
X = 4.

?- 4 #= X >> 4.
4#=X>>4.

所以我尝试使用 in/2 添加一些约束，但没有奏效，然后意识到我已经拥有了所有需要的约束并且它们起作用了。

asm(instruction('ADD', [A]), R) :-
    R #= 0b0000 + (A << 4),
    A #= (R - 0b0000) >> 4.

示例用法

?- asm(instruction('ADD', [5]), R).
R = 80.

?- asm(I,80).
I = instruction('ADD', [5]).

为了表明这不是一击奇迹。

asm(instruction('SUB', [A]), R) :-
    R #= 0b0001 + (A << 4),
    A #= (R - 0b0001) >> 4.

示例用法

?- asm(instruction('SUB', [5]), R).
R = 81.

?- asm(I,81).
I = instruction('SUB', [5]).

Answer 2

这是我的程序中的错误还是 Prolog 中的错误？我该如何解决这个问题？

这是您正在使用的顶层的可用性错误。如果您非常仔细观察，您可能会发现一个小提示：

81#=_42146<<4 .
             ^ SPACE

这个小空间意味着：请注意，答案不止于此。事实上，有两个答案。第一个答案（来自'ADD'）是假的，它不包含任何解决方案。只有第二个答案包含一个解决方案。

请注意，Prolog 主要产生答案而不是解决方案。这就是我们谈论答案替换的原因。答案和解决方案之间的关系是微妙的。一个答案可能包含零到无限多个解决方案。

那么为什么 Prolog 不直接产生解决方案呢？

首先，对于非常无效的无限解决方案。想想length(L,3)，它有一个答案，其中包含所有长度为 3 的列表以及任何可以想象的元素，因此有无限多的解决方案。比如L = [1,2,3]或者L = [bof, toto, machin-maschin]或者L = [louis_XVI, bernie, bernie]等等。在逻辑变量的帮助下，我们可以将这个无限的三元素列表折叠成以下答案：L = [_A,_B,_C]。这就是逻辑变量的威力！

这种能力也用于约束。但是有了这种力量，就会带来很多责任和很多负担。毕竟，许多问题在一个方向上很容易计算，而在另一个方向上却很困难。你发现了这样一个问题。在这种情况下，可以考虑改进clpfd 以轻松处理这种情况，但在一般情况下它是不确定的。因此，有时根本没有算法。在这种情况下，给出一个虚假的答案（不一致，Scheinlösung，solution blanche）是系统能做的最好的事情。或者，它可能会产生错误并中止整个计算。但这很恶心。通常，我们可以忍受这种不一致。

以你的情况为例，如果你真的想确保存在解决方案，请通过标记它们来消除答案中的限制！

?- asm(I,81), I = instruction(_,[R]).
   I = instruction('ADD', [R]),
   R in 0..1023,
   81#=R<<4
;  I = instruction('SUB', [R]),
   R in 0..1023,
   80#=R<<4.

?- asm(I,81), I = instruction(_,[R]), labeling([],[R]).
   I = instruction('SUB', [5]),
   R = 5
;  false.

正如@Guy-Coder 所展示的那样，另一种方法是使约束更强。这可能有效（然后很好），但理解起来更复杂。在某些情况下也可能效率较低。这是一个真正的工程问题。在某些情况下，我们何时接受不一致作为更快解决方案的代价？