我对 MaxSat 有一个想法，并且已经使用 MSU3 以及使用 minisat API 的顺序编码实现了一个简单的 Maxsat 求解器
我想知道是否有办法加快这个求解器的速度。
我带来了这篇论文： https://www.researchgate.net/publication/264936663_Incremental_Cardinality_Constraints_for_MaxSAT
这谈到了增量弱化及其使用累加器编码的实现
有没有办法通过顺序编码来实现增量弱化？
这会大大加快速度吗？
【问题讨论】：
标签： smt constraint-programming sat satisfiability sat-solvers
有没有办法通过顺序编码实现增量弱化？
顺序计数器编码可以增量构建，也就是说，给定一个电路<= k(1..n)，它可以扩展到<= k+1(1..n)和<= k(1..n+1)。当在 OptiMathSAT 中声明一个新的软子句时，我们在两个方向（即k、n）将顺序计数器电路的大小递增地扩展1。我看不出为什么不能只在一个维度上做到这一点。
快速浏览一下结果部分后，看起来迭代编码明显优于增量弱化技术。所以你不妨尝试实现前一种方法而不是后者。
迭代编码技术需要从<= 0(1..n) 开始，并沿着k 维度逐步扩展顺序计数器编码。 （如论文中提到的，一些MaxSAT算法可能希望在两个方向上增加电路）。
顺序计数器电路的输入将是每个软子句的否定文字，以便电路计算伪造的软子句的数量。
在第一次迭代中，s_n_1 将被假定为 false，将所有输入反向传播到 false（即强制所有软子句为 true）。
false，其余的软子句就会反向传播到true，除非发现新的冲突。
重复。
这会大大加快速度吗？
如果没有坚如磐石的实验，就很难预测性能。但是，我的建议是去做：实施这种方法应该不会那么难，而且论文的结果看起来很可靠。
顺序计数器编码需要O(n * k)子句，与在pag应用k-simplification后的totalizer encoding相同。 6、和O(n * k)辅助变量。考虑到类似的内存占用，也有可能获得类似的性能提升。
【讨论】：