On the performance of MaxSAT and MinSAT solvers on 2SAT-MaxOnes
Tóm tắt
We analyze and compare two solvers for Boolean optimization problems: WMaxSatz, a solver for Partial MaxSAT, and MinSatz, a solver for Partial MinSAT. Both MaxSAT and MinSAT are similar, but previous results indicate that when solving optimization problems using both solvers, the performance is quite different on some cases. For getting insights about the differences in the performance of the two solvers, we analyze their behaviour when solving 2SAT-MaxOnes problem instances, given that 2SAT-MaxOnes is probably the most simple, but NP-hard, optimization problem we can solve with them. The analysis is based first on the study of the bounds computed by both algorithms on some particular 2SAT-MaxOnes instances, characterized by the presence of certain particular structures. We find that the fraction of positive literals in the clauses is an important factor regarding the quality of the bounds computed by the algorithms. Then, we also study the importance of this factor on the typical case complexity of Random-p 2SAT-MaxOnes, a variant of the problem where instances are randomly generated with a probability p of having positive literals in the clauses. For the case p=0, the performance results indicate a clear advantage of MinSatz with respect to WMaxSatz, but as we consider positive values of p WMaxSatz starts to show a better performance, although at the same time the typical complexity of Random-p 2SAT-MaxOnes decreases as p increases. We also study the typical value of the bound computed by the two algorithms on these sets of instances, showing that the behaviour is consistent with our analysis of the bounds computed on the particular instances we studied first.
Tài liệu tham khảo
Abramé, A., Habet, D.: On the resiliency of unit propagation to max-resolution. In: proceedings of the 24th International Joint Conference on Artificial Intelligence (2015)
Ansótegui, C., Bonet, M.L., Levy, J.: Solving (weighted) partial maxSAT through satisfiability testing. In: Proceedings of SAT, vol. 2009, pp 427–440 (2009)
Ansótegui, C., Bonet, M.L., Levy, J.: Sat-based maxsat algorithms. Artif. Intell. 196, 77–105 (2013)
Argelich, J., Béjar, R., Fernández, C., Mateu, C.: On 2sat-maxones with unbalanced polarity: from easy problems to hard maxclique problems. In: proceedings of CCIA’2011, volume 232 of Frontiers in Artificial Intelligence and Applications, pp 21–30. IOS Press (2011)
Argelich, J., Li, C.M., Manyà, F., Planes, J.: The first and second maxSAT evaluations. JSAT 4(2–4), 251–278 (2008)
Argelich, J., Lynce, I., Marques-Silva, J.P.: On solving boolean multilevel optimization problems. In: Proceedings of IJCAI, vol. 2009, pp 393–398 (2009)
Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.). IOS Press (2009)
Bjorner, N., Narodytska, N.: Maximum satisfiability using cores and correction sets. In: proceedings of the 24th International Joint Conference on Artificial Intelligence (2015)
Cha, B., Iwama, K., Kambayashi, Y., Miyazaki, S.: Local search algorithms for partial maxSAT. In: AAAI’97, pp 263–268 (1997)
Chen, Y., Safarpour, S., Veneris, A.G., Marques-Silva, J.P.: Spatial and temporal design debug using partial maxSAT. In: Proceedings of 19th ACM Great Lakes Symposium on VLSI, pp 345–350 (2009)
Conrad, J., Gomes, C.P., van Hoeve, W.J., Sabharwal, A., Suter, J.: Connections in networks Hardness of feasibility versus optiMality. In: Proceedings of CPAIOR2007, pp 16–28 (2007)
Goerdt, A.: A threshold for unsatisfiability. J. Comput. Syst. Sci. 53(3), 469–486 (2006)
Graça, A., Lynce, I., Marques-Silva, J., Oliveira, A.L.: Haplotype inference combining pedigrees and unrelated individuals. In: WCB09, pp 27–36 (2009)
Håstad, J.: Clique is hard to approximate within n (1−𝜖). In: FOCS’06, pp 627–636 (1996)
Li, C.M., Manyà, F.: An exact inference scheme for minsat. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (2015)
Li, C.M., Manyà, F., Mohamedou, N.O., Planes, J.: Resolution-based lower bounds in maxSAT. Constraints 15(4), 456–484 (2010)
Li, C.M., Manyà, F., Planes, J.: New inference rules for Max-SAT. J. Artif Intell. Res. (JAIR) 30, 321–359 (2007)
Li, C.M., Quan, Z.: An efficient branch-and-bound algorithm based on maxSAT for the maximum clique problem. In: proceedings of AAAI’10, pp 128–133 (2010)
Li, C.M., Zhu, Z., Manyà, F., Simon, L.: Optimizing with minimum satisfiability. Artif. Intell. 190, 32–44 (2012)
Marques-Silva, J., Argelich, J., Graça, A., Lynce, I.: Boolean lexicographic optimization: algorithms & applications. Ann. Math. Artif. Intell. 62(3-4), 317–343 (2011)
Martins, R., Manquinho, V.M., Lynce, I.: Open-WBO A modular maxsat solver. In: Theory and Applications of Satisfiability Testing - SAT 2014 - 17th International Conference, Held as Part of the Vienna Summer of Logic, VSL 2014, pp 438–445. Proceedings, Vienna, Austria (2014)
Morgado, A., Dodaro, C., Marques-Silva, J.: Core-guided maxsat with soft cardinality constraints. In: Principles and Practice of Constraint Programming - 20th International Conference, CP 2014, pp 564–573. Proceedings, Lyon, France (2014)
Morgado, A., Heras, F., Liffiton, M.H., Planes, J., Marques-Silva, J.: Iterative and core-guided maxSAT solving: A survey and assessment. Constraints 18 (4), 478–534 (2013)
Rosa, E.D., Giunchiglia, E., Maratea, M.: Solving satisfiability problems with preferences. Constraints 15, 485–515 (2010)
Slaney, J.K., Walsh, T.: Phase transition behavior: from decision to optimization. In: Proceedings of SAT2002 (2002)
Zhang, W.: Phase transitions and backbones of 3-SAT and maximum 3-SAT. In: Proceedings of CP 2001, pp 153–167. Springer (2001)
Zhang, W., Korf, R.E.: A study of complexity transitions on the asymmetric traveling salesman problem. Artif. Intell. 81(1-2), 223–239 (1996)