In this paper we describe several variations of the incremental MSU3 and MSU4 algorithms for the MaxSAT problem, and show that some of these improve performance. Among the variations considered are new cardinality constraint encodings which enable incrementally updating the constraint, and have smaller worst-case size than those encodings previously considered. The new cardinality encodings are based on the well-known sorting networks. The incremental approach is also extended, in a novel way, inspired by the idea behind resizing arrays. Best performance was achieved when the totalizer encoding was used in conjunction with sorting networks; unlike other implementations of such combinations in the literature we found that to get best performance, sorting networks should be used very sparingly. We submitted a solver using a version of the methods described in this paper to the 2017 MaxSAT evaluation where it placed fourth out of 8 solvers participating in the unweighted category.
I.Abío, R.Nieuwenhuis, A.Oliveras and E.Rodríguez-Carbonell, A parametric approach for smaller and better encodings of cardinality constraints, in: Principles and Practice of Constraint Programming, Springer, 2013, pp. 80–96. doi:10.1007/978-3-642-40627-0_9.
4.
M.Ajtai, J.Komlós and E.Szemerédi, An O(n log n) sorting network, in: Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, ACM, 1983, pp. 1–9.
5.
C.Ansótegui, M.L.Bonet and J.Levy, Solving (weighted) partial MaxSAT through satisfiability testing, in: Theory and Applications of Satisfiability Testing – SAT 2009, Springer, 2009, pp. 427–440. doi:10.1007/978-3-642-02777-2_39.
6.
J.Argelich, D.Le Berre, I.Lynce, J.Marques-Silva and P.Rapicault, Solving Linux upgradeability problems using Boolean optimization, in: Proceedings First International Workshop on Logics for Component Configuration, EPTCS, 2010, pp. 11–23.
7.
R.Asín, R.Nieuwenhuis, A.Oliveras and E.Rodríguez-Carbonell, Cardinality networks: A theoretical and empirical study, Constraints16(2) (2011), 195–221. doi:10.1007/s10601-010-9105-0.
8.
G.Audemard and L.Simon, Predicting learnt clauses quality in modern SAT solvers, in: Proceedings of the Twenty-First International Joint Conference on Artificial Intelligence, Vol. 3, IJCAI, 2009, pp. 399–404.
9.
O.Bailleux and Y.Boufkhad, Efficient CNF encoding of Boolean cardinality constraints, in: Principles and Practice of Constraint Programming, Springer, 2003, pp. 108–122.
10.
K.E.Batcher, Sorting networks and their applications, in: Proceedings of the April 30–May 2, 1968, Spring Joint Computer Conference, ACM, 1968, pp. 307–314.
11.
Y.Chen, S.Safarpour, A.Veneris and J.Marques-Silva, Spatial and temporal design debug using partial MaxSAT, in: Proceedings of the 19th ACM Great Lakes Symposium on VLSI, ACM, 2009, pp. 345–350.
12.
M.Codish and M.Zazon-Ivry, Pairwise cardinality networks, in: Logic for Programming, Artificial Intelligence, and Reasoning, Springer, 2010, pp. 154–172. doi:10.1007/978-3-642-17511-4_10.
13.
J.Davies and F.Bacchus, Exploiting the power of MIP solvers in MAXSAT, in: Theory and Applications of Satisfiability Testing – SAT 2013, Springer, 2013, pp. 166–181. doi:10.1007/978-3-642-39071-5_13.
14.
N.Eén and A.Biere, Effective preprocessing in SAT through variable and clause elimination, in: Theory and Applications of Satisfiability Testing – SAT 2005, Springer, 2005, pp. 61–75.
15.
N.Eén and N.Sörensson, Translating pseudo-Boolean constraints into SAT, Journal on Satisfiability, Boolean Modeling and Computation2(3–4) (2006), 1–25.
16.
Z.Fu and S.Malik, On solving the partial MAX-SAT problem, in: Theory and Applications of Satisfiability Testing – SAT 2006, Springer, 2006, pp. 252–265. doi:10.1007/11814948_25.
17.
M.Koshimura, T.Zhang, H.Fujita and Ryuzo, Hasegawa. QMaxSAT: A partial Max-SAT solver, Journal on Satisfiability, Boolean Modeling and Computation8 (2012), 95–100.
18.
C.M.Li and F.Manyà, MaxSAT, hard and soft constraints, in: Handbook of Satisfiability, A.Biere, M.Heule and H.van Maaren, eds, Vol. 185, IOS Press, 2009.
19.
C.M.Li, F.Manyà and J.Planes, New inference rules for Max-SAT, Journal of Artificial Intelligence Research (JAIR)30(1) (2007), 321–359.
20.
J.Marques-Sila and J.Planes, Algorithms for maximum satisfiability using unsatisfiable cores, in: Advanced Techniques in Logic Synthesis, Optimizations and Applications, Springer, 2011, pp. 171–182. doi:10.1007/978-1-4419-7518-8_10.
21.
J.Marques-Silva and J.Planes, On using unsatisfiability for solving maximum satisfiability, Preprint, arXiv:0712.1097, 2007.
22.
R.Martins, Parallel search for maximum satisfiability, PhD thesis, Instituto Superior Técnico, 2013.
23.
R.Martins, S.Joshi, V.Manquinho and I.Lynce, Incremental cardinality constraints for MaxSAT, in: Principles and Practice of Constraint Programming, Springer, 2014, pp. 531–548.
24.
R.Martins, V.Manquinho and I.Lynce, Open-wbo: A modular MaxSAT solver, in: Theory and Applications of Satisfiability Testing – SAT 2014, Springer, 2014, pp. 438–445.
