2

我对 MaxSat 有一个想法，并且已经使用 MSU3 以及使用 minisat API 的顺序编码实现了一个简单的 Maxsat 求解器

我想知道是否有办法加快这个求解器的速度。

我附带了这篇论文： https ://www.researchgate.net/publication/264936663_Incremental_Cardinality_Constraints_for_MaxSAT

这谈到了增量弱化及其使用累加器编码的实现

有没有办法通过顺序编码来实现增量弱化？

这会大大加快速度吗？

4

1 回答 1

2

有没有办法通过顺序编码来实现增量弱化？

顺序计数器编码可以增量构建，也就是说，给定一个<= k(1..n)可以扩展为<= k+1(1..n)和的电路<= k(1..n+1)。当在 OptiMathSAT 中声明一个新的软子句时，我们在两个方向（即）上递增地扩展顺序计数器电路的大小。我看不出为什么不能只在一个维度上做到这一点。1kn

快速浏览一下结果部分后，看起来迭代编码明显优于增量弱化技术。因此，您不妨尝试实施前一种方法而不是后者。

迭代编码技术将需要从<= 0(1..n)顺序计数器编码开始并沿k维度逐步扩展。（正如论文中提到的，一些 MaxSAT 算法可能希望在两个方向上增加电路）。

  • 顺序计数器电路的输入将是每个软子句的否定文字，以便电路计算伪造的软子句的数量。

  • 在第一次迭代中，s_n_1将假定为false，将所有输入反向传播到false（即强制所有软子句为true）。

  • 如果第一步是unsat，则扩展<= 0(1..n)为 encode <= 1(1..n)，然后假设s_n_1是true并且在下一次可满足性检查中s_n_2是。false在搜索过程中，一旦将一个软子句分配给false，其余的软子句就会反向传播到 ，true除非发现新的冲突。

  • 重复。

这会大大加快速度吗？

如果没有坚如磐石的实验，就很难预测性能。但是，我的建议是去做：实施这种方法应该不难，而且论文的结果看起来很可靠。

顺序计数器编码需要子句，与在 pag应用k 简化后的累加器编码O(n * k)相同。6、辅助变量。鉴于类似的内存占用，类似的性能增益也是可能的。O(n * k)

于 2020-05-14T01:23:51.880 回答