如何通过 SAT 和优化解决顶点覆盖问题？答案

【问题标题】：How to Solve Vertex Cover Problem by SAT and Optimization?如何通过 SAT 和优化解决顶点覆盖问题？
【发布时间】：2020-03-25 03:35:59
【问题描述】：

所以现在我正在使用 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 作为求解器。

【问题讨论】：

我没有在问题中看到任何优化组件，因为它与伪代码一起呈现，所以我猜模型的某些部分丢失了。您可以编辑您的问题并包括缺失的部分吗？如果有任何优化，优化程序是属于minisat的还是你自己写的？在后一种情况下，您介意详细说明它是如何工作的吗？

标签： c++ algorithm optimization sat optimathsat

【解决方案1】：

首先，让我假设我在理解您的编码时遇到了一些困难，所以我将从头开始。这就是我解决问题的方式。

注意：我的示例基于 SMT-LIB 语法，可以使用 MaxSMT 求解器求解，例如 z3 和 optimathsat。但是，由于它不使用任何 SMT 功能，您实际上可以使用 MaxSAT 比赛中使用的the standard WCNF format 编写相同的内容。在选择求解器来处理问题时，这将为您提供更多选择。我可能错了，但我推测 MaxSAT 求解器在这个特定问题上可能优于 MaxSMT 求解器。

令 G = {V, E} 为图。

首先，为图中的每个顶点声明一个布尔变量：

(declare-fun vertex_1 () Bool)
...
(declare-fun vertex_K () Bool)

（任何没有边的顶点都应该省略，因为这只会浪费时间。）

其次，为图中连接顶点i和顶点j的每条边声明一个布尔变量（假设无向）

(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，用一个软子句断言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）来获得一个覆盖所有边缘同时使用最少的模型顶点数（如果有）。

【讨论】：