如何使用答案集编程从图中提取树？

Question

有一个无向图 (V,E)，边上的权重 w : E → N, a 目标 k ∈ N，阈值 O ∈ N。 重量小于阈值的图表。换句话说，选择 k 分别来自 V 和 E 的顶点和 k - 1 条边，使得它们 构成一棵树，以及所选边的权重之和 小于O。

编写一个以 V、E、w、k 和 O 作为输入的 ASP 程序，并找到 满足约束的边的选择，或输出 如果不能满足约束条件，则为“不可满足”。选择 边隐含地诱导顶点的选择，所以没有 需要明确显示选定的顶点。

这个问题的一个实例是通过谓词 vertex/1 提供的， 权重/3、目标/1 和阈值/1。所有边都有权重，所以 weight(a, b, 10) 形式的语句。可用于声明 顶点 a 和 b 之间同时存在一条边 声明它们的重量，并且不需要任何多余的边缘/ 2 谓词。

我尝试了以下方法：

% instance
vertex ( v1 ). vertex ( v2 ). vertex ( v3 ). 
vertex ( v4 ). vertex ( v5 ). vertex ( v6 ). 
vertex ( v7 ). vertex ( v8 ). vertex ( v9 ).
weight ( v1 , v2 ,3). weight ( v1 , v3 ,3). 
weight ( v2 , v4 ,1). weight ( v2 , v5 ,5). 
weight ( v3 , v4 ,3). weight ( v3 , v6 ,4). 
weight ( v4 , v5 ,4). weight ( v4 , v7 ,1). 
weight ( v5 , v7 ,7). 
weight ( v6 , v7 ,2). weight ( v6 , v8 ,2). 
weight ( v7 , v9 ,3). 
weight ( v8 , v9 ,2).
target (4).
threshold (4).

% encoding
(P-1) {select(X, Y) : weight(X, Y, Z)} (Q-1) :- target(P), target(Q).
sum(S) :- S = #sum {W,X,Y : select(X,Y), weight(X,Y,W); W,X,Z : select(X,Z), weight(X,Z,W) }.
:- sum(S),threshold(M), S > M.
:- select(A,B), select(C,D), A == C ; A == D ; B == C ; B == D. 

#show select/2.

我得到以下输出：

clingo version 5.5.0
Reading from stdin
Solving...
Answer: 1
select(v2,v4) select(v4,v7) select(v6,v7)
Answer: 2
select(v2,v4) select(v4,v7) select(v6,v8)
Answer: 3
select(v2,v4) select(v4,v7) select(v8,v9)
SATISFIABLE

Models       : 3
Calls        : 1
Time         : 0.013s (Solving: 0.00s 1st Model: 0.00s Unsat: 0.00s)
CPU Time     : 0.000s

我只是期待

select(v2,v4) select(v4,v7) select(v6,v7)

因为其他的显然不是发辫。

我认为这是因为有问题的行：

:- select(A,B), select(C,D), A == C ; A == D ; B == C ; B == D.

我该如何纠正这个问题？

Answer 1

好的，那是相当复杂的。我很确定我的解决方案并不完美，我也是初学者。

在开始编写代码之前，让我们再次检查一下问题：要求是选择k 节点和k-1 边。如果您稍微考虑一下，这可以形成两种模式：一棵连通树或多个非连通图，其中至少有一个循环。因此，如果您确保没有循环，您将获得一棵连接的树。

我在事实中添加了一些节点以检查是否形成了树或是否找到了廉价的未连接循环，为此我必须将 target 和 threshold 更改为更高的值。

1

#const n = 5.

vertex ( v1; v2; v3; v4; v5; v6; v7; v8; v9 ).
vertex ( m1; m2; m3 ). 
weight ( v1 , v2 ,3). weight ( v1 , v3 ,3). 
weight ( v2 , v4 ,1). weight ( v2 , v5 ,5). 
weight ( v3 , v4 ,3). weight ( v3 , v6 ,4). 
weight ( v4 , v5 ,4). weight ( v4 , v7 ,1). 
weight ( v5 , v7 ,7). 
weight ( v6 , v7 ,2). weight ( v6 , v8 ,2). 
weight ( v7 , v9 ,3). 
weight ( v8 , v9 ,2).
weight ( m1 , m2 ,0).
weight ( m2 , m3 ,0).
weight ( m3 , m1 ,0).
target (n).
threshold (6).

现在是代码，后面是解释。

% select subset of nodes and vertices
(P) {select(X) : vertex(X)} (P) :- target(P).
(P-1) {select(X, Y) : weight(X, Y, Z)} (Q-1) :- target(P), target(Q).
     
% postion does not matter in an undirected graph.
directed(A,B):-select(A,B).
directed(B,A):-select(A,B).

% for every selected edge all nodes are selected
:- directed(A,_), vertex(A), not select(A).

% for every selected node there exists at least one edge
:- select(A), {directed(A,B):vertex(B)}0.

% select a direction for each selected edge
{dir(A,B);dir(B,A)}==1 :- select(A,B). 

% force them in an order
{ found(X,1..n) } == 1 :- select(X).
{ found(X,N):select(X) } == 1 :- N = 1..n.
% reject if one edge does not follow the order 
:- found(X,NX), found(Y,NY),  dir(X,Y), NY<NX.
% reject if 2 different edges end in the same vertex 
:- dir(X,Z), dir(Y,Z), X!=Y.

:- threshold(M), M < #sum {W,X,Y : select(X,Y), weight(X,Y,W); W,X,Z : select(X,Z), weight(X,Z,W) }.

#show select/2.

解释：

• 为了方便我，我在 select/1 谓词中添加了选定的顶点。
• 由于处理无向图总是需要检查两个位置，因此我添加了 directed/2 谓词，它是所选边的有向图版本。
• 接下来，我确保每个选定的顶点都有一条选定的边，反之亦然。
• 现在是复杂的部分：检测周期。为此，我使用谓词dir/2 强制每个选定的边缘在其两个方向之一。在有向图中测试树更容易。
• 接下来我向顶点下达命令found/2。有向边dir/2 只允许使用此命令。这会强制循环到某种行为。
• 现在是循环破坏器：如果选定的图有一个循环，那么来自dir/2 的两条边将在同一个顶点结束。拒绝。如果这只是 clgo 的一个不幸的猜测，那么它会找到一个更幸运的猜测来满足这个标准。
• 总和的计算是从您那里复制和粘贴的。

输出是16倍

select(v2,v4) select(v4,v7) select(v6,v7) select(v6,v8)

重复是因为found/2 中的顶点顺序可能不同，但仍然得到相同的结果。