所以现在我正在研究使用 SAT 来解决最小顶点覆盖问题,这是我对图 G = {V,E} 具有 k 个顶点覆盖的编码,以下是子句:
Let n = sizeof(V);
首先,至少有一个顶点位于顶点覆盖中:
For i in {1..k}
Add clause (x<1,i> ∨ x<2,i> ∨ ··· ∨ x<n,i>);
那么,任何一个顶点都不能在顶点覆盖中出现两次:
For j in {1..n}
For l and m in {1..k} with l < m
Add clause (¬x<j,l> ∨ ¬x<j,m>)
之后,顶点覆盖中的某一特定位置只能出现一个顶点:
For j in {1..k}
For l and m in {1..n} with l < m
Add clause (¬x<l,j> ∨ ¬x<m,j>)
最后,顶点覆盖中至少有一个顶点应来自边:
For i and j in each edge e from E
Add clause (x<i,1> ∨ x<i,2> ∨ ... ∨ x<i,k> ∨ x<j,1> ∨ ... ∨ x<j,k>)
现在我可以通过使用这种编码来获得最小顶点覆盖,但效率很差。我只能得到顶点数 < 20 个的图的结果,否则只需要几分钟和几小时才能得到结果。我现在正在考虑从 SAT 进一步降低,也许到 3SAT。但看起来我不能简单地将所有子句从 nCNF 更改为 3CNF 以获得相同的结果。谁能帮我弄清楚我下一步应该做什么?我需要全新的编码吗?
非常感谢。
顺便说一句,我使用 MiniSAT 作为求解器。
最佳答案
首先,我假设我无法理解您的编码,所以我将从头开始。这就是我解决问题的方法。
注意:我的示例基于 SMT-LIB语法,可以使用 MaxSMT 求解器求解,例如 z3和 optimathsat 。但是,由于它不使用任何 SMT 功能,因此您实际上可以使用 the standard WCNF format 编写相同的内容。用于MaxSAT比赛。这将为您在选择求解器来处理问题时提供更多选择。我可能是错的,但我推测 MaxSAT 求解器在这个特定问题上可能优于 MaxSMT 求解器。
设 G = {V, E} 为图表。
首先,为图中的每个顶点声明一个 bool 变量:
(declare-fun vertex_1 () Bool)
...
(declare-fun vertex_K () Bool)
(任何没有边的顶点都应该被省略,因为它只会浪费时间。)
其次,为图中连接顶点 i
和顶点 j
的每条边声明一个 bool 变量(假设无向)
(declare-fun edge_i_j () Bool)
...
第三,断言必须覆盖每条边edge_i_j
:
(assert edge_i_j)
...
第四,如果一条边 edge_i_j
被覆盖,则顶点 i
或顶点 j
必须为 true
:
(assert (=> edge_i_j (or vertex_i vertex_j)))
...
第五,对于每个 vertex_i
,使用 soft 子句断言 vertex_i
应该为 false
。如果情况并非如此,则对 cover
的值进行值 1
的惩罚:
(assert-soft (not vertex_i) :weight 1 :id cover)
最后解决问题:
(set-option :config opt.maxsmt_engine=maxres) ; only for optimathsat
(minimize cover) ; only for optimathsat
(check-sat)
(get-objectives)
(get-model)
此时,我们可以使用任何高效的 MaxSAT/MaxSMT 引擎(例如 MaxRes )来获得一个覆盖所有边缘的模型,同时使用最少的资源顶点数(如果有)。
关于c++ - 如何通过SAT和优化解决顶点覆盖问题?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/59106461/