Prolog中的公式化

Question

我目前有以下问题，希望用Prolog解决。这是一个简单的例子，在Java/C或其他语言中很容易解决。我的问题是，我认为自己过于依赖Java的思维方式，无法用Prolog的逻辑能力来表达问题。

问题是...

我有6支箭，它们要么指向左边，要么指向右边。假设它们的初始配置如下:

->
<-
->
<-
->
<-

现在，只要两个箭头相邻，我就可以交换它们。我的目标是发现哪个操作序列能使最初的箭头配置变成

<-
<-
<-
->
->
->

我最初尝试阐述问题的方法是..

(此处涉及IT技术相关内容，具体涵义需要结合上下文进行翻译)

right(arrow_a).
left(arrow_b).
right(arrow_c).
left(arrow_d).
right(arrow_e).
left(arrow_f).

atPosition(1, arrow_a).
atPosition(2, arrow_b).
atPosition(3, arrow_c).
atPosition(4, arrow_d).
atPosition(5, arrow_e).
atPosition(6, arrow_f).

这将告诉Prolog箭头的初始配置是什么。但现在如何在其中插入附加逻辑呢？例如如何实现switchArrows(Index)？在Prolog中像这样声明初始条件，是否正确？当我尝试设置例如arrow_a在位置6时，atPosition(6, arrow_a)不会干扰后面的操作吗？

- devoured elysium

Answer 1

你的问题可以看作是在不同状态之间进行转换的一系列过程。首先，考虑如何表示单个状态。例如，你可以使用列表来表示初始状态[->,<-,->,<-,->,<-]。单个移动可以用关系step/2来描述，该关系用于step(State0, State)，描述了通过翻转相邻箭头可以从彼此“到达”的两个状态之间的关系。它通常是不确定的。然后，你的主谓语描述了一系列状态转换，从初始状态到目标状态。由于你想描述一个列表（状态列表），因此DCGs很适合：

solution(State0, Target) -->
    (    { State0 == Target } -> []
    ;    { step(State0, State1) },
         [State1],
         solution(State1, Target)
    ). 

如果存在解决方案，则可以使用迭代加深来查找解决方案，如下所示：

?- length(Solution, _), phrase(solution([->,<-,->,<-,->,<-], [<-,<-,<-,->,->,->]), Solution).

好的一点是，Prolog会自动回溯一旦尝试了所有给定长度的序列并且目标状态尚未达到。现在只需要实现step/2，就完成了。

- mat

Answer 2

既然已经有完整的解决方案了，这里是我的:

solution(State0, Target) -->
    (    { State0 == Target } -> []
    ;    { step(State0, State1) },
         [State1],
         solution(State1, Target)
    ).

flip(->, <-).
flip(<-, ->).

step([], []).
step([A|Rest0], [A|Rest]) :- step(Rest0, Rest).
step([A0,A1|Rest], [B0,B1|Rest]) :- flip(A0, B0), flip(A1, B1).

示例查询：

?- length(Solution, _), phrase(solution([->,<-,->,<-,->,<-], [<-,<-,<-,->,->,->]), Solution).
Solution = [[->, <-, ->, <-, <-, ->],
            [->, <-, ->, ->, ->, ->],
            [->, ->, <-, ->, ->, ->],
            [<-, <-, <-, ->, ->, ->]].

由于使用了迭代加深，我们知道没有比4步更短的解决方案可行。

我对你说的话有一般性的评论：

“这是一个简单的例子，在Java / C /任何其他语言中都可以轻松解决。我的问题是，我认为自己过于依赖Java的思维方式，无法以能够利用Prolog逻辑能力的方式来表达问题。”

个人认为，这个例子已经超出了一个初学者（比如Java程序员）的预期要求。请尝试在Java / C /任何其他语言中解决此问题，看看您能走多远。根据我的经验，当学生们说他们“过于依赖Java的思维方式”等等时，他们也无法在Java中解决问题。Prolog是不同的，但并不是“那么”不同，如果您对如何在Java中解决问题有清晰的想法，就可以将其直接转换为Prolog。我的解决方案使用了Prolog的内置搜索机制，但您不必这样做：您可以像在Java中一样自己实现搜索。

