zbMATH — the first resource for mathematics

Breaking cycle structure to improve lower bound for Max-SAT. (English) Zbl 07048079
Zhu, Daming (ed.) et al., Frontiers in algorithmics. 10th international workshop, FAW 2016, Qingdao, China, June 30 – July 2, 2016. Proceedings. Cham: Springer (ISBN 978-3-319-39816-7/pbk; 978-3-319-39817-4/ebook). Lecture Notes in Computer Science 9711, 111-124 (2016).
Summary: Many practical optimization problems can be translated to Max-SAT and solved using a Branch-and-Bound (BnB) Max-SAT solver. The performance of a BnB Max-SAT solver heavily depends on the quality of the lower bound. Lower bounds in state-of-the-art BnB Max-SAT solvers are based on detecting inconsistent subsets of clauses and then on applying Max-SAT resolution to transform each inconsistent subset of clauses into an equivalent set containing an empty clause and a number of compensation clauses. In this paper, we focus on the transformation of the inconsistent subsets of clauses containing one unit clause and a number of binary clauses. We show that Max-SAT resolution generates a lot of ternary compensation clauses when transforming such an inconsistent set, deteriorating the quality of the lower bound, and propose a new inference rule, called cycle breaking rule, to transform the inconsistent set. We prove the correctness of the rule and implement it in a new BnB Max-SAT solver called Brmaxsat. Experimental results showed that cycle breaking rule is very effective, especially on Max-2SAT.
For the entire collection see [Zbl 1407.68047].
68Wxx Algorithms in computer science
Full Text: DOI
[1] Cook, S.A.: The complexity of theorem proving procedures. In: Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, Shaker Heights, pp. 151–158 (1971)
[2] Zhang, L., Madigan, C.F., Moskewicz, M.H., Malik, S.: Efficient conflict driven learning in a boolean satisfiability solver. In: Proceedings of IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2001, pp. 279–285 (2001)
[3] Ansotegui, C., Bonet, M.L., Levy, J.: SAT-based MaxSAT algorithms. Artif. Intell. 196, 77–105 (2013) · Zbl 1270.68265
[4] Davies, J., Bacchus, F.: Postponing optimization to speed up MAXSAT solving. In: Schulte, C. (ed.) CP 2013. LNCS, vol. 8124, pp. 247–262. Springer, Heidelberg (2013)
[5] Gaspers, S., Sorkin, G.B.: A universally fastest algorithms for Max 2-Sat, Max 2-CSP, and everything in between. J. Comput. Syst. Sci. 78, 305–335 (2012) · Zbl 1238.68066
[6] Davis, M., Logemann, G., Loveland, D.: A machine program for theorem proving. Commun. ACM 5(7), 394–397 (1962) · Zbl 0217.54002
[7] Kuegel, A.: Improved exact solver for the weighted MAXSAT problem. In: Workshop Pragmatics of SAT, Edinburgh, Scotland (2010)
[8] Argelich, J., Li, C.-M., Manya, F.: An improved exact solver for partial Max-SAT. In: Proceedings of International Conference on Non-convex Programming: Local and Global Approaches, pp. 230–231 (2007)
[9] Liu, Y.-L., Li, C.-M., He, K.: Improved lower bounds in MAXSAT complete algorithm based optimizing inconsistent set. Chin. J. Comput. 10(36), 2087–2096 (2013)
[10] Abram, A., Habet, D.: On the resiliency of unit propagation to maxresolution. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI 2015), pp. 268–274 (2015)
[11] Anstegui, C., Malitsky, Y., Sellmann, M.: Max-SAT by Improved instance-specific algorithm configuration. In: Proceedings of the 28th National Conference on Artificial Intelligence (AAAI 2014), pp. 2594–2600 (2014)
[12] Tompkins, D.A.D., Hoos, H.H.: UBCSAT: an implementation and experimentation environment for SLS algorithms for SAT and MAX-SAT. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol. 3542, pp. 306–320. Springer, Heidelberg (2005) · Zbl 1122.68620
[13] Wallace, R., Freuder, E.: Comparative studies of constraint satisfaction and Davis-Putnam algorithms for maximum satisfiability problems. In: Johnson, D., Trick, M. (eds.) Cliques, Coloring and Satisfiability, vol. 26, pp. 587–615. American Mathematical Society, Providence (1996) · Zbl 0859.68072
[14] Shen, H., Zhang, H.: Study of lower bound functions for MAX-2SAT. In: Proceedings of the 19th National Conference on Artificial Intelligence (AAAI 2004), pp. 185–190 (2004)
[15] Li, C.-M., Manyà, F., Planes, J.: Exploiting unit propagation to compute lower bounds in branch and bound Max-SAT solvers. In: van Beek, P. (ed.) CP 2005. LNCS, vol. 3709, pp. 403–414. Springer, Heidelberg (2005) · Zbl 1153.68470
[16] Li, C.-M., Manya, F., Planes, J.: New inference rules for Max-SAT. J. Artif. Intell. Res. 30, 321–329 (2007) · Zbl 1182.68254
[17] Li, C.M., Manyà, F., Mohamedou, N., Planes, J.: Exploiting cycle structures in Max-SAT. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 467–480. Springer, Heidelberg (2009) · Zbl 1247.68256
[18] Li, C.-M., Manya, F., Mohamedou, N., Planes, J.: Resolution-based lower bounds in MaxSAT. Constraints 15(4), 456–484 (2010) · Zbl 1208.68204
[19] Bonet, M.L., Levy, J., Manya, F.: Resolution for Max-SAT. Artif. Intell. 171, 606–618 (2007) · Zbl 1168.68541
[20] Luo, C., Cai, S., Wu, W., Jie, Z., Su, K.: CCLS: an efficient local search algorithm for weighted maximum satisfiability. IEEE Trans. Comput. 64(7), 1830–1843 (2015) · Zbl 1360.68786
[21] Bansal, N., Raman, V.: Upper bounds for MaxSat: further improved. In: Aggarwal, A.K., Pandu Rangan, C. (eds.) ISAAC 1999. LNCS, vol. 1741, pp. 247–258. Springer, Heidelberg (1999) · Zbl 0971.68069
[22] Niedermeier, R., Rossmanith, P.: New upper bounds for maximum satisfiability. J. Algorithms 36, 63–88 (2000) · Zbl 0959.68049
[23] http://www.maxsat.udl.cat/index.html
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.