我有一个关于MaxSat的想法，并且已经用MSU3实现了一个天真的Maxsat解算器，同时还用minisat APIs实现了顺序编码。
我想知道有没有办法加快这个解题速度。
我是带着这篇论文来的。https: /www.researchgate.netpublication264936663_Incremental_Cardinality_Constraints_for_MaxSAT
这说的是增量式弱化，它的实现采用累加器编码。
有没有办法用顺序编码实现增量弱化？
这是否会带来相当大的速度？
有没有办法用顺序编码实现增量减弱？
该 顺序计数器 编码可以逐步建立，即给定一个电路 <= 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 除非发现新的冲突。
重复一遍。
这样会不会有相当大的提速？
没有坚如磐石的实验，很难预测性能。然而，我的建议是去做：不应该是这样的。那么难 来实施这个方法，论文的结果看起来很扎实。
该 顺序计数器 编码要求 O(n * k) 句，数量同 累加器编码 涂抹 k-简化 在第6页，和 O(n * k) 辅助变量。考虑到类似的内存占用，也有可能获得类似的性能提升。