- mat

---

嗯，有趣，你是如何避免检查之前的步骤（以免进入无限循环），并且如何先找到最小的解决方案的？我相信这是因为不同的步进算法（与我的解决方案相比）？ - Volodymyr Gubarkov

好的，我已经达到了最小长度。这是因为length（Solution，_）使其从找到1步解决方案开始，然后是2步，依此类推。有趣！ - Volodymyr Gubarkov

感谢回答。我会努力消化它，直到我理解它为止。我已经在C/Python中实现了更先进的算法（Q学习/神经网络/粒子群优化）。 - devoured elysium

顺便说一下，似乎你的算法并没有完全做到它应该做的事情，但可能只是因为我没有很好地描述问题。我的想法是交换任意两个相邻箭头。从你的解决方案的第一行到第二行似乎并没有发生这种情况。 - devoured elysium

这意味着左箭头和右箭头的数量必须保持不变。 - devoured elysium

Answer 3

这是我的解决方案：

solution(Begin, End, PrevSteps, [Step | Steps]) :-
    Step = step(Begin, State1),
    Step,
    forall(member(step(S, _), PrevSteps),
           State1 \= S
          ), % prevent loops
    (   State1 == End
    ->  Steps = []
    ;   solution(State1, End, [Step | PrevSteps], Steps)
    ).

rev(->,<-).
rev(<-,->).

step([X,Y|T], [XX,YY|T]) :- rev(X,XX), rev(Y, YY).
step([A,X,Y|T], [A,XX,YY|T]) :- rev(X,XX), rev(Y, YY).
step([A,B,X,Y|T], [A,B,XX,YY|T]) :- rev(X,XX), rev(Y, YY).
step([A,B,C,X,Y|T], [A,B,C,XX,YY|T]) :- rev(X,XX), rev(Y, YY).
step([A,B,C,D,X,Y], [A,B,C,D,XX,YY]) :- rev(X,XX), rev(Y, YY).


run :-
    solution([->,<-,->,<-,->,<-], [<-,<-,<-,->,->,->],[],Steps),
    !,
    forall(member(Step,Steps),writeln(Step)).

它只找到了所有可能解中的第一个解，虽然我认为找到的解不是最优的，而是第一个可行的解。

- Volodymyr Gubarkov

---

他的问题看起来像是一道作业题。给他写出整个解决方案可能有点不妥，最好只是帮助他入门。 - Dan

Answer 4

成功将Mat的代码转换为Mercury：

:- module arrows.

:- interface.

:- import_module io.

:- pred main(io, io).
:- mode main(di, uo) is cc_multi.

:- implementation.

:- import_module list, io, int.

:- type arrow ---> (->); (<-).

:- mode solution(in, in, in, in, out, in) is cc_nondet.
solution(State0, Target, MaxDepth, CurrentDepth) -->
    {CurrentDepth =< MaxDepth},
    (    { State0 = Target } -> []
    ;    { step(State0, State1) },
         [State1],
         solution(State1, Target, MaxDepth, CurrentDepth + 1)
    ).

flip(->, <-).
flip(<-, ->).

step([], []).
step([A|Rest0], [A|Rest]) :- step(Rest0, Rest).
step([A0,A1|Rest], [B0,B1|Rest]) :- flip(A0, B0), flip(A1, B1).

main -->
    (({
    member(N, 1..10),
        solution([->,<-,->,<-,->,<-], [<-,<-,<-,->,->,->], N, 0, Solution, [])
    }) 
    -> print(Solution)
    ; print("No solutions")
    ).

使用mmc --infer-all arrows.m编译，以推断签名和确定性

- Volodymyr Gubarkov