I've an idea about MaxSat and have already implemented a naive Maxsat solver using MSU3 along with sequential encoding with minisat APIs
I was wondering if there's a way to speed up this solver.
I came with this paper: https://www.researchgate.net/publication/264936663_Incremental_Cardinality_Constraints_for_MaxSAT
That talks about incremental weakening and it's implementation using totalizer encoding
Is there a way to implement incremental weakening with sequential encoding?
Will that give a considerable speed up?
Is there a way to implement incremental weakening with sequential encoding?
The sequential counter encoding can be built incrementally, that is, given a circuit <= k(1..n) this can be extended to <= k+1(1..n) and <= k(1..n+1). When asserting a new soft-clause in OptiMathSAT, we incrementally extend the size of the sequential counter circuit by 1 in both directions (i.e. k, n). I see no reason why this couldn't be done along one dimension only.
After a quick glance at the results sections, it looks like the iterative encoding is significantly better than the incremental weakening technique. So you might as well try to implement the former approach rather than the latter.
The iterative encoding technique would require starting from <= 0(1..n) and progressively extend the sequential counter encoding along the k dimension. (As mentioned in the paper, some MaxSAT algorithms may want to increase the circuit in both directions).
The inputs of the sequential counter circuit would be the negated literals of each soft-clause, so that the circuit counts the number of falsified soft-clauses.
At the first iteration, s_n_1 would be assumed to be false, back-propagating all inputs to false(i.e. forcing all soft-clauses to be true).
If the first step is unsat, one extends <= 0(1..n) to encode <= 1(1..n), and then assumes s_n_1 to be true and s_n_2 to be false at the next satisfiability check. During the search, as soon as one soft-clause is assigned to false, the remaining soft-clauses are back-propagated to true unless a new conflict is found.
Repeat.
Will that give a considerable speed up?
It's hard to predict performance without a rock-solid experiment. However, my suggestion is to go for it: it shouldn't be that hard to implement this approach and the results of the paper look solid.
The sequential counter encoding requires O(n * k) clauses, the same number as the totalizer encoding after applying the k-simplification at pag. 6, and O(n * k) auxiliary variables. Given the similar memory footprint, a similar performance gain is also possible.