undirected-graph - 如何使用答案集编程从图中提取树?
问题描述
有一个无向图 (V,E),边上的权重 w : E → N,目标 k ∈ N,阈值 O ∈ N。找到权重小于阈值的图的 k 顶点树。也就是说,分别从V和E中选择k个顶点和k-1条边,使得它们构成一棵树,并且所选择的边的权重之和小于O。
编写一个 ASP 程序,将 V、E、w、k 和 O 作为输入,并找到满足约束的边的选择,如果不能满足约束,则输出“不可满足”。选择边隐含地导致选择顶点,因此不需要显式显示所选顶点。
通过谓词 vertex/1、weight/3、target/1 和 threshold/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.
我该如何纠正?
解决方案
好的,那是相当复杂的。我很确定我的解决方案并不完美,我也是初学者。
在开始编写代码之前,让我们再次检查一个问题:要求是选择k
节点和k-1
边。如果您稍微考虑一下,这可以形成两种模式:一棵连通树或多个非连通图,其中至少有一个循环。因此,如果您确保没有循环,您将获得一棵连接的树。
我在事实中添加了一些节点来检查是否形成了树或是否找到了廉价的未连接循环,为此我必须更改target
并threshold
设置更高的值。
#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
谓词,它是所选边的有向图版本。 - 接下来,我确保每个选定的顶点都有一个选定的边,反之亦然。
- 现在是复杂的部分:检测周期。为此,我通过使用 predicate 强制每个选定的边缘在其两个方向之一
dir/2
。在有向图中测试树更容易。 - 接下来我
found/2
对顶点下订单。dir/2
仅允许使用此顺序的有向边。这会强制循环到某种行为。 - 现在是循环破坏器:如果选定的图有一个循环,那么来自的两条边
dir/2
将在同一个顶点结束。拒绝。如果这只是来自 cligo 的一个不幸的猜测,那么它会找到一个更幸运的猜测来满足这个标准。 - 总和的计算是从您那里复制和粘贴的。
输出为16倍
select(v2,v4) select(v4,v7) select(v6,v7) select(v6,v8)
重复来自这样一个事实,即顶点的顺序found/2
可以不同但仍然得到相同的结果。
推荐阅读
- angular - 以角度 8 从简单 api 打印数据
- java - 如何获取 SAST 的 ZoneId?
- zabbix - zabbix监控url响应时间apache访问日志
- javascript - 持久性设置为本地时 onAuthStateChanged() 的奇怪行为
- javascript - HTML 复选框/选择:只读与禁用
- python - 只能连接错误,不知道该怎么做
- hyperledger-fabric - 尝试使分类帐在 rafts 中持久存在时出错
- typescript - 如何在 TypeScript 中将对象属性作为参数传递
- django - 如何在 Django 3.0.8 中更改 USERNAME_FIELD。不创建自定义用户?
- r - R Shiny动态编辑reactiveTimer定时器间隔