smt - 增量减弱 Maxsat

Question

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

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

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

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

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

这会带来相当大的速度吗？

Answer 1

Is there a way to implement incremental weakening with sequential encoding?

顺序计数器编码可以增量构建，即给定电路 <= k(1..n)这可以扩展到 <= k+1(1..n)和 <= k(1..n+1) .在 OptiMathSAT 中断言新的软子句时，我们将顺序计数器电路的大小增加了 1在两个方向(即 k ， n )。我看不出为什么不能仅沿一维完成此操作。

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

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

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

在第一次迭代中，s_n_1将被假定为 false ，将所有输入反向传播到 false (即强制所有软条款为 true )。

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

重复。

Will that give a considerable speed up?

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

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